What the sequence expressions Guarded2Network builds over inbox mean.

Core/ComputableTLAPlus/Semantics/Interface.lean keeps the expression layer abstract: Eval is a relation with no axioms about any particular operator, and the only sequence facts it carries are value-level (seqAppend, isSeq). That is deliberate — Core's semantics has no business naming TLA⁺'s Sequences module. But this pass compiles a receive into Head/Tail/Len calls over inbox (Guarded2Network.head/.tail/.lenGt), so its refinement proof has to know that Head(inbox) denotes the first element of what inbox holds — a fact about those expressions, not about Eval in general.

So the laws live here, in a class the refinement theorems take instance-implicit, and the split is: ExprSemantics says what a sequence value is, SeqBuiltins says what this pass's sequence expressions evaluate to. A concrete TLA⁺ evaluator will satisfy both; nothing in Core/ has to mention Head to state either.

Each law is an ↔ against the expression's shape rather than a one-directional evaluation rule, because the proof needs both readings: forwards to compute the target's guard from the source's channel contents, backwards to rule out a target step the source cannot match.

class Guarded2Network.SeqBuiltins (V : Type u) [ComputableTLAPlus.ExprSemantics V] : Prop

The meaning of Guarded2Network's own sequence expressions, on top of ExprSemantics's value-level sequence vocabulary.

• evalHead {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {M : ComputableTLAPlus.Memory V} {e : ComputablePlusCal.Expression} {τ : ComputableTLAPlus.Typ} {v : V} : ComputableTLAPlus.ExprSemantics.Eval Ξ Ω M (head τ e) v ↔ ∃ (s : V) (vs : List V), ComputableTLAPlus.ExprSemantics.Eval Ξ Ω M e s ∧ ComputableTLAPlus.ExprSemantics.isSeq s (v :: vs)

  Head(e) denotes the first element of the sequence e denotes — and denotes nothing when that sequence is empty, which is what makes an empty inbox block the guard rather than abort the branch.

• evalTail {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {M : ComputableTLAPlus.Memory V} {e : ComputablePlusCal.Expression} {τ : ComputableTLAPlus.Typ} {t : V} : ComputableTLAPlus.ExprSemantics.Eval Ξ Ω M (tail τ e) t ↔ ∃ (s : V) (v : V) (vs : List V), ComputableTLAPlus.ExprSemantics.Eval Ξ Ω M e s ∧ ComputableTLAPlus.ExprSemantics.isSeq s (v :: vs) ∧ ComputableTLAPlus.ExprSemantics.isSeq t vs

  Tail(e) denotes the sequence of everything but that first element.

• evalLenGt {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {M : ComputableTLAPlus.Memory V} {e : ComputablePlusCal.Expression} {τ : ComputableTLAPlus.Typ} {n : ℕ} {s : V} {vs : List V} : ComputableTLAPlus.ExprSemantics.Eval Ξ Ω M e s → ComputableTLAPlus.ExprSemantics.isSeq s vs → ∃ (b : V), ComputableTLAPlus.ExprSemantics.Eval Ξ Ω M (lenGt τ e n) b ∧ ComputableTLAPlus.ExprSemantics.isBool b ∧ (b = ComputableTLAPlus.ExprSemantics.tru ↔ n < vs.length)

  Len(e) > n is a boolean whenever e is a sequence, and is TRUE exactly when that sequence has more than n elements. Two clauses rather than one: the guards this pass emits are awaits, and Statement.aborting's await case distinguishes "evaluates to a non-boolean" (abort) from "evaluates to something other than TRUE" (block), so a proof that the compiled guard never aborts needs the boolean-ness separately from the truth condition.

• evalSeqNil {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {M : ComputableTLAPlus.Memory V} {τ : ComputableTLAPlus.Typ} {s : V} : ComputableTLAPlus.ExprSemantics.Eval Ξ Ω M (ComputableTLAPlus.Expression.seq [] τ) s ↔ ComputableTLAPlus.ExprSemantics.isSeq s []

  The empty-sequence literal <<>> denotes the empty sequence. What Guarded2Network/PlusCal.lean's inbox initializer (.seq [] τ) contributes to the initial state, and so what the refinement invariant starts from.

The three laws at the one argument the pass ever passes them

Every call site builds its sequence expression over the variable inbox, so each law arrives with its inner Eval already determined by a memory lookup. Specialising once here keeps ExprSemantics.evalVar and isSeq_inj out of the refinement proofs, which is otherwise the same four lines at every use.

theorem Guarded2Network.eval_head_inbox {V : Type u} [ComputableTLAPlus.ExprSemantics V] [SeqBuiltins V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {M : ComputableTLAPlus.Memory V} {inbox : String} {τ : ComputableTLAPlus.Typ} {sv v w : V} {vs : List V} (hlk : Finmap.lookup inbox M = some sv) (hseq : ComputableTLAPlus.ExprSemantics.isSeq sv (v :: vs)) : ComputableTLAPlus.ExprSemantics.Eval Ξ Ω M (head τ (ComputableTLAPlus.Expression.var (SurfaceTLAPlus.Typ.seq τ) (TypedTLAPlus.Origin.free inbox))) w ↔ w = v

Head(inbox) denotes the first element inbox holds, and only that. Note the hypothesis has the sequence non-empty: on an empty inbox the law gives no value at all, which is what makes the compiled guard block rather than abort.

theorem Guarded2Network.eval_tail_inbox {V : Type u} [ComputableTLAPlus.ExprSemantics V] [SeqBuiltins V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {M : ComputableTLAPlus.Memory V} {inbox : String} {τ : ComputableTLAPlus.Typ} {sv v t : V} {vs : List V} (hlk : Finmap.lookup inbox M = some sv) (hseq : ComputableTLAPlus.ExprSemantics.isSeq sv (v :: vs)) : ComputableTLAPlus.ExprSemantics.Eval Ξ Ω M (tail τ (ComputableTLAPlus.Expression.var (SurfaceTLAPlus.Typ.seq τ) (TypedTLAPlus.Origin.free inbox))) t ↔ ComputableTLAPlus.ExprSemantics.isSeq t vs

Tail(inbox) denotes the sequence of everything after that first element.

theorem Guarded2Network.eval_lenGt_inbox {V : Type u} [ComputableTLAPlus.ExprSemantics V] [SeqBuiltins V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} {M : ComputableTLAPlus.Memory V} {inbox : String} {τ : ComputableTLAPlus.Typ} {sv : V} {n : ℕ} {vs : List V} (hlk : Finmap.lookup inbox M = some sv) (hseq : ComputableTLAPlus.ExprSemantics.isSeq sv vs) : ∃ (b : V), ComputableTLAPlus.ExprSemantics.Eval Ξ Ω M (lenGt τ (ComputableTLAPlus.Expression.var (SurfaceTLAPlus.Typ.seq τ) (TypedTLAPlus.Origin.free inbox)) n) b ∧ ComputableTLAPlus.ExprSemantics.isBool b ∧ (b = ComputableTLAPlus.ExprSemantics.tru ↔ n < vs.length)

Len(inbox) > n is a boolean, and is TRUE exactly when inbox holds more than n elements.