Translation & Simulationconcept:translation-simulation

recorded-call-tree-prefixclaim:recorded-call-tree-prefix

Each recorded call binding on StraightRows without cause handlers names a wait in the admitted call tree, using replies submitted in that run; arbitrary command budget, no progress

Every accepted call binding names a wait in the admitted call tree. The tape contains only exits carried by submitted replies in this run. This is the command-prefix connection consumed by the original routing clause.

Module

Effect4.Laws.Run.CallTree

∀ (s : Effect4.Run),
  s.Reached →
    Eq (Effect4.Program.Denote.StraightRows s.built.table s.built.program) Bool.true →
      Eq (Effect4.Run.CallTree.NoCauseHandler s.built.program) Bool.true →
        Effect4.Program.SourceScope.ExternalOnly s.built.program →
          Effect4.Program.SourceScope.ConcreteReplies s.built.table →
            ∀ (call : Effect4.Api.HostSession.Call) (token : Nat),
              List.instMembership.mem (s.journal.zip s.phases)
                  { fst := Effect4.Api.Runner.Command.bind call token,
                    snd := Effect4.Api.HostSession.Phase.bound } →
                Exists fun i =>
                  Exists fun row =>
                    Exists fun T =>
                      And (Eq call.op (Effect4.Program.NativeOp.external i))
                        (And (Eq (Effect4.Program.externalRow s.built.table i) (Option.some row))
                          (And
                            (∀ (ex : Effect4.Machine.ExitV),
                              List.instMembership.mem T ex →
                                Exists fun reply =>
                                  And
                                    (List.instMembership.mem s.journal
                                      (Effect4.Api.Runner.Command.submit reply))
                                    (Eq reply.completion (Effect4.Machine.Completion.ofExit ex)))
                            (Eq (Effect4.Run.CallTree.treeWaits s.built.table s.built.program T)
                              (Effect4.Program.Denote.RowsStop.waiting i call.request))))

run-eq-meaningclaim:run-eq-meaning

Frame machine execution matches denotational meaning on Straight fragment

The ordinary run of a straight-line program, with fuel for its depth and its commands, finishes with the exit and the stores of its meaning — under the op budget or past it, where the root yields, parks, and flush fires its dispatcher round after round (E4-DEN-CE-005, repaired). The trace is not pinned (E4-DEN-CE-003).

Module

Effect4.Laws.Program.Agreement.Segment

Literature

Leroy2009, audit C10 (analogy)

∀ (e : Effect4.Program.NativeEff) (fuel : Nat),
  Eq (Effect4.Program.Denote.Straight e) Bool.true →
    instLENat.le (Effect4.Program.Agreement.depth e) fuel →
      instLENat.le (instHAdd.hAdd (instHMul.hMul 2 (Effect4.Program.Agreement.steps e)) 6) fuel →
        And (Eq (Effect4.Api.run e fuel).outcome Effect4.Api.Outcome.finished)
          (And
            (Eq (Effect4.Api.run e fuel).exit
              (Option.some
                (Effect4.Program.Denote.meaning e List.nil Effect4.Machine.Stores.empty).fst))
            (Eq (Effect4.Api.run e fuel).stores
              (Effect4.Program.Denote.meaning e List.nil Effect4.Machine.Stores.empty).snd))

loop-agreementclaim:loop-agreement

Loop agreement on the loop-bearing fragment (Looped)

The loop agreement (O12, S8a-L). For every program of the loop-bearing fragment: when its budgeted meaning finishes at a budget k, the machine's ordinary run finishes with that exit and those stores at every fuel past a bound. The bound is the compile depth and twice the local step bound at k; by meaningB_unique the answer does not depend on the budget that found it.

Module

Effect4.Laws.Program.Agreement.Loop

∀ (e : Effect4.Program.NativeEff),
  Eq (Effect4.Program.Denote.Looped e) Bool.true → Effect4.Program.Agreement.LoopAgreement e

run-eq-refclaim:run-eq-ref

Frame machine replay matches term reference replay at empty host table

run_eq_ref. The frame machine's replay and the term reference's replay of the same program, at the same compile and command budget, on the same Completion tape, end the same way and observe the same thing: every fiber's exit and the whole stores. No premise: the relation is inhabited at the load and preserved by every command. Nothing is said about an external host.

At the empty table (DI-57). Api.replay takes a RowTable; this theorem takes none, so it stays at its default, the empty table. The reference takes the row table too (interpR, replayR), and the agreement at every row table is run_eq_ref_table (Laws/Program/Table/Agreement.lean, decisions row 314).

Module

Effect4.Laws.Program.RuntimeR

Literature

LynchVaandrager1995, audit C4 (proofTechnique)

∀ (e : Effect4.Program.NativeEff) (fuel : Nat) (tape : List Effect4.Api.Decision),
  And
    (Eq (Effect4.Api.replay e fuel tape).outcome
      (Effect4.Program.Sched.classify (Effect4.Program.Sched.replayR e fuel tape)))
    (Eq (Effect4.Machine.obs (Effect4.Api.replay e fuel tape).machine)
      (Effect4.Program.Sched.obsR
        (Effect4.Machine.ReplayResult.machine (Effect4.Program.Sched.replayR e fuel tape))))

profile-plus-exactclaim:profile-plus-exact

The checked integer addition answers exactly when the reference addition answers inside the profile, for two arguments inside it: a face equals the reference inside its profile and refuses outside it (DI-56), for the one operation that grows; nothing about the OCaml row or the TypeScript helper, each a trusted row run by a control (decisions rows 108 and 321)

The checked row answers exactly when the reference row answers inside the profile. Premise: both arguments are inside it.

Module

Effect4.Laws.Machine.IntegerProfile

∀ (bound : Nat) (x y v : Effect4.Machine.Val),
  Eq (Effect4.Program.Within bound x) Bool.true →
    Eq (Effect4.Program.Within bound y) Bool.true →
      Iff (Eq (Effect4.Program.intAddIn bound x y) (Option.some v))
        (And (Eq (Effect4.Program.intAdd x y) (Option.some v))
          (Eq (Effect4.Program.Within bound v) Bool.true))

profile-mul-exactclaim:profile-mul-exact

The checked natural multiplication answers exactly for the represented atom product inside the supplied bound; target rows remain trusted implementations with finite controls (DI-56)

The represented natural multiplication uses exactly the checked product judgment. Claim: profile-mul-exact, translation-simulation R8. Target execution remains a separate control.

Module

Effect4.Laws.Machine.IntegerProfile

∀ (bound a b n : Nat),
  Iff (Eq (Effect4.Program.scaleIn bound a b) (Option.some n))
    (And
      (Eq
        (Effect4.Program.NativeAtom.mul.eval
          (List.cons (Effect4.Store.Val.nat a) (List.cons (Effect4.Store.Val.nat b) List.nil)))
        (Option.some (Effect4.Store.Val.nat n)))
      (Eq (Effect4.Program.Within bound (Effect4.Store.Val.nat n)) Bool.true))

rows-denotation-straightclaim:rows-denotation-straight

The call tree over the stores and the host rows extends denote: on Straight it is denote's tree injected on the left of the coproduct (DI-69; the fragment StraightRows admits catchIf, decisions row 310)

On Straight the tree is denote's tree, injected on the left. The connector of the two denotations: denote is denoteRows at no host call.

Module

Effect4.Laws.Program.DenoteRows

∀ (table : Effect4.Program.RowTable) (e : Effect4.Program.NativeEff)
  (env : List Effect4.Machine.Val),
  Eq (Effect4.Program.Denote.Straight e) Bool.true →
    Eq (Effect4.Program.Denote.denoteRows table e env) (Effect4.Program.Denote.denote e env).inl

rows-denotation-appendclaim:rows-denotation-append

C2 of DB-01 for host rows, on StraightRows: the meaning of an old program under a host of an appended row table is its meaning under that host restricted to its own rows (nothing outside the fragment, where C2 stays operational; decisions row 310)

C2 for host rows, on the fragment: the meaning of an old program under a host of an appended table is its meaning under that host's restriction to its own table.

Module

Effect4.Laws.Program.DenoteRowsAppend

∀ {σ : Type} (table ext : Effect4.Program.RowTable)
  (host :
    Effects.Handler (Effect4.Program.Denote.RowSig (instHAppendOfAppend.hAppend table ext))
      (StateT σ Option))
  (e : Effect4.Program.NativeEff) (env : List Effect4.Machine.Val) (s : Effect4.Machine.Stores)
  (state : σ),
  Eq (Effect4.Program.Denote.StraightRows table e) Bool.true →
    Eq (Effect4.Program.Denote.meaningUnder host e env s state)
      (Effect4.Program.Denote.meaningUnder (Effect4.Program.Denote.restrictRows table ext host) e
        env s state)

rows-denotation-referenceclaim:rows-denotation-reference

The reference machine's term of a StraightRows program, its control markers erased, is the program's call tree read into the reference machine's signature, when the compile budget covers the program's depth (a step of rows-denotation-session on the reference route; decisions row 310)

The reference's term of a program of the fragment, with its control markers erased, is the program's tree over the stores and the rows, when the compile budget covers its depth. It extends denoteR_straight by the one arm of a host call.

Module

Effect4.Laws.Program.DenoteRowsR

∀ (root : Effect4.Program.NativeEff) (table : Effect4.Program.RowTable)
  (e : Effect4.Program.NativeEff) (p : Effect4.Program.Point),
  Eq (Effect4.Program.Denote.StraightRows table e) Bool.true →
    instLENat.le (Effect4.Program.Sched.depthRows e) p.fuel →
      Eq (Effect4.Program.Sched.eraseControl (Effect4.Program.Sched.denoteR root e p))
        (Effects.interpret (Effect4.Program.Sched.toRef table)
          (Effect4.Program.Denote.denoteRows table e p.env))

run-eq-ref-tableclaim:run-eq-ref-table

The frame machine and the reference machine agree at every row table: on every program, decision tape and pair of budgets, the same class and the same observation obs (no premise on the tape; a host answer reaches either machine only as a decision, DI-23; nothing of reply admission, reply typing, a host's conformance or the session's ledger; DI-57, decisions rows 310 and 314)

The frame machine and the reference machine agree at every row table (DI-57). On every program, row table, decision tape and pair of budgets, the two replays end in the same class, and they have the same observation obs: every fiber's exit and the whole stores, the external allocations included. It is Machine.Book's replay theorem at the two instances at the table: stepAgrees and hooksAgree_of hold at every row table under the store invariant StoresOk, whose clause externals holds at the empty row table alone; the registration arm answers nothing on both machines, since a host answer is a decision (DI-23). Reach: no premise on the tape, so an answer that no session admits is in reach. It does not establish reply admission, the typing of a reply, a host's conformance or the session's ledger. run_eq_ref is its instance at the empty row table. Concept translation-simulation, claim run-eq-ref-table, role simulation; requirement R6. Consumer: session_eq_ref.

Module

Effect4.Laws.Program.Table.Agreement

Effect4.Program.Sched.RunEqRefTable

session-eq-refclaim:session-eq-ref

A session's reading is the reference machine's replay of the run's own tape: for a recorded, funded run, the same class and the same observation (proved by session_eq_ref_of_raw from run_eq_ref_table; nothing about a run with a stopped row, the session's ledger or reply admission; DI-57, decisions rows 310 and 314)

A session's reading is the reference machine's replay of the run's tape (DI-57). For a recorded run that is funded, the session's class and observation are the class and observation of the reference machine's replay of the run's own tape, at the run's row table and budgets. Reach: any built program and any journal, under funded: no row of the journal is a stopped row. It does not establish that a run is funded, the session's ledger, reply admission or a host's conformance. A run with a stopped row is outside it: the control is three calls at a command budget of 5. It is proved by session_eq_ref_of_raw from run_eq_ref_table (slice H6a), so it rests on no planned goal. Concept translation-simulation, claim session-eq-ref, role simulation; requirement R6. Consumer: the typed session (decisions row 99), and the meaning of a run's certificate.

Module

Effect4.Laws.Api.SessionRef

Effect4.Program.Sched.SessionEqRef

rows-denotation-sessionclaim:rows-denotation-session

The meaning of a StraightRows program under a run's reply tape is the root's exit with the stores, or the frontier: for a recorded run that is funded, at rest and driven by a host (one fiber; nothing about an interruption, a clock step, a delayed cell read or a handle row; DI-69, decisions row 310)

The meaning under a run's reply tape is the run's observation (DI-69). For a recorded run of a program of the fragment, the meaning of the program under the run's reply tape is the root's exit with the stores, and the reply tape is read to its end. Where the root has no exit, the meaning is the frontier. Reach: StraightRows, one fiber, every compile budget; a run that is funded, at rest and driven by a host: its controls evaluate the root or flush, and each reply holds an exit. It does not establish the same for a run with an interruption, a clock step, a delayed cell read or a handle row: each has a red control. It says nothing of a fiber, a scope or a loop. Concept translation-simulation, claim rows-denotation-session, role simulation; requirement R6. Consumer: a fact of a program's call tree, read on a run.

The proof (slice H8): the session's tape is answered (tapeFrom_answered); each decision keeps the machine in a settled form whose position the local run with calls reaches (tape_holds); a machine at rest is exited or waits on a call; and there the meaning is what the local run says (meaning_settled), the compile's frontier being a divergence that rest excludes.

Module

Effect4.Laws.Api.SessionMeaning

Effect4.Run.DenoteRowsEqSession Effect4.Program.Denote.StraightRows

rows-denotation-hostclaim:rows-denotation-host

H9, the host as a handler: for a recorded StraightRows run that is funded, at rest, driven by a host and finished, under any host (a comodel of the row signature) whose answers are the run's, the host's run of the call tree is the root's exit with the stores and the host ends where the answers left it (one fiber; no progress claim; nothing about a run stopped at a call, an interruption, a clock step or a handle row; decisions row 310; the coalgebra note, slice CO-5)

H9: the host as a handler. For a recorded run of a program of the fragment that is funded, at rest, driven by a host, and whose root exited: under any host whose answers are the run's (HostAnswered), the run of the program's call tree under that host is the root's exit with the stores, and the host ends at the state the run's answers left it in. The reply host is one host: H8. Reach: StraightRows, one fiber, every compile budget, finished runs. It does not establish that a host's drive finishes (progress), nor anything of a run that stopped at a call, an interruption, a clock step or a handle row. Concept translation-simulation, role simulation; requirement R6. Consumer: host utilities composed with Effects.Comodel's constructions (docs/research/2026-10-09-host-coalgebra.md, slice CO-5).

Module

Effect4.Laws.Api.SessionMeaning

Effect4.Run.DenoteRowsEqSessionHost Effect4.Program.Denote.StraightRows

rows-loop-sessionclaim:rows-loop-session

H8 on loops: for a recorded run of a LoopedRows program the row fragment with loops admits (LoopedDataRows), funded, at rest and driven by a host, past a budget bound the coarse observation of the budgeted meaning under the run's reply tape is the root's exit with the stores, or none (one fiber; no global compile-depth premise; a budget cut is no failure and no divergence; nothing of a waiting position's stores or request, a scope, a handle allocation, a fork or an interruption; the host-meaning widening, slice L1)

H8 on loops (Q7): for a recorded run of a program of the row fragment with loops that is funded, at rest and driven by a host, past a budget bound the coarse observation of the budgeted meaning under the run's reply tape is the root's exit with the stores, the tape read to its end; where the root has no exit it is none. Concept translation-simulation, claim rows-loop-session, role simulation; requirement R6. Consumers: the paged data-row client and the driver theorem on loops. It establishes no scope, external handle allocation, interruption, fork, progress or target claim, and no waiting position's stores or request.

Module

Effect4.Laws.Api.SessionMeaningLoop

Effect4.Run.H8LoopedRows

rows-loop-hostclaim:rows-loop-host

H9 on loops: for a finished recorded run of the same fragment, under any host whose answers are the run's, past a budget bound the budgeted meaning under the host is the root's exit with the stores and the host ends where the answers left it (no progress claim; nothing of a run stopped at a call; the host-meaning widening, slice L1)

H9 on loops (Q8): for a finished recorded run of the same fragment, under any host whose answers are the run's (HostAnswered), past a budget bound the budgeted meaning under the host is the root's exit with the stores, and the host ends where the answers left it. H8 on loops at a finished run is its instance at the reply host. Concept translation-simulation, claim rows-loop-host, role simulation; requirement R6. Consumer: the driver theorem on loops (Q9). It does not establish that a host's drive finishes, nor anything of a run that stopped at a call.

Module

Effect4.Laws.Api.SessionMeaningLoop

Effect4.Run.H9LoopedRows

rows-loop-driverclaim:rows-loop-driver

H9 at the driver on loops: open a LoopedRows program the row fragment with loops admits, evaluate its root and drive it with a reactor inside the envelope that answers with exits (Run.runWith); when the run is funded, at rest and its root exited, past a budget bound the reactor read as a host runs the budgeted call tree to the root's exit with the stores and ends at the drive's state (no progress claim; the host-meaning widening, Q9)

H9 at the driver, on loops (Q9): open a program of the row fragment with loops, evaluate its root and drive it with a reactor inside the envelope that answers with exits. When the run is funded, at rest and its root exited, past a budget bound the reactor read as a host runs the budgeted call tree to the root's exit with the run's stores, and ends at the drive's state. runWith_denotes with H9 on loops in place of H9. It does not establish that the drive finishes, that its rounds suffice, or that the run is funded. Concept translation-simulation, claim rows-loop-driver, role simulation; requirement R6. Consumer: the run interface's hosts on stream and paging modules.

Module

Effect4.Laws.Api.SessionMeaningLoop

∀ {σ : Type} (b : Effect4.Api.Built) (r : Effect4.Run.Reactor σ) (st : σ) (id : String)
  (budget : Effect4.Api.Budget) (rounds : Nat),
  r.Envelops b.table →
    r.ExitsOnly →
      Eq (Effect4.Program.Denote.LoopedRows b.program) Bool.true →
        Eq (Effect4.Program.Denote.LoopedDataRows b.table b.program) Bool.true →
          Eq (Effect4.Run.runWith b r st id budget rounds).fst.funded Bool.true →
            Eq (Effect4.Run.runWith b r st id budget rounds).fst.atRest Bool.true →
              ∀ (ex : Effect4.Machine.ExitV),
                Eq (Effect4.Run.runWith b r st id budget rounds).fst.exit (Option.some ex) →
                  Exists fun lower =>
                    ∀ (k : Nat),
                      instLENat.le lower k →
                        Eq
                          (Effect4.Program.Denote.hostRunB (Effect4.Run.reactorHost b.table r) k
                            b.program List.nil Effect4.Machine.Stores.empty st)
                          (Option.some
                            { fst := Option.some ex,
                              snd :=
                                {
                                  fst :=
                                    (Effect4.Run.runWith b r st id budget rounds).fst.machine.state
                                      (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),
                                  snd := (Effect4.Run.runWith b r st id budget rounds).snd } })

rows-loop-straightclaim:rows-loop-straight

The budgeted row meaning extends the row meaning: on StraightRows it is denoteRows finished, at every budget (the host-meaning widening, Q1)

On StraightRows the budgeted meaning is denoteRows, finished (Q1, the conservative connector): no budget is read. Each arm is thenOpt_map_some and the induction. Claim rows-loop-straight.

Module

Effect4.Laws.Program.DenoteRowsB

∀ (table : Effect4.Program.RowTable) (k : Nat) (e : Effect4.Program.NativeEff)
  (env : List Effect4.Machine.Val),
  Eq (Effect4.Program.Denote.StraightRows table e) Bool.true →
    Eq (Effect4.Program.Denote.denoteRowsB table k e env)
      (Effects.Program.instMonad.map Option.some (Effect4.Program.Denote.denoteRows table e env))

rows-loop-loopedclaim:rows-loop-looped

The budgeted row meaning extends the loop meaning: on Looped it is denoteB injected on the left of the coproduct, at the same budget (the host-meaning widening, Q1)

On Looped the budgeted meaning is denoteB, injected on the left (Q1): a host-free loop calls no row. The left injection commutes with each arm (inl_thenOpt, inl_iter, inl_loopStep), and a leaf is denoteRows_straight. Claim rows-loop-looped.

Module

Effect4.Laws.Program.DenoteRowsB

∀ (table : Effect4.Program.RowTable) (k : Nat) (e : Effect4.Program.NativeEff)
  (env : List Effect4.Machine.Val),
  Eq (Effect4.Program.Denote.Looped e) Bool.true →
    Eq (Effect4.Program.Denote.denoteRowsB table k e env)
      (Effect4.Program.Denote.denoteB k e env).inl

rows-denotation-driverclaim:rows-denotation-driver

H9 at the driver: open a StraightRows program, evaluate its root and drive it with a reactor inside the envelope that answers with exits (Run.runWith); when the run is funded, at rest and its root exited, the reactor read as a host runs the call tree to the root's exit with the stores and ends at the drive's state (one fiber; no progress claim: nothing shows that the drive finishes, that its rounds suffice or that the run is funded; the coalgebra note, slice CO-6)

H9 at the driver: the reactor's run of the call tree is the driver's. Open a program of the fragment, evaluate its root and drive it with a reactor inside the envelope that answers with exits. When the run is funded, at rest and its root exited, the reactor read as a host runs the program's call tree to the root's exit with the run's stores, and ends at the drive's state. Reach: StraightRows, one fiber, a reactor inside the envelope that answers with exits. It does not establish that the drive finishes, that its rounds suffice, or that the run is funded. Concept translation-simulation, role simulation; requirement R6. Consumer: the run interface's hosts, composed by Effects.Comodel (slice CO-6).

Module

Effect4.Laws.Api.HostDrive

∀ {σ : Type} (b : Effect4.Api.Built) (r : Effect4.Run.Reactor σ) (st : σ) (id : String)
  (budget : Effect4.Api.Budget) (rounds : Nat),
  r.Envelops b.table →
    r.ExitsOnly →
      Eq (Effect4.Program.Denote.StraightRows b.table b.program) Bool.true →
        Eq (Effect4.Run.runWith b r st id budget rounds).fst.funded Bool.true →
          Eq (Effect4.Run.runWith b r st id budget rounds).fst.atRest Bool.true →
            ∀ (ex : Effect4.Machine.ExitV),
              Eq (Effect4.Run.runWith b r st id budget rounds).fst.exit (Option.some ex) →
                Eq
                  (Effect4.Program.Denote.hostRun (Effect4.Run.reactorHost b.table r) b.program
                    List.nil Effect4.Machine.Stores.empty st)
                  (Option.some
                    { fst := ex,
                      snd :=
                        {
                          fst :=
                            (Effect4.Run.runWith b r st id budget rounds).fst.machine.state
                              (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),
                          snd := (Effect4.Run.runWith b r st id budget rounds).snd } })

m7-routeclaim:m7-route

M7 conditional route: typed exits and stores from ledger hypotheses M5 and M6

M7 from the ledger (decisions row 138's route): loadsTyped and decision_preserves at one source and budget give M7a–c at every answer-free tape.

Module

Effect4.Laws.Program.Typed.Assembly

Literature

WrightFelleisen1994, audit P36 (analogy)

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy) (fuel : Nat)
  (tape : List Effect4.Api.Decision),
  Effect4.Program.Typed.LoadsTyped root rootTy fuel fuel →
    (∀ (d : Effect4.Api.Decision), Effect4.Program.Typed.DecisionKeeps root rootTy fuel d) →
      And (Effect4.Program.Typed.M7Exits root rootTy fuel tape)
        (And (Effect4.Program.Typed.M7Stores root rootTy fuel tape)
          (Effect4.Program.Typed.M7NoHalt root rootTy fuel tape))

m7-exits-typedclaim:m7-exits-typed

M7a: every exit the observation records fits its fiber's declared type on M7Fragment

M7a–c (decisions row 138): on the M7 fragment (the empty host table, a checked closed source, answer-free tapes), the frame machine's observation is typed and its run never halts: m7_of_ledger at the proved load (loadsTyped) and decisions (decision_preserves). The frame machine only: not the OCaml engine, not a TypeScript run.

Module

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

Literature

WrightFelleisen1994, audit P36 (analogy)

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy) (fuel : Nat)
  (tape : List Effect4.Api.Decision),
  And (Effect4.Program.Typed.M7Exits root rootTy fuel tape)
    (And (Effect4.Program.Typed.M7Stores root rootTy fuel tape)
      (Effect4.Program.Typed.M7NoHalt root rootTy fuel tape))

m7-stores-typedclaim:m7-stores-typed

M7b: the observed stores fit at a world that describes them on M7Fragment

M7a–c (decisions row 138): on the M7 fragment (the empty host table, a checked closed source, answer-free tapes), the frame machine's observation is typed and its run never halts: m7_of_ledger at the proved load (loadsTyped) and decisions (decision_preserves). The frame machine only: not the OCaml engine, not a TypeScript run.

Module

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

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy) (fuel : Nat)
  (tape : List Effect4.Api.Decision),
  And (Effect4.Program.Typed.M7Exits root rootTy fuel tape)
    (And (Effect4.Program.Typed.M7Stores root rootTy fuel tape)
      (Effect4.Program.Typed.M7NoHalt root rootTy fuel tape))

m7-never-haltsclaim:m7-never-halts

M7c: the frame machine never halts on M7Fragment (row 139's stuck = none in J)

M7a–c (decisions row 138): on the M7 fragment (the empty host table, a checked closed source, answer-free tapes), the frame machine's observation is typed and its run never halts: m7_of_ledger at the proved load (loadsTyped) and decisions (decision_preserves). The frame machine only: not the OCaml engine, not a TypeScript run.

Module

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

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy) (fuel : Nat)
  (tape : List Effect4.Api.Decision),
  And (Effect4.Program.Typed.M7Exits root rootTy fuel tape)
    (And (Effect4.Program.Typed.M7Stores root rootTy fuel tape)
      (Effect4.Program.Typed.M7NoHalt root rootTy fuel tape))

m7-admittedclaim:m7-admitted

M7a–c for a program the API admits at the empty row table, with a closed requirement row and an answer-free tape

M7 for a program the API admits at an empty row table (R9 at the API's admission, within M7Fragment): with a closed requirement row and an answer-free tape, its replay's exits fit, its stores fit, and the frame machine has not halted. The services may be declared.

Module

Effect4.Laws.Program.Typed.AdmittedSource

∀ {program : Effect4.Program.NativeEff} {app : Effect4.Program.SigApp}
  (a : Effect4.Program.AdmittedProgram program app),
  Eq app.rows List.nil →
    ∀ (fuel : Nat) (tape : List Effect4.Api.Decision),
      Eq a.ty.requires Effect4.Machine.Env.Requirement.empty →
        (∀ (d : Effect4.Api.Decision),
            List.instMembership.mem tape d → Effect4.Program.Typed.NoHostAnswer d) →
          And (Effect4.Program.Typed.M7Exits a.source a.ty fuel tape)
            (And (Effect4.Program.Typed.M7Stores a.source a.ty fuel tape)
              (Effect4.Program.Typed.M7NoHalt a.source a.ty fuel tape))

m7-exit-handles-validclaim:m7-exit-handles-valid

Recorded exits name only live scope handles on every reachable machine (row 139)

Recorded successes name only live handles (exitHandles_valid, organization M4, row 139): on every reachable machine of a checked program, a fiber's successful exit value is valid in the machine's stores. J holds there (reachable_typed, with a closed root row), the exit fits its fiber's declared type, and a member of any type is valid in a typed store (fits_validIn, the F-WF repair). The exit connector's validity premise.

Module

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

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy) (fuel : Nat)
  (m : Effect4.Program.Sched.RState), Effect4.Program.Typed.ExitHandlesValid root rootTy fuel m

obs-typed-admittedclaim:obs-typed-admitted

The frame machine's observation on every ghost-admitted tape of a checked program is typed and the run has not halted

The frame machine's observation on every admitted tape is typed and its run has not halted: reachable_typed across run_eq_ref's relation (obsTyped_admitted). M7a–c without the fragment's lawful and answer-free premises; row 117's closed row remains; the frame machine at its empty row table only.

Module

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

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy) (fuel : Nat)
  (tape : List Effect4.Api.Decision),
  Eq (Effect4.Program.typeOfProgram root.sig.signature root.program) (Option.some rootTy) →
    Eq rootTy.requires Effect4.Machine.Env.Requirement.empty →
      Effect4.Program.Typed.AdmittedTape root rootTy fuel tape →
        Exists fun w =>
          And
            (Effect4.Program.Typed.MachineTyped root rootTy w
              (Effect4.Machine.ReplayResult.machine
                (Effect4.Program.Sched.replayR root.program fuel tape)))
            (And
              (Effect4.Program.Typed.ExitsFit rootTy w
                (Effect4.Machine.obs (Effect4.Api.replay root.program fuel tape).machine))
              (And
                (Effect4.Program.Typed.StoresFit root w
                  (Effect4.Machine.obs (Effect4.Api.replay root.program fuel tape).machine).stores)
                (Eq
                  ((Effect4.Api.replay root.program fuel tape).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)))

m7-results-exit-hastyclaim:m7-results-exit-hasty

Every recorded exit of a checked program's frame-machine run satisfies the meaning layer's exit judgment at its declared type (T1)

T1. Recorded exits have their declared type, in the meaning layer's judgment. On every admitted tape of a checked program, there is a declaration of the fibers, the root at the program's type, under which every exit the frame machine's observation records satisfies Denote.ExitHasTy at its fiber's type over the observed stores.

Module

Effect4.Laws.Program.Typed.Results

∀ (root : Effect4.Program.Typed.ProgramSource) (rootTy : Effect4.Program.EffTy) (fuel : Nat)
  (tape : List Effect4.Api.Decision),
  Eq (Effect4.Program.typeOfProgram root.sig.signature root.program) (Option.some rootTy) →
    Eq rootTy.requires Effect4.Machine.Env.Requirement.empty →
      Effect4.Program.Typed.AdmittedTape root rootTy fuel tape →
        Exists fun Γ =>
          And (Eq (Γ Effect4.Api.root) (Option.some rootTy))
            (∀ (id : Effect4.FiberId) (ex : Effect4.Machine.ExitV),
              List.instMembership.mem
                  (Effect4.Machine.obs (Effect4.Api.replay root.program fuel tape).machine).exits
                  { fst := id, snd := Option.some ex } →
                Exists fun ty =>
                  And (Eq (Γ id) (Option.some ty))
                    (Effect4.Program.Denote.ExitHasTy ty.answer ty.error
                      (Effect4.Machine.obs
                          (Effect4.Api.replay root.program fuel tape).machine).stores
                      ex))

replay-externalsclaim:replay-externals

No replay at the empty row table allocates an external handle

No replay allocates an external handle, on every tape, host answers included: the frame machine runs at the empty row table, where the external registration and the prepared answer fall back without minting (StoresOk.externals). The exit connector's allocation premise (exitHasTy_of_fitsExit).

Module

Effect4.Laws.Program.RuntimeR

∀ (e : Effect4.Program.NativeEff) (fuel : Nat) (tape : List Effect4.Api.Decision),
  Eq
    ((Effect4.Api.replay e fuel tape).machine.state
          (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)).externals.allocated
    List.nil

run-controls-replayclaim:run-controls-replay

Journaled control rows leave the raw replay's machine whenever every added phase progressed

Journaled control execution agrees with raw frame replay at the same machine, table and command budget when every added row progressed. The initial machine already fixes the compile budget. Earlier phases may include host answers, refusals or fuel frontiers.

This is machine equality, not equality of session metadata or an assertion that the program has finished. A refused row or an insufficient-budget row cannot satisfy the premise.

Module

Effect4.Laws.Run

∀ (s : Effect4.Run) (tape : List Effect4.Api.Decision),
  Eq (s.play (Effect4.Rows.tape tape)).phases
      (instHAppendOfAppend.hAppend s.phases
        (List.replicate tape.length Effect4.Api.HostSession.Phase.progressed)) →
    Eq (s.play (Effect4.Rows.tape tape)).machine
      (Effect4.Run.machineOf
        (Effect4.Run.replayFrom s.built.program s.built.table s.budget.fuel tape s.machine))

run-tape-replayclaim:run-tape-replay

A journal's machine is the raw replay of its tape: the controls that progressed and the reply applications, each as the decision the session hands the machine (machine equality for any run and any journal whose tape reads to its end; no session ledger, no journal that stops at a frontier, no lowered engine; decisions row 254)

A journal's machine is the raw replay of its tape. When the tape reads every row, the machine that the journal leaves is the machine that the raw frame replay leaves on the tape's decisions, at the same table and budgets. It is the machine clause of a lowered run: a replay of the machine alone needs the tape, not the session. Reach: any run, any rows whose tape reads to the end: no row at a frontier, and every decision taken at a live machine with enough fuel. It needs no premise on the session, because the tape holds the decision that the session hands the machine: a reply's own answer decision (replyDecision). It does not establish equal session ledgers: the raw replay has none. It does not reach a journal that stops at a frontier, and it says nothing of a lowered engine: that link is the finite comparison of ocaml/engine/test/scenarios/test_scenarios.ml. It extends play_controls_eq_replay (src/Effect4/Laws/Run.lean) from control rows to reply applications. Concept translation-simulation, R8. Consumer: the lowered runs of Test/Dogfood/Scenario/Lowered.lean, whose finite runs check it at every position of every fixture.

Module

Effect4.Laws.Run.Tape

Effect4.Run.TapeReplays

funded-run-replayclaim:funded-run-replay

The machine of a funded run is the raw replay of its tape's decisions, from the program's own load (any recorded run whose journal has no stopped row; nothing about a run with a stopped row, a session ledger or a generated engine; decisions rows 226 and 254)

The machine of a funded run is the raw replay of its tape's decisions. For a recorded run whose journal holds no stopped row, the machine is the machine that the raw frame replay leaves on the decisions of the run's tape, from the program's own load, at the run's table and budgets. Reach: any run that was opened and then played (Run.Reached), under funded. It is one application of tape_replays at the run's fresh open, with Run.journal_replays. It does not establish that a run is funded: that is the open claim embedded-budget-sufficient. It does not establish equal session ledgers, and it says nothing of a run with a stopped row. Concept translation-simulation, R8. Consumer: each statement over runs that takes funded as its budget premise, the planned goals of Test/Dogfood/Scenario/QueueWorkers.lean first.

Module

Effect4.Laws.Run.Tape

∀ (s : Effect4.Run),
  s.Reached →
    Eq s.funded Bool.true →
      Eq s.machine
        (Effect4.Run.machineOf
          (Effect4.Run.replayFrom s.built.program s.built.table s.budget.fuel s.tapeOf
            (Effect4.Api.load s.built.program s.budget.compileFuel)))

journal-position-replayclaim:journal-position-replay

The machine after a position of a journal's tape is the raw replay of the decisions up to it, from the run's own machine (any run, any rows and any position; nothing about a stopped row's machine, a session ledger or a generated engine)

The machine after a position is the raw replay of the decisions up to it. At position i of a journal's tape, the machine of the run after the position's row is the machine that the raw frame replay leaves on the first i + 1 decisions. The replay starts at the machine of the run that the tape was read from, at the same table and budgets. Reach: any run, any rows and any position of the tape. The tape need not read every row: a later stopped row adds no position. It does not establish the machine after a stopped row, equal session ledgers, or anything of a generated engine. It replays from the run's own machine: a replay from a new load needs a fresh open, which the consumer states. Concept translation-simulation, R13: it is tape_replays on the prefix that ends at the position's row. Consumer: shown_views_opened (Test/Dogfood/Scenario/Tape.lean), the views of a lowered run.

Module

Effect4.Laws.Run.Tape

∀ (s : Effect4.Run) (rows : List Effect4.Api.Runner.Command) (i : Nat)
  (position : Effect4.Run.Position),
  Eq (List.instGetElem?NatLtLength.getElem? (s.tapeFrom rows).fst i) (Option.some position) →
    Eq position.after.machine
      (Effect4.Run.machineOf
        (Effect4.Run.replayFrom s.built.program s.built.table s.budget.fuel
          (List.map (fun x => x.decision) (List.take (instHAdd.hAdd i 1) (s.tapeFrom rows).fst))
          s.machine))

pool-steps-agreeclaim:pool-steps-agree

Each of Pool's six step terms agrees with the abstract model's step on every model state, through an encoding table that is injective for the lease, the withdrawal and the closer's step: the reply, the stored value through the encoding table, and the selected waiters' records (a part of pool-expansion-agrees; the sixth is the closer's step of decisions row 276, point 2; no order of the wake across helpers, no cancellation law, no wait of the close along a run, no liveness, no wrapper and no host; decisions rows 267 to 269 and 276)

The six step statements hold (the claim pool-steps-agree, a part of the proposed claim pool-expansion-agrees). Each field is one statement of this file. It establishes no order of the wake across helpers, no cancellation law, no liveness, no wait of the close along a run and nothing of a wrapper. Its consumer is the attempt laws of the public operations (src/Effect4/Laws/Library/Pool/Ops.lean), and then the law of a run.

Module

Effect4.Laws.Library.Pool.Steps

Effect4.Pool.Model.StepsAgree

queue-steps-agreeclaim:queue-steps-agree

Each of the Queue's six step terms agrees with the abstract model's step on the first profile: the reply, the stored value through the encoding table, and the ordered signals (a part of queue-expansion-agrees; no delivery, no cancellation law, no liveness, no wrapper and no host; decisions row 255)

The six step statements hold (the proposed claim queue-steps-agree, a part of queue-expansion-agrees). Each field is one theorem of this file. It establishes no delivery, no cancellation law, no liveness and nothing of a wrapper. Its consumer is the wrapper's law, in the public path's slice.

Module

Effect4.Laws.Library.Queue.Steps

Effect4.Queue.Model.StepsAgree

semaphore-steps-agreeclaim:semaphore-steps-agree

Each of Semaphore's five step terms agrees with the abstract model's step on every model state: the reply, the stored value through the encoding table, and the selected waiter's record (a part of semaphore-expansion-agrees; no order of the wake across visits, no cancellation law, no liveness, no wrapper and no host; decisions rows 259 to 261 and 265)

The five step statements hold (the proposed claim semaphore-steps-agree, a part of semaphore-expansion-agrees). Each field is one statement of this file. It establishes no order of the wake across visits, no cancellation law, no liveness and nothing of a wrapper. Its consumer is the public law, in the slice of the operations that wait.

Module

Effect4.Laws.Library.Semaphore.Steps

Effect4.Semaphore.Model.StepsAgree

straight-composition-agreementclaim:straight-composition-agreement

StraightEq programs run to equal exits and stores at their own sufficient budgets (the straight-fragment composition relation)

Runtime consumer of straight-fragment composition. Budgets may differ: a rewrite can change its step bound. The observation includes state retained after failure/finalization; trace equality and insufficient-budget executions are outside this statement.

Module

Effect4.Laws.Program.MeaningEq

∀ {a b : Effect4.Program.NativeEff},
  Effect4.Program.Denote.StraightEq a b →
    ∀ (fa fb : Nat),
      instLENat.le (Effect4.Program.Agreement.depth a) fa →
        instLENat.le (instHAdd.hAdd (instHMul.hMul 2 (Effect4.Program.Agreement.steps a)) 6) fa →
          instLENat.le (Effect4.Program.Agreement.depth b) fb →
            instLENat.le (instHAdd.hAdd (instHMul.hMul 2 (Effect4.Program.Agreement.steps b)) 6)
                fb →
              And (Eq (Effect4.Api.run a fa).outcome Effect4.Api.Outcome.finished)
                (And (Eq (Effect4.Api.run b fb).outcome Effect4.Api.Outcome.finished)
                  (And (Eq (Effect4.Api.run a fa).exit (Effect4.Api.run b fb).exit)
                    (Eq (Effect4.Api.run a fa).stores (Effect4.Api.run b fb).stores)))

mask-printed-form-profileclaim:mask-printed-form-profile

The mask as a derived form, the getter bound to its body under uninterruptible: the surface's builder is that expansion; it types as its body under the saved state's binder, and a restore site of any other saved term has no type; it is readable exactly when its body is, so it prints and reads back; inside the getter the fiber is masked and a pending cause fails it at the getter's restoring frame, and after that frame an interruptible caller is interruptible until the body's mask (decisions rows 245, 246; no equality with the native spelling and no agreement with a release)

The printed form's profile (the claim mask-printed-form-profile; concept translation-simulation, requirements R10 and R11; decisions rows 245 and 246).

Reach: the checker at any signature; program syntax at any lawful spelling; the frame machine at any interpreter, machine and fiber. The two checkpoints are stated as steps and frame passes of the machine, from saved_mask_restoration.

It does not establish equality with the native spelling, and it states no agreement with a named release: that the compiled form and the pin's printed form answer one observation is a finite check (harness/truth/Truth.lean, pMaskWait and pMaskedRestore), and the cuts at the two checkpoints on the pin are Codex's runs. That the form spends three operations more than the native mask is measured, not proved (Test/Program/MaskContract.lean, S8). The form's contract has one premise for its clients: nothing is acquired or registered before the body begins. Under it an interrupt at either checkpoint equals an interrupt before the form.

Its consumers are the Queue's waiting wrapper and the Semaphore's protected permit, whose first step is inside the body.

Module

Effect4.Laws.Codegen.Mask

Effect4.Program.MaskFormProfile

step-language-soundclaim:step-language-sound

A stored step translates to a term reading its carrier value from caller terms reading the input encodings and canonical record names; folds require aligned caller value and source scope lengths, and deferred comparisons require DeferredIdentity at the carrier interpretation; captured sources resolve at their original scope; each module separately proves its value equation against an independent model; no optional field, allocation, wrapper, run or host behavior follows (decisions row 330)

The reading law, with scope alignment only when a fold occurs.

Module

Effect4.Laws.Step

∀ {Γ : List Effect4.Program.Ty} (L : Effect4.Schema.Model.Leaves) (vs : Effect4.Modules.Inputs L Γ)
  {src : {t : Effect4.Program.Ty} → Effect4.Modules.Input Γ t → Effect4.Program.Authoring.TermSrc}
  {env : Effect4.Program.Authoring.Env} {path : List Nat} {vals : List Effect4.Store.Val},
  (∀ {t : Effect4.Program.Ty} (x : Effect4.Modules.Input Γ t),
      Effect4.Modules.Reads (src x) env path vals
        ((Effect4.Schema.Model.imageAt L t).toVal (x.get vs))) →
    ∀ {s : Effect4.Program.Ty} (e : Effect4.Modules.Step Γ s),
      Eq e.canonical Bool.true →
        autoParam (e.ScopeFacts env vals.length) Effect4.Modules.Step.sound._auto_1 →
          autoParam (Effect4.Modules.Step.IdentityFacts L e) Effect4.Modules.Step.sound._auto_3 →
            Effect4.Modules.Reads (Effect4.Modules.Step.term (fun {t} => src) e) env path vals
              ((Effect4.Schema.Model.imageAt L s).toVal (Effect4.Modules.Step.eval L vs e))

step-frameclaim:step-frame

On an update spine of an input, a field that no overwrite of the step names keeps its value: on carriers with no premise on the record's names (Step.frame), and on the machine's record frame for ascending names (Step.frame_read); nothing of a step that is no spine (decisions row 330, slice L2)

Module

Effect4.Laws.Step

∀ {Γ : List Effect4.Program.Ty} (L : Effect4.Schema.Model.Leaves) (vs : Effect4.Modules.Inputs L Γ)
  {fs : List (Prod String (Prod Bool Effect4.Program.Ty))}
  (x : Effect4.Modules.Input Γ (Effect4.Program.Ty.record fs)) {t : Effect4.Program.Ty}
  (g : Effect4.Schema.FieldRef fs t) (e : Effect4.Modules.Step Γ (Effect4.Program.Ty.record fs)),
  Eq e.spine (Option.some x.index) →
    Not (List.instMembership.mem e.writes g.name) →
      Eq (g.get (Effect4.Modules.Step.eval L vs e)) (g.get (x.get vs))

latch-steps-agreeclaim:latch-steps-agree

Each of the Latch's four steps, written natively in the step language, agrees with the model of rc.112's class Latch: isOpen, open and release with scheduleUnsafe's one flush per batch, flushScheduled and closeUnsafe; the reply and the next state through the table, the cell's value being the carrier's image; each by the step language's reading law and one equation of Lean values; nothing of await, interruption, the posted flush's fiber or liveness (decisions row 330, slice L3)

The Latch's steps agree with its model (claim latch-steps-agree).

Module

Effect4.Laws.Library.Latch.Steps

Effect4.Latch.Model.StepsAgree

latch-registration-agreesclaim:latch-registration-agrees

Latch initial construction, await registration and first-match withdrawal read the independent model's reply and next cell; registration uses the table's identity and hint, withdrawal assumes an injective table and aligned value and source scope lengths; cleanup searches waiters before the attached scheduled batch and keeps the scheduled flag, including duplicate registrations; no interruption delivery, posted-flush execution, liveness or host behavior follows (decisions row 330)

Claim latch-registration-agrees: initial construction, registration, and first-match cleanup.

Module

Effect4.Laws.Library.Latch.Registration

Effect4.Latch.Model.RegistrationAgree

partitioned-semaphore-bookkeepingclaim:partitioned-semaphore-bookkeeping

PartitionedSemaphore's four scalar step terms read the independent natural-count model: initialization, availability, attempted acquisition, and reservation of the unmet need; reservation assumes insufficient availability and a request within capacity; initialization returns the scalar record, availability returns its count, and attempted acquisition and reservation return their replies with next scalar records, under successful readings of the input images; no waiter registration, identity allocation, wake delivery, cancellation, wrapper, schedule, progress, codec admission or host behavior (decisions rows 330, 331 and 335)

The four source readings observe the independent scalar model. Reservation retains the insufficient-availability and within-capacity branch premises. This claim excludes identities, registration, cancellation, delivery, wrappers, and host execution.

Module

Effect4.Laws.Library.PartitionedSemaphore.Steps

And
  (∀ (capacity : Nat) (source : Effect4.Program.Authoring.TermSrc)
    (env : Effect4.Program.Authoring.Env) (path : List Nat) (vals : List Effect4.Store.Val),
    Effect4.Modules.Reads source env path vals (Effect4.Store.Val.nat capacity) →
      Effect4.Modules.Reads (Effect4.PartitionedSemaphore.initialStep source) env path vals
        ((Effect4.Schema.Modeled.image Effect4.PartitionedSemaphore.Model.Counts).toVal
          (Effect4.PartitionedSemaphore.Model.initial capacity)))
  (And
    (∀ (s : Effect4.PartitionedSemaphore.Model.Counts) (source : Effect4.Program.Authoring.TermSrc)
      (env : Effect4.Program.Authoring.Env) (path : List Nat) (vals : List Effect4.Store.Val),
      Effect4.Modules.Reads source env path vals
          ((Effect4.Schema.Modeled.image Effect4.PartitionedSemaphore.Model.Counts).toVal s) →
        Effect4.Modules.Reads (Effect4.PartitionedSemaphore.availableStep source) env path vals
          (Effect4.Store.Val.nat (Effect4.PartitionedSemaphore.Model.available s)))
    (And
      (∀ (s : Effect4.PartitionedSemaphore.Model.Counts) (n : Nat)
        (amount source : Effect4.Program.Authoring.TermSrc) (env : Effect4.Program.Authoring.Env)
        (path : List Nat) (vals : List Effect4.Store.Val),
        Effect4.Modules.Reads amount env path vals (Effect4.Store.Val.nat n) →
          Effect4.Modules.Reads source env path vals
              ((Effect4.Schema.Modeled.image Effect4.PartitionedSemaphore.Model.Counts).toVal s) →
            Effect4.Modules.Reads (Effect4.PartitionedSemaphore.tryTakeStep amount source) env path
              vals
              ((Effect4.Store.Image.bool.tuple2
                    (Effect4.Schema.Modeled.image Effect4.PartitionedSemaphore.Model.Counts)).toVal
                (Effect4.PartitionedSemaphore.Model.tryTake s n)))
      (∀ (s : Effect4.PartitionedSemaphore.Model.Counts) (n : Nat)
        (amount source : Effect4.Program.Authoring.TermSrc) (env : Effect4.Program.Authoring.Env)
        (path : List Nat) (vals : List Effect4.Store.Val),
        Effect4.Modules.Reads amount env path vals (Effect4.Store.Val.nat n) →
          Effect4.Modules.Reads source env path vals
              ((Effect4.Schema.Modeled.image Effect4.PartitionedSemaphore.Model.Counts).toVal s) →
            instLTNat.lt s.available n →
              instLENat.le n s.capacity →
                Effect4.Modules.Reads (Effect4.PartitionedSemaphore.reserveStep amount source) env
                  path vals
                  ((Effect4.Store.Image.nat.tuple2
                        (Effect4.Schema.Modeled.image
                          Effect4.PartitionedSemaphore.Model.Counts)).toVal
                    (Effect4.PartitionedSemaphore.Model.reserve s n)))))

pubsub-single-steps-agreeclaim:pubsub-single-steps-agree

Six pure PubSub bookkeeping sources read the independent capacity-one, replay-zero, natural-message model: initial, subscription with a fresh logical name, tryPublish, poll, unsubscribe and slide; input sources read their exact images, and folds require aligned value and source scope lengths; observations contain each reply and next model state; no host subscription-object identity relation, handle allocation, delivery, lifetime, backpressure execution, arbitrary capacity or whole module run (decisions rows 330, 331 and 335)

The six pure source observations agree with the independent model images. This claim retains fresh subscribe names and aligned fold scopes. Model.Live bounds its source interpretation; the formal equations do not require it.

Module

Effect4.Laws.Library.PubSub.Steps

And
  (∀ (env : Effect4.Program.Authoring.Env) (path : List Nat) (vals : List Effect4.Store.Val),
    Effect4.Modules.Reads Effect4.PubSub.initialStep env path vals
      ((Effect4.Schema.Modeled.image Effect4.PubSub.Model.State).toVal
        Effect4.PubSub.Model.initial))
  (And
    (∀ (s : Effect4.PubSub.Model.State) (id : Nat)
      (idSrc cellSrc : Effect4.Program.Authoring.TermSrc) (env : Effect4.Program.Authoring.Env)
      (path : List Nat) (vals : List Effect4.Store.Val),
      Effect4.Modules.Reads idSrc env path vals (Effect4.Store.Val.nat id) →
        Effect4.Modules.Reads cellSrc env path vals
            ((Effect4.Schema.Modeled.image Effect4.PubSub.Model.State).toVal s) →
          Effect4.PubSub.Model.Fresh s id →
            Effect4.Modules.Reads (Effect4.PubSub.subscribeStep idSrc cellSrc) env path vals
              ((Effect4.Store.Image.unit.tuple2
                    (Effect4.Schema.Modeled.image Effect4.PubSub.Model.State)).toVal
                (Effect4.PubSub.Model.subscribe s id)))
    (And
      (∀ (s : Effect4.PubSub.Model.State) (message : Nat)
        (messageSrc cellSrc : Effect4.Program.Authoring.TermSrc)
        (env : Effect4.Program.Authoring.Env) (path : List Nat) (vals : List Effect4.Store.Val),
        Effect4.Modules.Reads messageSrc env path vals (Effect4.Store.Val.nat message) →
          Effect4.Modules.Reads cellSrc env path vals
              ((Effect4.Schema.Modeled.image Effect4.PubSub.Model.State).toVal s) →
            Effect4.Modules.Reads (Effect4.PubSub.tryPublishStep messageSrc cellSrc) env path vals
              ((Effect4.Store.Image.bool.tuple2
                    (Effect4.Schema.Modeled.image Effect4.PubSub.Model.State)).toVal
                (Effect4.PubSub.Model.tryPublish s message)))
      (And
        (∀ (s : Effect4.PubSub.Model.State) (id : Nat)
          (idSrc cellSrc : Effect4.Program.Authoring.TermSrc) (env : Effect4.Program.Authoring.Env)
          (path : List Nat) (vals : List Effect4.Store.Val),
          Eq vals.length (List.length env.names) →
            Effect4.Modules.Reads idSrc env path vals (Effect4.Store.Val.nat id) →
              Effect4.Modules.Reads cellSrc env path vals
                  ((Effect4.Schema.Modeled.image Effect4.PubSub.Model.State).toVal s) →
                Effect4.Modules.Reads (Effect4.PubSub.pollStep idSrc cellSrc) env path vals
                  ((Effect4.Store.Image.nat.option.tuple2
                        (Effect4.Schema.Modeled.image Effect4.PubSub.Model.State)).toVal
                    (Effect4.PubSub.Model.poll s id)))
        (And
          (∀ (s : Effect4.PubSub.Model.State) (id : Nat)
            (idSrc cellSrc : Effect4.Program.Authoring.TermSrc)
            (env : Effect4.Program.Authoring.Env) (path : List Nat) (vals : List Effect4.Store.Val),
            Eq vals.length (List.length env.names) →
              Effect4.Modules.Reads idSrc env path vals (Effect4.Store.Val.nat id) →
                Effect4.Modules.Reads cellSrc env path vals
                    ((Effect4.Schema.Modeled.image Effect4.PubSub.Model.State).toVal s) →
                  Effect4.Modules.Reads (Effect4.PubSub.unsubscribeStep idSrc cellSrc) env path vals
                    ((Effect4.Store.Image.unit.tuple2
                          (Effect4.Schema.Modeled.image Effect4.PubSub.Model.State)).toVal
                      (Effect4.PubSub.Model.unsubscribe s id)))
          (∀ (s : Effect4.PubSub.Model.State) (cellSrc : Effect4.Program.Authoring.TermSrc)
            (env : Effect4.Program.Authoring.Env) (path : List Nat) (vals : List Effect4.Store.Val),
            Effect4.Modules.Reads cellSrc env path vals
                ((Effect4.Schema.Modeled.image Effect4.PubSub.Model.State).toVal s) →
              Effect4.Modules.Reads (Effect4.PubSub.slideStep cellSrc) env path vals
                ((Effect4.Store.Image.unit.tuple2
                      (Effect4.Schema.Modeled.image Effect4.PubSub.Model.State)).toVal
                  (Effect4.PubSub.Model.slide s)))))))

channel-batch-transformclaim:channel-batch-transform

The authored Channel batch dispatcher selects the wrapped batch transformation only for an exact Chunk input, selects unchanged completion for End, and propagates input failure with its resulting stores; actual handler elaboration and aligned scopes are premises; the selected handler's complete meaning includes its failure and stores; no execution of stored definition calls, nonempty output, scheduling or host simulation

Batch mapping selects the wrapped transformation only for Chunk. End retains its leftover; an input failure retains its cause and resulting stores. The selected handler's full meaning retains a transformation failure and its stores.

Module

Effect4.Laws.Library.Channel.Protocol

∀ {self : Effect4.Program.Authoring.Src Effect4.Program.NativeOp}
  {transform :
    Effect4.Program.Authoring.TermSrc → Effect4.Program.Authoring.Src Effect4.Program.NativeOp}
  {env : Effect4.Program.Authoring.Env} {path : List Nat} {vals : List Effect4.Machine.Val}
  {body success done : Effect4.Program.NativeEff},
  Eq vals.length (List.length env.names) →
    ∀
      (outcome :
        Effect4.Exit (Except Effect4.Machine.Val (List Effect4.Machine.Val)) Effect4.Machine.Err
          Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
      (stores after : Effect4.Machine.Stores),
      Eq (self env (instHAppendOfAppend.hAppend path (List.cons 0 List.nil))) (Except.ok body) →
        Eq (Effect4.Program.Denote.meaning body vals stores)
            (Effect4.Channel.bindAnswer_protocol.match_1✝
              (fun outcome => Prod Effect4.Machine.ExitV Effect4.Machine.Stores) outcome
              (fun leftover =>
                { fst := Effect4.Exit.success (Effect4.Program.Stream.endVal leftover),
                  snd := after })
              (fun items =>
                { fst := Effect4.Exit.success (Effect4.Program.Stream.chunkVal items),
                  snd := after })
              fun cause => { fst := Effect4.Exit.failure cause, snd := after }) →
          Eq
              (Effect4.Program.Authoring.succeed
                (Effect4.Pull.endValue
                  (Effect4.Program.Authoring.minted
                    ((env.push (List.cons (env.mint "answer") List.nil)).mint "payload")))
                ((env.push (List.cons (env.mint "answer") List.nil)).push
                  (List.cons ((env.push (List.cons (env.mint "answer") List.nil)).mint "payload")
                    List.nil))
                (instHAppendOfAppend.hAppend
                  (instHAppendOfAppend.hAppend path (List.cons 1 List.nil)) (List.cons 0 List.nil)))
              (Except.ok done) →
            Eq
                (Effect4.Program.Authoring.bindWith
                  (transform
                    (Effect4.Program.Authoring.app "snd"
                      (List.cons
                        (Effect4.Program.Authoring.minted
                          ((env.push (List.cons (env.mint "answer") List.nil)).mint "rest"))
                        List.nil)))
                  (fun mapped => Effect4.Program.Authoring.succeed (Effect4.Pull.chunkValue mapped))
                  ((env.push (List.cons (env.mint "answer") List.nil)).push
                    (List.cons ((env.push (List.cons (env.mint "answer") List.nil)).mint "rest")
                      List.nil))
                  (instHAppendOfAppend.hAppend
                    (instHAppendOfAppend.hAppend path (List.cons 1 List.nil))
                    (List.cons 1 List.nil)))
                (Except.ok success) →
              Exists fun tree =>
                And
                  (Eq (Effect4.Channel.Internal.mapEffectOf self transform env path)
                    (Except.ok tree))
                  (Eq (Effect4.Program.Denote.meaning tree vals stores)
                    (Effect4.Channel.bindAnswer_protocol.match_1✝
                      (fun outcome => Prod Effect4.Machine.ExitV Effect4.Machine.Stores) outcome
                      (fun leftover =>
                        Effect4.Program.Denote.meaning done
                          (instHAppendOfAppend.hAppend
                            (instHAppendOfAppend.hAppend vals
                              (List.cons (Effect4.Program.Stream.endVal leftover) List.nil))
                            (List.cons leftover List.nil))
                          after)
                      (fun items =>
                        Effect4.Program.Denote.meaning success
                          (instHAppendOfAppend.hAppend
                            (instHAppendOfAppend.hAppend vals
                              (List.cons (Effect4.Program.Stream.chunkVal items) List.nil))
                            (List.cons (Effect4.Program.Stream.chunkVal items) List.nil))
                          after)
                      fun cause => { fst := Effect4.Exit.failure cause, snd := after }))

channel-completion-transformclaim:channel-completion-transform

The authored Channel completion dispatcher selects the wrapped completion transformation only for an exact End input, selects unchanged batches for Chunk, and propagates input failure with its resulting stores; actual handler elaboration and aligned scopes are premises; no execution of stored definition calls, nonempty output, scheduling or host simulation

Completion mapping selects the wrapped transformation only for End. Chunk retains its batch; input failures and selected-handler failures keep their stores.

Module

Effect4.Laws.Library.Channel.Protocol

∀ {self : Effect4.Program.Authoring.Src Effect4.Program.NativeOp}
  {transform :
    Effect4.Program.Authoring.TermSrc → Effect4.Program.Authoring.Src Effect4.Program.NativeOp}
  {env : Effect4.Program.Authoring.Env} {path : List Nat} {vals : List Effect4.Machine.Val}
  {body success done : Effect4.Program.NativeEff},
  Eq vals.length (List.length env.names) →
    ∀
      (outcome :
        Effect4.Exit (Except Effect4.Machine.Val (List Effect4.Machine.Val)) Effect4.Machine.Err
          Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
      (stores after : Effect4.Machine.Stores),
      Eq (self env (instHAppendOfAppend.hAppend path (List.cons 0 List.nil))) (Except.ok body) →
        Eq (Effect4.Program.Denote.meaning body vals stores)
            (Effect4.Channel.bindAnswer_protocol.match_1✝
              (fun outcome => Prod Effect4.Machine.ExitV Effect4.Machine.Stores) outcome
              (fun leftover =>
                { fst := Effect4.Exit.success (Effect4.Program.Stream.endVal leftover),
                  snd := after })
              (fun items =>
                { fst := Effect4.Exit.success (Effect4.Program.Stream.chunkVal items),
                  snd := after })
              fun cause => { fst := Effect4.Exit.failure cause, snd := after }) →
          Eq
              (Effect4.Program.Authoring.bindWith
                (transform
                  (Effect4.Program.Authoring.minted
                    ((env.push (List.cons (env.mint "answer") List.nil)).mint "payload")))
                (fun mapped => Effect4.Program.Authoring.succeed (Effect4.Pull.endValue mapped))
                ((env.push (List.cons (env.mint "answer") List.nil)).push
                  (List.cons ((env.push (List.cons (env.mint "answer") List.nil)).mint "payload")
                    List.nil))
                (instHAppendOfAppend.hAppend
                  (instHAppendOfAppend.hAppend path (List.cons 1 List.nil)) (List.cons 0 List.nil)))
              (Except.ok done) →
            Eq
                (Effect4.Program.Authoring.succeed
                  (Effect4.Pull.chunkValue
                    (Effect4.Program.Authoring.app "snd"
                      (List.cons
                        (Effect4.Program.Authoring.minted
                          ((env.push (List.cons (env.mint "answer") List.nil)).mint "rest"))
                        List.nil)))
                  ((env.push (List.cons (env.mint "answer") List.nil)).push
                    (List.cons ((env.push (List.cons (env.mint "answer") List.nil)).mint "rest")
                      List.nil))
                  (instHAppendOfAppend.hAppend
                    (instHAppendOfAppend.hAppend path (List.cons 1 List.nil))
                    (List.cons 1 List.nil)))
                (Except.ok success) →
              Exists fun tree =>
                And
                  (Eq (Effect4.Channel.Internal.mapDoneEffectOf self transform env path)
                    (Except.ok tree))
                  (Eq (Effect4.Program.Denote.meaning tree vals stores)
                    (Effect4.Channel.bindAnswer_protocol.match_1✝
                      (fun outcome => Prod Effect4.Machine.ExitV Effect4.Machine.Stores) outcome
                      (fun leftover =>
                        Effect4.Program.Denote.meaning done
                          (instHAppendOfAppend.hAppend
                            (instHAppendOfAppend.hAppend vals
                              (List.cons (Effect4.Program.Stream.endVal leftover) List.nil))
                            (List.cons leftover List.nil))
                          after)
                      (fun items =>
                        Effect4.Program.Denote.meaning success
                          (instHAppendOfAppend.hAppend
                            (instHAppendOfAppend.hAppend vals
                              (List.cons (Effect4.Program.Stream.chunkVal items) List.nil))
                            (List.cons (Effect4.Program.Stream.chunkVal items) List.nil))
                          after)
                      fun cause => { fst := Effect4.Exit.failure cause, snd := after }))

pull-protocol-selectionclaim:pull-protocol-selection

Pull's outcome handler selects exactly one batch, completion or failure branch under the existing denotation: an exact Chunk or End value, or the complete input cause, chooses its branch; aligned source and value scopes and successful elaboration of all handlers are premises; the selected handler receives the input's resulting stores, and its full exit and final stores are the result; no scheduler, whole-stream run, nonempty-batch admission, host Done adapter or mixed-Done correspondence (decisions rows 331 and 335)

Under an exact input observation, Pull chooses its one protocol handler. All handlers elaborate at their actual scopes. The selected handler receives the input's resulting stores; its complete exit and final stores are the result. This is a law of the existing denotation, not a scheduling or host correspondence theorem.

Module

Effect4.Laws.Library.Pull.Protocol

∀ {self : Effect4.Program.Authoring.Src Effect4.Program.NativeOp} {options : Effect4.Pull.Handlers}
  {env : Effect4.Program.Authoring.Env} {path : List Nat} {vals : List Effect4.Machine.Val}
  {body success done failure : Effect4.Program.NativeEff},
  Eq vals.length (List.length env.names) →
    ∀
      (outcome :
        Effect4.Exit (Except Effect4.Machine.Val (List Effect4.Machine.Val)) Effect4.Machine.Err
          Effect4.Machine.Defect Effect4.FiberId Effect4.Machine.Ann)
      (stores after : Effect4.Machine.Stores),
      Eq (self env (instHAppendOfAppend.hAppend path (List.cons 0 List.nil))) (Except.ok body) →
        Eq (Effect4.Program.Denote.meaning body vals stores)
            (Effect4.Pull.matchEffect_protocol.match_1
              (fun outcome => Prod Effect4.Machine.ExitV Effect4.Machine.Stores) outcome
              (fun leftover =>
                { fst := Effect4.Exit.success (Effect4.Program.Stream.endVal leftover),
                  snd := after })
              (fun items =>
                { fst := Effect4.Exit.success (Effect4.Program.Stream.chunkVal items),
                  snd := after })
              fun cause => { fst := Effect4.Exit.failure cause, snd := after }) →
          Eq
              (options.onDone
                (Effect4.Program.Authoring.minted
                  ((env.push (List.cons (env.mint "value") List.nil)).mint "payload"))
                ((env.push (List.cons (env.mint "value") List.nil)).push
                  (List.cons ((env.push (List.cons (env.mint "value") List.nil)).mint "payload")
                    List.nil))
                (instHAppendOfAppend.hAppend
                  (instHAppendOfAppend.hAppend path (List.cons 1 List.nil)) (List.cons 0 List.nil)))
              (Except.ok done) →
            Eq
                (options.onSuccess
                  (Effect4.Program.Authoring.app "snd"
                    (List.cons
                      (Effect4.Program.Authoring.minted
                        ((env.push (List.cons (env.mint "value") List.nil)).mint "rest"))
                      List.nil))
                  ((env.push (List.cons (env.mint "value") List.nil)).push
                    (List.cons ((env.push (List.cons (env.mint "value") List.nil)).mint "rest")
                      List.nil))
                  (instHAppendOfAppend.hAppend
                    (instHAppendOfAppend.hAppend path (List.cons 1 List.nil))
                    (List.cons 1 List.nil)))
                (Except.ok success) →
              Eq
                  (options.onFailure (Effect4.Program.Authoring.minted (env.mint "cause"))
                    (env.push (List.cons (env.mint "cause") List.nil))
                    (instHAppendOfAppend.hAppend path (List.cons 2 List.nil)))
                  (Except.ok failure) →
                Exists fun tree =>
                  And (Eq (Effect4.Pull.matchEffect self options env path) (Except.ok tree))
                    (Eq (Effect4.Program.Denote.meaning tree vals stores)
                      (Effect4.Pull.matchEffect_protocol.match_1
                        (fun outcome => Prod Effect4.Machine.ExitV Effect4.Machine.Stores) outcome
                        (fun leftover =>
                          Effect4.Program.Denote.meaning done
                            (instHAppendOfAppend.hAppend
                              (instHAppendOfAppend.hAppend vals
                                (List.cons (Effect4.Program.Stream.endVal leftover) List.nil))
                              (List.cons leftover List.nil))
                            after)
                        (fun items =>
                          Effect4.Program.Denote.meaning success
                            (instHAppendOfAppend.hAppend
                              (instHAppendOfAppend.hAppend vals
                                (List.cons (Effect4.Program.Stream.chunkVal items) List.nil))
                              (List.cons (Effect4.Program.Stream.chunkVal items) List.nil))
                            after)
                        fun cause =>
                        Effect4.Program.Denote.meaning failure
                          (instHAppendOfAppend.hAppend vals
                            (List.cons (Effect4.Machine.Val.exitErr cause) List.nil))
                          after))

pull-completion-recoveryclaim:pull-completion-recovery

Pull's completion recovery uses the existing bind denotation: after successful elaboration of the input and answer handler, an input failure retains its complete cause and resulting stores, and an input success runs the answer handler at the bound value with those stores; that handler's failure escapes unchanged; exact Chunk and End selection is the helper matchAnswer_meaning, and no scheduler, whole-stream run or host Done correspondence follows (decisions rows 331 and 335)

Completion recovery passes an input failure through with all stores left by the input. For a success it uses the already compiled answer handler, including its failure result.

Module

Effect4.Laws.Library.Pull.Protocol

∀ {self : Effect4.Program.Authoring.Src Effect4.Program.NativeOp}
  {onDone :
    Effect4.Program.Authoring.TermSrc → Effect4.Program.Authoring.Src Effect4.Program.NativeOp}
  {env : Effect4.Program.Authoring.Env} {path : List Nat} {vals : List Effect4.Machine.Val}
  {body rest : Effect4.Program.NativeEff} (stores : Effect4.Machine.Stores),
  Eq (self env (instHAppendOfAppend.hAppend path (List.cons 0 List.nil))) (Except.ok body) →
    Eq
        (Effect4.Pull.matchAnswer (Effect4.Program.Authoring.minted (env.mint "answer"))
          (fun chunk => Effect4.Program.Authoring.succeed chunk) onDone
          (env.push (List.cons (env.mint "answer") List.nil))
          (instHAppendOfAppend.hAppend path (List.cons 1 List.nil)))
        (Except.ok rest) →
      Exists fun tree =>
        And (Eq (Effect4.Pull.catchDone self onDone env path) (Except.ok tree))
          (Eq (Effect4.Program.Denote.meaning tree vals stores)
            (Effect4.Pull.catchDone_meaning.match_1
              (fun x => Prod Effect4.Machine.ExitV Effect4.Machine.Stores)
              (Effect4.Program.Denote.meaning body vals stores)
              (fun value after =>
                Effect4.Program.Denote.meaning rest
                  (instHAppendOfAppend.hAppend vals (List.cons value List.nil)) after)
              fun cause after => { fst := Effect4.Exit.failure cause, snd := after }))

stream-array-step-agreementclaim:stream-array-step-agreement

The Stream array source's atomic batch extraction returns the pending list and clears its allocated backing cell, under aligned source and value scopes, a receiver reading the cell handle, and the cell holding the input image; the stored Step callback reads an independent list model and consumes Ref's operation law; no whole pull, stream run, scheduling, scope finalization, host correspondence, codec admission or handle allocation (decisions rows 331 and 335)

One allocated cell step agrees with the independent batch extraction transition.

Module

Effect4.Laws.Library.Stream.Array

∀ (A : Effect4.Program.Ty) (L : Effect4.Schema.Model.Leaves)
  (pending : List (Effect4.Schema.Model.CarrierAt L A)) {env : Effect4.Program.Authoring.Env}
  {path : List Nat} {vals : List Effect4.Machine.Val} {receiver : Effect4.Program.Authoring.TermSrc}
  {q : Effect4.Machine.RefKey} {stores : Effect4.Machine.Stores},
  Eq vals.length (List.length env.names) →
    Effect4.Modules.Reads receiver env path vals (Effect4.Machine.Val.cell q) →
      Eq (Effect4.Machine.refPeek stores.refs q)
          (Option.some ((Effect4.Schema.Model.imageAt L A.list).toVal pending)) →
        Exists fun term =>
          Exists fun request =>
            And
              (Eq (Effect4.Stream.arrayBatch A receiver env path)
                (Except.ok
                  (Effect4.Program.Eff.perform (Effect4.Program.NativeOp.refModifyWith term)
                    request)))
              (And
                (Eq (Effect4.Program.evalTerm vals request)
                  (Option.some (Effect4.Machine.Val.cell q)))
                (Eq
                  (Effect4.Machine.syncOpStep (Effect4.Machine.SyncOp.refModify q term vals) stores)
                  (Option.some
                    {
                      fst :=
                        Effect4.Ref.resultStores (Effect4.Schema.Model.imageAt L A.list)
                          (Effect4.Ref.Model.modify Effect4.Stream.ArrayModel.pull pending) q
                          stores,
                      snd :=
                        (Effect4.Schema.Model.imageAt L A.list).toVal
                          (Effect4.Ref.Model.modify Effect4.Stream.ArrayModel.pull
                              pending).reply })))

ref-steps-agreeclaim:ref-steps-agree

Each of Ref's thirteen effectful operations agrees with the independent model of latest's Ref (Effect 4.0.1): allocation appends the initial value; on one allocated cell holding the encoded value, with a callback that evaluates to the encoded next value, each operation's reply and final stores are the model's; the laws compare replies and final stores under their allocation and callback-evaluation premises, not write events, so they say nothing of whether an operation writes an unchanged value; no scheduling, whole run, host object identity, callback exception or reentrant mutation (decisions row 335)

The thirteen operation laws hold (the claim ref-steps-agree, role simulation). Placement: concept translation-simulation, requirement R10. Reach: allocation for any exact image; every other operation on one allocated cell holding the encoded value, with a callback that evaluates to the encoded next value. Each law observes the reply and the final stores. Not established: the laws compare replies and final stores, not write events; no scheduling, whole run, host object identity, callback exception or reentrant mutation. Consumers: the typed callback connector (src/Effect4/Laws/Library/Ref/Callback.lean), then SynchronizedRef and the keyed cells (decisions row 335).

Module

Effect4.Laws.Library.Ref.Operations

Effect4.Ref.StepsAgree