Reactive Schedulingconcept:reactive-scheduling

machine-typed-not-haltedclaim:machine-typed-not-halted

Halted machine configuration outside MachineTyped invariant

A halted machine is outside J (row 139; probe C's typedState_halt, read at J).

Module

Effect4.Laws.Program.Typed.Assembly

Literature

PFPL, ch. 28, §28.2, p. 263 (adaptedResult)

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy)
  (w : Effect4.Program.Typed.World) (m : Effect4.Program.Sched.RState)
  (why : Effect4.Machine.Stuck),
  Not (Effect4.Program.Typed.MachineTyped root rootTy w (Effect4.Machine.RunMachine.halt m why))

flush-fairclaim:flush-fair

Every initially armed owner in a duplicate-free queue is entered within its length in rounds

LIVE/fair: under enough command fuel for the initial queue, every initially armed owner is entered within its length in rounds, even if callbacks rearm.

Module

Effect4.Laws.Machine.Scheduling

Literature

LynchVaandrager1995, audit C4 (proofTechnique)

∀ {ν σ : Type u} {β : Type v} {ε δ ι α χ : Type u} {St : Type (max u v)} [inst : DecidableEq ε]
  [inst_1 : DecidableEq δ] [inst_2 : DecidableEq ι] [inst_3 : DecidableEq α]
  (interp : Effect4.Machine.RunInterp ν σ β ε δ ι α χ St) (fuel rounds : Nat)
  (m : Effect4.Machine.RunMachine ν σ β ε δ ι α χ St),
  (m.armed (Effect4.Prim ν σ β ε δ ι α) (Effect4.FrameFiber ν σ β ε δ ι α)
        (Effect4.FrameEvent ν σ β ε δ ι α)).Nodup →
    Eq
        (Effect4.Machine.Scheduling.FlushReady interp fuel
          (m.armed (Effect4.Prim ν σ β ε δ ι α) (Effect4.FrameFiber ν σ β ε δ ι α)
              (Effect4.FrameEvent ν σ β ε δ ι α)).length
          m)
        Bool.true →
      instLENat.le
          (m.armed (Effect4.Prim ν σ β ε δ ι α) (Effect4.FrameFiber ν σ β ε δ ι α)
              (Effect4.FrameEvent ν σ β ε δ ι α)).length
          rounds →
        ∀ (owner : Effect4.FiberId),
          List.instMembership.mem
              (m.armed (Effect4.Prim ν σ β ε δ ι α) (Effect4.FrameFiber ν σ β ε δ ι α)
                (Effect4.FrameEvent ν σ β ε δ ι α))
              owner →
            Eq (Effect4.Machine.Scheduling.FiredWithin interp fuel rounds m owner) Bool.true

random-descentclaim:random-descent

Under a bisimulation that is an equivalence, and the local diamond up to it, every complete tape of a step labelled by decisions has one length and an equal end; one complete tape bounds every tape. Nothing of the machine: the checked fragment of decisions row 361 is its use

Every complete tape has the same length and an R-equal end. The pointer of the claim random-descent.

Module

Effect4.Laws.Machine.Descent

∀ {S : Type u} {D : Type v} {step : S → D → Option S} {R : S → S → Prop},
  Equivalence R →
    Effect4.Machine.Descent.Bisim step R →
      Effect4.Machine.Descent.Diamond step R →
        ∀ {s t1 t2 : S} {c1 c2 : List D},
          Eq (Effect4.Machine.Descent.run step s c1) (Option.some t1) →
            Effect4.Machine.Descent.Terminal step t1 →
              Eq (Effect4.Machine.Descent.run step s c2) (Option.some t2) →
                Effect4.Machine.Descent.Terminal step t2 → And (R t1 t2) (Eq c1.length c2.length)

step-loop-preservesclaim:step-loop-preserves

The loop decision preserves configuration typing

loop keeps I (loop_preserves): every clause, the walk.

Module

Effect4.Laws.Program.Typed.Commands.Clauses.All

Literature

WrightFelleisen1994, audit P36 (adaptedResult)

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy)
  (id : Effect4.FiberId) (y : Bool),
  Effect4.Program.Typed.StepPreserves root rootTy (Effect4.Machine.Cmd.loop id y)

Register record E4-TYPED-CE-025 (REPAIRED)

| `E4-TYPED-CE-025` | REPAIRED 2026-10-03 (row 134 (b), the waiter column `MachineWide.waiters`; the refuted goals `M6Ledger.step_loop` and `step_deliver` are proved over it: `loop_preserves`, `deliver_preserves`, `Typed/Commands/Clauses/All.lean`, `053aa3d9`, `[propext, Quot.sound]`); SEEDED 2026-10-01 (seat D3, `5789df56`, merged `7d50cfe6`; kernel-checked at `[propext, Quot.sound]`) | `StepPreserves` for `loop` and `deliver` is false: completing a Deferred owes its waiters the completion at tokens no clause relates to the cell | `docs/research/2026-10-01-landing/seat-D3/probes/LoopDeliver.lean`: `loop_false`, `deliver_false` | row 134 (b): a waiter column in `J` (ruled; seat D5) |

step-deliver-preservesclaim:step-deliver-preserves

The deliver decision preserves configuration typing

deliver keeps I (deliver_preserves): every clause, the walk.

Module

Effect4.Laws.Program.Typed.Commands.Clauses.All

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy)
  (id : Effect4.FiberId) (y : Bool),
  Effect4.Program.Typed.StepPreserves root rootTy (Effect4.Machine.Cmd.deliver id y)

Register record E4-TYPED-CE-025 (REPAIRED)

| `E4-TYPED-CE-025` | REPAIRED 2026-10-03 (row 134 (b), the waiter column `MachineWide.waiters`; the refuted goals `M6Ledger.step_loop` and `step_deliver` are proved over it: `loop_preserves`, `deliver_preserves`, `Typed/Commands/Clauses/All.lean`, `053aa3d9`, `[propext, Quot.sound]`); SEEDED 2026-10-01 (seat D3, `5789df56`, merged `7d50cfe6`; kernel-checked at `[propext, Quot.sound]`) | `StepPreserves` for `loop` and `deliver` is false: completing a Deferred owes its waiters the completion at tokens no clause relates to the cell | `docs/research/2026-10-01-landing/seat-D3/probes/LoopDeliver.lean`: `loop_false`, `deliver_false` | row 134 (b): a waiter column in `J` (ruled; seat D5) |

store-frame-typingclaim:store-frame-typing

A store edit satisfying the stated frame, store typing, key and due-owner premises keeps configuration typing

A store edit keeps I at the world over the edited store (note.md §4): the views J reads move as the frame says, and the new store states its own clauses (well-formedness, the generated store typing, no new internal key, owners for its scheduled due entries).

Module

Effect4.Laws.Program.Typed.Commands.Bookkeeping

Literature

deVilhenaPottier2021, §4.2.4 (frame rule); audit P8 (analogy)

∀ {root : Effect4.Program.Typed.ProgramSource} {rootTy : Effect4.Program.EffTy}
  {w : Effect4.Program.Typed.World} {m : Effect4.Program.Sched.RState}
  {q : List Effect4.Program.Sched.RCmd},
  Effect4.Program.Typed.ConfigTyped root rootTy w m q →
    ∀ {s : Effect4.Machine.Stores},
      Effect4.Program.Typed.StoreFrame m.state s →
        s.WF →
          Effect4.Program.Typed.StoresOk (Effect4.Program.Typed.preds root)
              { ids := w.ids, state := s, Γ := w.Γ, «Π» := w.«Π», Ρ := w.Ρ, Θ := w.Θ,
                serviceTy := w.serviceTy }
              Effect4.Program.Typed.Expect.root s →
            List.instHasSubset.Subset
                (Effect4.Program.Guard.internalKeys
                  { fibers := m.fibers, races := m.races, nextId := m.nextId,
                    nextToken := m.nextToken, nextRace := m.nextRace,
                    middlewareInstalled := m.middlewareInstalled, armed := m.armed, state := s,
                    trace := m.trace, stuck := m.stuck, forks := m.forks })
                (Effect4.Program.Guard.internalKeys m) →
              (∀
                  (o :
                    Effect4.Machine.Owed
                      (Effect4.Machine.Completion Effect4.Machine.Val Effect4.Machine.Err
                        Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)),
                  List.instMembership.mem
                      (s.deferreds.due
                        (Effect4.Machine.Completion Effect4.Machine.Val Effect4.Machine.Err
                          Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann))
                      o →
                    ∀ (owner : Effect4.FiberId) (priority : Nat),
                      Eq o.mode (Effect4.Machine.WakeMode.scheduled owner priority) →
                        Eq (Effect4.Machine.RunMachine.fiber? m owner).isSome Bool.true) →
                And
                  (w.leHost
                    { ids := w.ids, state := s, Γ := w.Γ, «Π» := w.«Π», Ρ := w.Ρ, Θ := w.Θ,
                      serviceTy := w.serviceTy })
                  (Effect4.Program.Typed.ConfigTyped root rootTy
                    { ids := w.ids, state := s, Γ := w.Γ, «Π» := w.«Π», Ρ := w.Ρ, Θ := w.Θ,
                      serviceTy := w.serviceTy }
                    { fibers := m.fibers, races := m.races, nextId := m.nextId,
                      nextToken := m.nextToken, nextRace := m.nextRace,
                      middlewareInstalled := m.middlewareInstalled, armed := m.armed, state := s,
                      trace := m.trace, stuck := m.stuck, forks := m.forks }
                    q)

waiter-completion-typingclaim:waiter-completion-typing

A completion fitting its cell's columns meets a waiter's declared answer and error demand

The waiter → due transfer (note.md §3): a waiter declared at a type that accepts its cell's columns accepts any completion the cell holds, the cell's completion moving along both columns (fitsExit_sub; a delayed read along the checker's order, Ty.sub_le_subN).

Module

Effect4.Laws.Program.Typed.Commands.Bookkeeping

Literature

deVilhenaPottier2021, §3.3 (protocol subsumption); audit P8 (proofTechnique)

∀ {w : Effect4.Program.Typed.World} {a e : Effect4.Program.Ty} {ty : Effect4.Program.EffTy}
  {c :
    Effect4.Machine.Completion Effect4.Machine.Val Effect4.Machine.Err Effect4.Machine.Defect
      Effect4.FiberId Effect4.Machine.Ann},
  Effect4.Program.Typed.AwaitDemand a e ty →
    Effect4.Program.Typed.CompletionStrong w
        { answer := a, error := e, requires := Effect4.Machine.Env.Requirement.empty } c →
      Effect4.Program.Typed.CompletionStrong w ty c

step-wake-preservesclaim:step-wake-preserves

The wake command keeps configuration typing through its waiter-to-due transfer

wake keeps I at the world over the woken store.

Module

Effect4.Laws.Program.Typed.Commands.Bookkeeping

Literature

LynchVaandrager1995, §6 (invariants); audit C4 (proofTechnique)

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy)
  (list : Effect4.Machine.WakeKey) (phase : Effect4.Machine.WakePhase),
  Effect4.Program.Typed.StepPreserves root rootTy (Effect4.Machine.Cmd.wake list phase)

step-launch-preservesclaim:step-launch-preserves

The launch command keeps configuration typing when adding a fresh race entrant

launch keeps I (Machine/Fibers.lean:1879-1896, rc.112 :1520-1528): the entrant is allocated at the old nextId and declared at the race's result type (its program, typed at a type whose columns are below it, widened there; closed because the race token's declaration is), the race loses that program, and the entrant's evaluation and enrollment are queued ahead of the next launch. Every other arm leaves the machine and drops the head.

Module

Effect4.Laws.Program.Typed.Commands.Launch

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy) (raceId : Nat),
  Effect4.Program.Typed.StepPreserves root rootTy (Effect4.Machine.Cmd.launch raceId)

Register record E4-TYPED-CE-029 (REPAIRED)

| `E4-TYPED-CE-029` | REPAIRED 2026-10-03 (row 134 (e), fresh-bounded fiber ids; the refuted goal `M6Ledger.step_launch` is proved over it: `launch_preserves`, `Typed/Commands/Launch.lean`); SEEDED 2026-10-01 (seat D3, `5789df56`, merged `7d50cfe6`; kernel-checked at `[propext, Quot.sound]`) | `StepPreserves` for `launch` is false: a race's live set may name the next fiber id | `docs/research/2026-10-01-landing/seat-D3/probes/Races.lean`: `Launch.launch_false` | row 134 (e): fresh-bounded fiber ids (ruled; seat D5) |

step-registration-done-preservesclaim:step-registration-done-preserves

Completing race registration keeps configuration typing through immediate settlement or parking

registrationDone keeps I at the same world (Concept 4, scheduler step preservation; Machine/Fibers.lean:1912-1931). The head's authority names the race and its running, unparked host on the race's marker; RegistrationState gives the race token's declared type resultTy and a host stack accepting it (StackReply); RaceOk gives the race column at that type (RacePayload), which does not read registering. An accepted exit is typed by the column and installed as raceSettle (raceSettle_typed) under the queued loop. With no answer the cancel frame is pushed (stackAccepts_raceFinalizer): a deferred interrupt clears the park and the queued loop reads the marker, which ReadCode leaves to RegistrationState; otherwise the host parks idle at the race key with a void record, which no observer reads (decisions row 134 (d); configTyped_rupdate_park), and the race retains its declared token.

Module

Effect4.Laws.Program.Typed.Commands.Registration

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy) (raceId : Nat)
  (yielding : Bool),
  Effect4.Program.Typed.StepPreserves root rootTy
    (Effect4.Machine.Cmd.registrationDone raceId yielding)

drivestate-liftclaim:drivestate-lift

Command loop invariant lifting for driveState

Lift 1, the command loop. One fact per command gives the fact for driveState at every fuel, machine and pending list, at some later world.

Module

Effect4.Laws.Machine.Lift

Literature

PFPL, ch. 28, pp. 261–268 (proofTechnique)

∀ {ν σ : Type u} {β : Type v} {ε δ ι α χ : Type u} {St : Type (max u v)} [inst : DecidableEq ε]
  [inst_1 : DecidableEq δ] [inst_2 : DecidableEq ι] [inst_3 : DecidableEq α]
  {κ φ η : Type (max u v)} [inst_4 : Effect4.Machine.FiberCore ν β ε δ ι α κ φ]
  [inst_5 : Effect4.Machine.FiberEvaluator ν σ β ε δ ι α χ St κ φ η] {W : Type w}
  (o : Effect4.Laws.Effects.WorldOrder W) (interp : Effect4.Machine.RunInterp ν σ β ε δ ι α χ St κ)
  (I :
    W →
      Effect4.Machine.RunMachine ν σ β ε δ ι α χ St κ φ η →
        List (Effect4.Machine.Cmd ν σ β ε δ ι α κ) → Prop),
  Effect4.Machine.Lift.StepKeeps o interp I →
    ∀ (fuel : Nat) (w : W) (m : Effect4.Machine.RunMachine ν σ β ε δ ι α χ St κ φ η)
      (cmds : List (Effect4.Machine.Cmd ν σ β ε δ ι α κ)),
      I w m cmds →
        Exists fun w' =>
          And (o.le w w')
            (I w' (Effect4.Machine.driveState interp fuel m cmds).fst
              (Effect4.Machine.driveState interp fuel m cmds).snd)

typed-state-admittedclaim:typed-state-admitted

Every admitted replay of a checked program ends in J: host answers admitted at the ghost token table keep the typed state

Every admitted replay of a checked program is typed: the reference replay of a tape whose host answers are admitted (AdmittedTape, the ghost admission at Θ) ends in J, for every checked closed program, with row 117's empty requirement row at the load. M5 (load_typed) and M6 (decision_preserves) through admitted_typed. Concept 4 (typed-state-reachable); it reduces the host lane's typing half (T4) to executable admission (admit_sound, decisions rows 97–99).

Module

Effect4.Laws.Program.Typed.Commands.Clauses.All

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy) (fuel : Nat),
  Eq (Effect4.Program.typeOfProgram root.sig.signature root.program) (Option.some rootTy) →
    Eq rootTy.requires Effect4.Machine.Env.Requirement.empty →
      ∀ (tape : List Effect4.Api.Decision),
        Effect4.Program.Typed.AdmittedTape root rootTy fuel tape →
          Exists fun w =>
            Effect4.Program.Typed.MachineTyped root rootTy w
              (Effect4.Machine.ReplayResult.machine
                (Effect4.Program.Sched.replayR root.program fuel tape))

run-work-selectionclaim:run-work-selection

The opt-in control planner selects exactly a queued flush or the first runnable evaluation on a non-stuck machine

The selected control belongs to the declared two-choice policy.

Module

Effect4.Laws.Run

∀ (s : Effect4.Run) (decision : Effect4.Api.Decision),
  Iff (Eq s.nextControl (Option.some decision))
    (And
      (Eq
        (s.machine.stuck
          (Effect4.Prim Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
            Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
          (Effect4.FrameFiber Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
            Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
          (Effect4.FrameEvent Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
            Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann))
        Option.none)
      (Or (And (Eq decision Effect4.Api.flush) (Ne s.work.queued List.nil))
        (Exists fun fiber =>
          And (Eq decision (Effect4.Machine.RunDecision.evaluate fiber))
            (And (Eq s.work.queued List.nil) (Eq s.work.runnable.head? (Option.some fiber))))))

scheduler-progressclaim:scheduler-progress

Operational progress with successor transitions or live frontier classification

fair-tape-drains-armedclaim:fair-tape-drains-armed

A fair finite tape that suffices leaves no armed owner at its live end (R12-a: the finite endpoint consequence of FairTape's final prefix; not general fairness, not infinite tapes)

A fair finite tape leaves nothing armed at its live end (R12-a, the finite endpoint consequence): when the whole tape suffices and its replay is not stuck, FairTape at the split tape ++ [] asks each armed owner for a later servicing decision inside the empty suffix, so no owner is armed. Concept reactive-scheduling, claim fair-tape-drains-armed. Reach: one finite tape, at any interpreter and fuel. It does not establish liveness on infinite tapes, termination, host progress, general scheduler fairness (flush_fair permits rearming), or that the frontier names the remaining waits (R12-b). It serves R12 as the finite half of "liveness under FairTape".

Module

Effect4.Laws.Machine.Scheduling

∀ {ν σ : Type u} {β : Type v} {ε δ ι α χ : Type u} {St : Type (max u v)} [inst : DecidableEq ε]
  [inst_1 : DecidableEq δ] [inst_2 : DecidableEq ι] [inst_3 : DecidableEq α]
  (interp : Effect4.Machine.RunInterp ν σ β ε δ ι α χ St) (fuel : Nat)
  (m : Effect4.Machine.RunMachine ν σ β ε δ ι α χ St)
  (tape : List (Effect4.Machine.RunDecision ν σ β ε δ ι α)),
  Effect4.Machine.Scheduling.FairTape interp fuel m tape →
    Eq (Effect4.Machine.Suffices interp fuel tape m) Bool.true →
      Eq
          ((Effect4.Machine.replayEval interp fuel tape m).machine.stuck
            (Effect4.Prim ν σ β ε δ ι α) (Effect4.FrameFiber ν σ β ε δ ι α)
            (Effect4.FrameEvent ν σ β ε δ ι α))
          Option.none →
        Eq
          ((Effect4.Machine.replayEval interp fuel tape m).machine.armed
            (Effect4.Prim ν σ β ε δ ι α) (Effect4.FrameFiber ν σ β ε δ ι α)
            (Effect4.FrameEvent ν σ β ε δ ι α))
          List.nil

frontier-names-workclaim:frontier-names-work

R12-b: at a live, unfinished machine whose tape ran out, the frontier is empty exactly at a deadlock: nothing runnable, nothing armed, no host request, no timer, no compile budget (not progress, not liveness)

R12-b: at a live, unfinished machine, the tape frontier is empty exactly at a deadlock. So the frontier names a reason whenever work is armed (E4-SCHED-CE-021, repaired by decisions row 201 (b)).

Concept reactive-scheduling, claim frontier-names-work: the frontier half of the classification that scheduler-progress asks for. Reach: every frame machine (NativeMachine), with no reachability or typing premise, at the tape exhaustion site; a fuel frontier always names .commandFuel (commandFuel_iff). It does not establish that the named decision steps the machine, what any decision does at a deadlocked machine, or liveness (R12-c). It serves R12: Deadlocked requires nothing armed.

Module

Effect4.Laws.Api.Frontier

∀ (m : Effect4.Program.NativeMachine),
  Eq
      (m.stuck
        (Effect4.Prim Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
          Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
        (Effect4.FrameFiber Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
          Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
        (Effect4.FrameEvent Effect4.Program.EffName Effect4.Program.EffThunk Effect4.Machine.Val
          Effect4.Machine.Err Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann))
      Option.none →
    Eq (Effect4.Machine.RunMachine.finished m) Bool.false →
      Iff (Eq (Effect4.Api.frontierReasons Effect4.Machine.Exhaustion.tape m) List.nil)
        (Effect4.Api.Deadlocked m)

decision-keeps-typedclaim:decision-keeps-typed

M6b: one tape decision keeps J when its host answer, if any, is admitted

A tape decision keeps J (decision_preserves): the command facts and the six edits through the decision lift (decisionKeeps_of_ledger).

Module

Effect4.Laws.Program.Typed.Commands.Clauses.All

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy) (fuel : Nat)
  (d : Effect4.Api.Decision), Effect4.Program.Typed.DecisionKeeps root rootTy fuel d

fair-schedulingclaim:fair-scheduling

Progress under weak fairness

Literature

PFPL, chs. 39–41, pp. 371–406 (excludedFeature)

queue-step-capacityclaim:queue-step-capacity

One step of the Queue's abstract model under suspend keeps the capacity, the strategy and the buffer's bound (a helper of queue-expansion-agrees on its abstract client's side; lengths in the natural-number model, no delivery and no target; decisions rows 219, 233 and 255)

Abstract positive-capacity suspend steps keep the configuration and buffer bound. Consumer: the later Queue term-to-model refinement. No wrapper or host claim. The proof does not use _hpos.

Module

Effect4.Laws.Library.Queue.Capacity

∀ (c : Nat) (s : Effect4.Queue.Model.State) (op : Effect4.Queue.Model.Op),
  instLTNat.lt 0 c →
    Eq s.capacity (Option.some c) →
      Eq s.strategy Effect4.Queue.Model.Strategy.suspend →
        instLENat.le s.messages.length c →
          have next := (Effect4.Queue.Model.step Effect4.Queue.Model.Fault.none { s := s } op).s;
          And (Eq next.capacity (Option.some c))
            (And (Eq next.strategy Effect4.Queue.Model.Strategy.suspend)
              (instLENat.le next.messages.length c))

queue-first-profile-closedclaim:queue-first-profile-closed

Each first operation of the Queue's abstract model keeps the first profile, when its request keeps the step's premise (a helper of queue-expansion-agrees: the domain of the step goals; no agreement of a term with the model; decisions rows 219, 233 and 255)

The first profile is closed. Each first operation of the model leaves a state of the profile, when its request keeps the premise. Consumer: each step goal of the Queue's term-to-model refinement, along a run. No wrapper or host claim.

Module

Effect4.Laws.Library.Queue.Profile

∀ (s : Effect4.Queue.Model.State) (op : Effect4.Queue.Model.Op),
  Effect4.Queue.Model.FirstProfile s →
    Eq (Effect4.Queue.Model.firstOp op) Bool.true →
      Effect4.Queue.Model.Requested s op →
        Effect4.Queue.Model.FirstProfile
          (Effect4.Queue.Model.step Effect4.Queue.Model.Fault.none { s := s } op).s

semaphore-visit-selects-earliestclaim:semaphore-visit-selects-earliest

One visit of Semaphore's model selects the earliest fitting waiter at or after its cursor, and that waiter leaves (a helper of semaphore-expansion-agrees' waiting clauses; one visit, no walk and no liveness; decisions row 259)

A visit resumes the earliest fitting waiter at or after its cursor. On a profile state, the selected waiter is enrolled, its stamp is at or after the cursor, and its count fits the free count. Its stamp is the least among the waiters that are at or after the cursor and fit. The selected waiter leaves the list, and nothing else changes. Consumer: the waiting clauses of the proposed claim semaphore-expansion-agrees. It states one visit, and nothing about a whole walk.

Module

Effect4.Laws.Library.Semaphore.Profile

∀ {s : Effect4.Semaphore.Model.State},
  Effect4.Semaphore.Model.Profile s →
    ∀ {cursor : Nat} {w : Effect4.Semaphore.Model.Waiter},
      Eq (Effect4.Semaphore.Model.visit s cursor).snd (Option.some w) →
        And (List.instMembership.mem s.waiters w)
          (And (instLENat.le cursor w.stamp)
            (And (instLENat.le w.need (Effect4.Semaphore.Model.free s))
              (And
                (∀ (u : Effect4.Semaphore.Model.Waiter),
                  List.instMembership.mem s.waiters u →
                    instLENat.le cursor u.stamp →
                      instLENat.le u.need (Effect4.Semaphore.Model.free s) →
                        instLENat.le w.stamp u.stamp)
                (Eq (Effect4.Semaphore.Model.visit s cursor).fst
                  { permits := s.permits, taken := s.taken, waiters := s.waiters.erase w,
                    next := s.next }))))

semaphore-visit-stopsclaim:semaphore-visit-stops

One visit of Semaphore's model selects nobody exactly when no permit is free or no waiter at or after the cursor fits, and then it changes nothing (a helper of semaphore-expansion-agrees' waiting clauses; one visit, no walk and no liveness; decisions row 259)

A visit stops only when no permit is free or no such waiter fits. A visit selects nobody exactly when the free count is zero, or each waiter at or after the cursor needs more than the free count. It then changes nothing. Consumer: the waiting clauses of the proposed claim semaphore-expansion-agrees. It states one visit, and no liveness.

Module

Effect4.Laws.Library.Semaphore.Profile

∀ (s : Effect4.Semaphore.Model.State) (cursor : Nat),
  And
    (Iff (Eq (Effect4.Semaphore.Model.visit s cursor).snd Option.none)
      (Or (Eq (Effect4.Semaphore.Model.free s) 0)
        (∀ (u : Effect4.Semaphore.Model.Waiter),
          List.instMembership.mem s.waiters u →
            instLENat.le cursor u.stamp → instLTNat.lt (Effect4.Semaphore.Model.free s) u.need)))
    (Eq (Effect4.Semaphore.Model.visit s cursor).snd Option.none →
      Eq (Effect4.Semaphore.Model.visit s cursor).fst s)

queue-first-step-invariantclaim:queue-first-step-invariant

One step of a first operation of the Queue's abstract model keeps the run invariant of the first profile: the profile, the buffer's bound, tidy, quiet at the run's signalled, and the two flags (the model's half of wait-registration-no-gap and of waiting-request-obligation-preserved; no program, no delivery of a signal and no liveness; decisions rows 219, 233, 255 and 275)

One step of a first operation keeps the run invariant. From every run of the invariant, the model's step by a first operation whose request keeps Requested leaves a run of the invariant. So the step keeps both flags. After it no taker stands ready without a signal. Each request that waited still waits, is the step's own, or is named by a signal.

It is the model's half of wait-registration-no-gap and of waiting-request-obligation-preserved. Consumer: first_run_inv, and then the run-level law of the Queue's wrapper. The statement is of the model alone: no program, no delivery of a signal, no liveness and no fairness.

Module

Effect4.Laws.Library.Queue.Invariant

∀ (r : Effect4.Queue.Model.Run) (op : Effect4.Queue.Model.Op),
  Effect4.Queue.Model.FirstRunInv r →
    Eq (Effect4.Queue.Model.firstOp op) Bool.true →
      Effect4.Queue.Model.Requested r.s op →
        Effect4.Queue.Model.FirstRunInv
          (Effect4.Queue.Model.step Effect4.Queue.Model.Fault.none r op)

queue-first-run-flagsclaim:queue-first-run-flags

From the empty queue of a positive capacity both flags of the Queue's abstract model hold after every list of first operations whose requests keep their premises at each prefix (the bounded exploration's two flags at every length, on the first profile; decisions rows 219, 233, 255 and 275)

From the empty queue both flags hold after every list of first operations. The model's bounded exploration holds both flags to a fixed depth, over more operations. This statement holds them at every length, on the first profile. Consumer: the run-level law of the Queue's wrapper. It says nothing of close or shutdown, and nothing of a delivery.

Module

Effect4.Laws.Library.Queue.Invariant

∀ (c : Nat) (ops : List Effect4.Queue.Model.Op),
  Effect4.Queue.Model.FirstOps { s := { capacity := Option.some (instHAdd.hAdd c 1) } } ops →
    And
      (Eq
        (List.foldl (Effect4.Queue.Model.step Effect4.Queue.Model.Fault.none)
            { s := { capacity := Option.some (instHAdd.hAdd c 1) } } ops).ok
        Bool.true)
      (Eq
        (List.foldl (Effect4.Queue.Model.step Effect4.Queue.Model.Fault.none)
            { s := { capacity := Option.some (instHAdd.hAdd c 1) } } ops).named
        Bool.true)

pool-select-takes-firstclaim:pool-select-takes-first

One selection of Pool's model takes the first waiters of the state that it finds, at most its count, and it changes the waiters alone (a helper of pool-wake-selection; one selection, no run and no liveness)

A selection takes the first waiters of the state that it finds, at most its count, and exactly those. The selected identities are a prefix of the waiters, in the order of enrolment. They are as many as the count, or every waiter where fewer wait. They leave the list, and nothing else changes: a wake reserves nothing. Consumer: the proposed claim pool-wake-selection. It states one selection, and nothing about a run.

Module

Effect4.Laws.Library.Pool.Profile

∀ (s : Effect4.Pool.Model.State) (count : Nat),
  And
    (Eq
      (instHAppendOfAppend.hAppend (Effect4.Pool.Model.select s count).snd
        (Effect4.Pool.Model.select s count).fst.waiters)
      s.waiters)
    (And (Eq (Effect4.Pool.Model.select s count).snd.length (instMinNat.min count s.waiters.length))
      (Eq (Effect4.Pool.Model.select s count).fst
        { items := s.items, available := s.available, waiters := List.drop count s.waiters,
          closing := s.closing, next := s.next }))