Host Session Protocolconcept:host-session-protocol

run-admitted-historyclaim:run-admitted-history

Every reached recorded run has its built program's call table and a history of session-admitted native decisions, at its compile budget; no progress or outside-host claim

Every reached run's machine is a history of its program. Reach: every built program, name, budget and profile, every row.

Module

Effect4.Laws.Run.Frame

∀ (s : Effect4.Run),
  s.Reached →
    And (Eq s.session.calls (Effect4.Api.HostSession.callTable s.built.program s.built.table))
      (Effect4.Run.HistoryOf s.built s.budget.compileFuel s.machine)

keys-onceclaim:keys-once

A reached run binds, submits and applies each key at most once, and applies no retired key

Each key is bound once, received once and applied once, and a retired call is never applied. In every recorded run of every program: the session binds a key at most once, accepts at most one reply receipt and applies at most one reply at a key, and no key that a control or an application retired is ever applied. Concept host-session-protocol, R6; the proposed claim keys-once (role preservation). The machine's part is that a guard the machine dropped never holds a request again (reservedKeys_steppedBy): a later park takes a fresh token. Consumer: stale_never_applies, clauses one to three. Reach: every program, table, budget and journal of the four row kinds, with its raw rows. It does not establish reply admission at the application, the retirement edge of the host protocol, the order of two applications, or which reply a host sends: a host may answer a call with any body it chooses.

Module

Effect4.Laws.Run.Journal

∀ (s : Effect4.Run),
  s.Reached →
    And s.boundKeys.Nodup
      (And s.submittedKeys.Nodup
        (And s.appliedKeys.Nodup
          (∀ (k : Effect4.Api.HostSession.Key),
            List.instMembership.mem s.retiredKeys k →
              Not (List.instMembership.mem s.appliedKeys k))))

allows-answerclaim:allows-answer

Answering an async request is an allowed transition from awaitingAsync

An answer is an edge from awaitingAsync to every state, so the machine it leaves is never a protocol refusal.

Module

Effect4.Laws.Run

Literature

Wadler2012, audit P35 (adaptedResult)

∀ (key : Effect4.Api.HostSession.Key) (target : Effect4.Api.HostProtocol.State),
  Eq
    (Effect4.Api.HostProtocol.allows Effect4.Api.HostProtocol.State.awaitingAsync
      (Effect4.Api.HostProtocol.Label.answer key) target)
    Bool.true

reply-commuteclaim:reply-commute

Independent host replies commute in session submission

Two accepted receipts for distinct keys commute as whole sessions. The machine, active calls, call IDs, consumed ledger, and retired ownership are unchanged in either order. This is receipt/storage only, not answerAsync continuation execution.

Module

Effect4.Laws.Api.HostSession

Literature

LynchVaandrager1995, audit C4 (analogy)

∀ {program : Effect4.Api.Program} {table : Effect4.Program.RowTable}
  (s : Effect4.Api.HostSession.Session program table) (a b : Effect4.Api.HostSession.Reply),
  Ne a.key b.key →
    Eq (Effect4.Api.HostSession.submit s a).phase Effect4.Api.HostSession.Phase.preflight →
      Eq (Effect4.Api.HostSession.submit s b).phase Effect4.Api.HostSession.Phase.preflight →
        Eq (Effect4.Api.HostSession.submit (Effect4.Api.HostSession.submit s a).session b).session
          (Effect4.Api.HostSession.submit (Effect4.Api.HostSession.submit s b).session a).session

session-success-prepared-membershipclaim:session-success-prepared-membership

A session-accepted successful reply prepares a member of its selected shape-decided row, or, where the row's own columns refuse it, it is admitted at its call's checked instance (InstanceSuccess; decisions row 323)

A session-accepted successful completion prepares the actual row-typed value, or it is admitted at the call's checked instance and reaches the program unchanged. On the row's path membership requires the selected row's shape-decided answer column. Failures, world-reading columns and token-world correlation remain outside this theorem. The session is not executed here.

Module

Effect4.Laws.Api.HostSession

∀ {program : Effect4.Api.Program} {table : Effect4.Program.RowTable}
  (s : Effect4.Api.HostSession.Session program table) (reply : Effect4.Api.HostSession.Reply)
  (decision : Effect4.Program.NativeDecision) (value : Effect4.Machine.Val),
  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 →
    Eq reply.completion (Effect4.Machine.Completion.ofExit (Effect4.Exit.success value)) →
      Eq (Effect4.Api.HostSession.preflight s reply) (Except.ok decision) →
        Or (Effect4.Api.HostSession.PreparedSuccess s reply decision)
          (Effect4.Api.HostSession.InstanceSuccess s reply decision)

reply-at-call-instanceclaim:reply-at-call-instance

A reply admitted at its call's checked instance is a handle-free member of the instance's answer column, and the machine prepares it unchanged, at a row whose answer column allocates nothing; a failure admitted there holds no reserved defect; the registration keeps its call's address and the session reads programCallAt there, from a table made once at open (reached_callInstance); in a recorded, funded run that address holds a call of the operation in the program (origin_addresses_call); the expansion of layer references keeping it there is open (decisions rows 183, 323)

A success admitted at its call's instance is a member of the instance's answer column, holds no handle, and reaches the program unchanged: the machine's preparation leaves the stores as they are and answers the value itself.

Module

Effect4.Laws.Program.Admit

∀ (program : Effect4.Program.NativeEff) (table : Effect4.Program.RowTable)
  (instanceAt : List Nat → Option (Effect4.Program.CallInstance Effect4.Program.NativeOp))
  (m : Effect4.Program.NativeMachine) (r : Effect4.Program.RecordedReply)
  (value : Effect4.Machine.Val),
  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 r.completion (Effect4.Machine.Completion.ofExit (Effect4.Exit.success value)) →
      Effect4.Program.InstanceEnvelope table instanceAt m r →
        Exists fun origin =>
          Exists fun c =>
            And (Eq (Effect4.Program.originOf m r.fiber r.token) (Option.some origin))
              (And (Eq (instanceAt origin) (Option.some c))
                (And (Eq c.op r.op)
                  (And
                    (Eq
                      (Effect4.Program.Val.hasTy value c.answer
                        (m.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)
                      Bool.true)
                    (And (Eq (Effect4.Store.Val.handles value) List.nil)
                      (Eq
                        (Effect4.Machine.prepareAsyncAnswer (Effect4.Program.interpOf program table)
                          m r.fiber r.token r.completion)
                        {
                          fst :=
                            m.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.Prim.success value })))))

block-call-instanceclaim:block-call-instance

On a program that the module check admits, the call instance answers at every call, with the call's operation: in a definition's body at the block's signature and its declared request, in a block's main program at the block's signature, and in a program with no block (programCallAt over Eff.partAt); the session's call table is its lookup, so a session that start made has an instance at every call of its admitted program (start_callInstance_complete); it does not say that the expansion of layer references keeps a call at its address, nor anything of a run (decisions rows 323, 328, 333)

The claim block-call-instance. On a program that the module check admits, the call instance answers at every call, with the call's operation: inside a definition's body, in the main program of a block, and in a program with no block. Before this law the session's call table missed every call of a program with a block (seat HOST's probe, part B).

Module

Effect4.Laws.Program.Typing.Parts

∀ {Op : Type} {s : Effect4.Program.Signature Op} {p : Effect4.Program.Eff Op}
  {T : Effect4.Program.EffTy} {path : List Nat} {op : Op} {request : Effect4.Program.Term},
  Eq (Effect4.Program.Checker.checkModule s p) (Except.ok T) →
    Eq ((Effect4.Program.Node.eff p).at_ path)
        (Option.some (Effect4.Program.Node.eff (Effect4.Program.Eff.perform op request))) →
      Exists fun c =>
        And (Eq (Effect4.Program.programCallAt s List.nil p path) (Option.some c)) (Eq c.op op)

session-failure-shape-freeclaim:session-failure-shape-free

A session-accepted failing reply carries no reserved defect: the failure half of admit_sound (decisions row 191, E4-HOST-CE-008)

An accepted failing reply has no shape defect (decisions row 191, E4-HOST-CE-008): executable admission refuses the reserved defects (admit_failure_reservedFree), so a session-accepted failure satisfies NoShapeDefect at every type. This is the failure half of admit_sound, executable admission implying the ghost AnswerOk; the value half waits on row 97's handle declarations, and the cause's membership in the error column is external_error_typed.

Module

Effect4.Laws.Api.HostSession

∀ {program : Effect4.Api.Program} {table : Effect4.Program.RowTable}
  (s : Effect4.Api.HostSession.Session program table) (reply : Effect4.Api.HostSession.Reply)
  (decision : Effect4.Program.NativeDecision) (c : Effect4.Machine.CauseV),
  Eq reply.completion (Effect4.Machine.Completion.ofExit (Effect4.Exit.failure c)) →
    Eq (Effect4.Api.HostSession.preflight s reply) (Except.ok decision) →
      ∀ (ty : Effect4.Program.EffTy),
        Effect4.Program.Typed.NoShapeDefect ty (Effect4.Exit.failure c)

Register record E4-HOST-CE-008 (REPAIRED)

| `E4-HOST-CE-008` | REPAIRED 2026-10-03 (decisions row 191: `admit` and `externalAdmits` refuse a host failure carrying `badName` or `notImplemented`, `Refusal.reservedDefect`; `preflight_failure_noShapeDefect`, `Laws/Api/HostSession.lean`, `[propext, Quot.sound]`); SEEDED 2026-10-03 (Codex, `docs/research/2026-10-03-session-work/t4-audit.lean`; registered by Claude) | Executable admission is at least as strict as the typed exit judgment on failures: `admit = none` on a failing reply gives `CompletionStrong`, the failure half of `admit_sound` (T4) | `Test/Counterexamples/Machine/Runtime/HostReservedDefect.lean`: the session accepted `die badName` (`preflight` returned the answer decision, `admit` no refusal, `externalAdmits` true) while `ExitOk` refuses it at every world (`NoShapeDefect`, row 152) | Admission refuses the two reserved defects before reading the error column, on the decision path and the oracle path; ordinary defects and interrupts stay admitted at every error column. The value half of admission (row 97) is unchanged. |

frontier-awaithostclaim:frontier-awaithost

Machine awaitingAsync state matches frontier awaitHost reasons

Module

Effect4.Laws.Api.Frontier

∀ (why : Effect4.Machine.Exhaustion) (m : Effect4.Program.NativeMachine),
  Iff (Eq (Effect4.Api.HostProtocol.observe m) Effect4.Api.HostProtocol.State.awaitingAsync)
    (Exists fun key =>
      List.instMembership.mem (Effect4.Api.frontierReasons why m)
        (Effect4.Api.FrontierReason.awaitHost key))

host-progressclaim:host-progress

Host session progress under external answers

Reason

Host session progress is subject to external driver execution; outside closed runtime

rows-loop-frontierclaim:rows-loop-frontier

H8's detailed frontier on loops: for a recorded run of a LoopedRows program the row fragment with loops admits, funded, at rest and driven by a host, every call the machine waits on is a host row, and past a budget bound the detailed observation of the budgeted meaning under the run's reply tape waits at that row and request, with the machine's stores and the tape read to its end (no progress claim: a wait is a frontier, never a failure; nothing of a fork, a scope or an interruption; the host-meaning widening, slice L4)

H8's detailed frontier on loops (Q4): for a recorded run of a program of the row fragment with loops that is funded, at rest and driven by a host, every call the machine waits on is a host row, and past a budget bound the detailed observation of the budgeted meaning under the run's reply tape waits at that row and request, with the machine's stores and the tape read to its end. The session prefix (session_settled) leaves a root parked on that call, and the local wait is the meaning's (localWaitC_to_rowsB). Concept host-session-protocol, claim rows-loop-frontier, role simulation; requirement R12 (and R6). Consumers: the waiting driver and the resource prefix (slices S1 and S2). It establishes no progress: a wait is a frontier, never a failure, and nothing says the host answers; nothing of a fork, a scope or an interruption.

Module

Effect4.Laws.Api.SessionMeaningLoop

Effect4.Run.H8FrontierLoopedRows

rows-loop-frontier-hostclaim:rows-loop-frontier-host

H9's detailed frontier on loops: the same under any host whose answers are the run's and which leaves the waited call unanswered: past a budget bound the meaning under the host waits at that call, with the machine's stores and the host where the answers left it (the host's silence is a premise; the host-meaning widening, slice L4)

H9's detailed frontier on loops (Q4 under a host): as rows_loop_frontier, under any host whose answers are the run's (HostAnswered) and which does not answer the call the machine waits on: past a budget bound the meaning under the host waits at that call, with the machine's stores and the host where the answers left it. Concept host-session-protocol, claim rows-loop-frontier-host, role simulation; requirement R12 (and R6). It does not establish that the host leaves the call unanswered: that is the premise.

Module

Effect4.Laws.Api.SessionMeaningLoop

Effect4.Run.H9FrontierLoopedRows