What processPrecondition does to a branch's guard block.
The pass compiles a receive into an await on the inbox's length plus two consumption
assignments, and it does not emit those assignments where the receive was: they are prepended
to the branch's action block (stepBranch), so they run after every remaining guard. Each such
guard is rewritten on the way past — that is substGuards, and
Guarded2Network/Lemmas/Reorder.lean says the two moves cancel.
This file is the other half: what one receive becomes, in the adjacent ordering where its two
assignments sit immediately after its await. The reorder lemmas turn that ordering into the
emitted one, and the walk applies them one step at a time — the pair a receive contributes is
moved past the following guards by the very steps that compile those guards, so no two orderings
of a whole block are ever related.
Index versus substitution. In the emitted ordering the k-th receive's guard is
Len(inbox) > k, because no assignment has run yet and the inbox still holds every pending
message. In the adjacent ordering the k preceding pairs have already run, the inbox has been
tailed k times, and the guard is Len(inbox) > 0. The two say the same thing, but no
substitution relates them — this pass emits no offset for substGuards to grow — so the bridge
is the semantic reorder_consumption_lenGt below instead.
The last section is the walk itself, as a chain of Hoare triples: stepStatement_spec carries the
refinement-so-far in the state, Spec.mapM_list iterates it over the block, and
processPrecondition_spec reads the block back off the result.
The pass's own inbox syntax, named #
stepStatement builds these as lets inside its receive case. Naming them here is what lets a
lemma be stated against the pass rather than against a transcription of it — the same reason
Lemmas/Reorder.lean names consumptions.
The variable node every sequence expression the pass emits is built over.
Equations
Instances For
The reference the tailed sequence is assigned back through. No index path: inbox is a plain
process-local variable.
Equations
- Guarded2Network.inboxRef inbox τ = { name := inbox, args := [], baseType := SurfaceTLAPlus.Typ.seq τ }
Instances For
The reference the tailed sequence is assigned back through. No index path: inbox is a plain
process-local variable.
The two entries one receive appends to newInstrs: bind the coerced head, then drop it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
What a receive needs of the names around it, in the same shape Lemmas/Statement.lean's
Fresh uses. Four conditions, each earned by construction in a real compilation: the pass's
inbox is generated with a $ separator so no source reference can mention it,
WellFormedness/Restrictions.lean keeps a channel's index path clear of what the branch writes, and
elaboration leaves every index expression of the target reference locally closed (no dangling de
Bruijn), which the consumption assignment's substitution into later guards relies on.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The consumption expression Head(inbox) reads only inbox — its one free variable, so the
Coercion.FreshFor coe {inbox} clause of ReceiveFresh is exactly evalCoerce's side condition.
The two compiled pieces, characterized once #
Both the receive lemmas below and the guard reorder further down take these apart, in both
directions. Stating each once as an ↔ is what keeps either from re-deriving the other's shape.
The compiled guard's step: it changes nothing, emits nothing, and is enabled exactly when the
inbox holds more than n elements.
The compiled guard's blocked step: it is blocked exactly when the inbox holds no more than n
elements. await_lenGt_iff's companion — one is the guard firing, the other its blocking.
One receive's two consumption assignments, as a single step: the inbox must hold at least one
element, the coerced head lands under the reference, and the tail is written back. Note what the pair
does not need — nothing about r's index path relative to inbox, since both orderings evaluate
the assignments at exactly the same two memories. Only r.name ≠ inbox matters, and only so that the
first assignment leaves the inbox for the second to read.
One receive, in the adjacent ordering #
The terminating half. A target run of await Len(inbox) > 0 followed by the two consumption
assignments is matched by the source's receive, or — when the invariant permits an inbox holding
messages over a channel the source has no FIFO for at all — by the source aborting.
Every hypothesis of the source's receive comes from somewhere specific: the channel's resolved
path and the head value from relatesTo's split F₁[c] = inbox ++ F₂[c], the coercion from
evalCoerce run backwards on the assignment's right-hand side, and the reference's own path and
update transferred across the inbox-difference by Ref.EvalArgs.congr_of_fresh and
Memory.update_transfer.
The aborting half. Every way the compiled group can go wrong is a way the source's receive
can, and the source's abort emits nothing — so no trace obligation survives.
Most of the target's abort clauses are unreachable rather than matched, and it is worth saying which
and why. The await cannot abort at all: eval_lenGt_inbox gives its guard both a value and
boolean-ness, which is exactly the pair Statement.aborting's await case rules out. Neither can
the second assignment: inbox is bound (the first assignment writes some other name), Tail has a
value (isSeq_tail), the reference has no index path to resolve, and an empty-path update cannot
fail. What is left is the first assignment's four clauses, which map onto four of the receive's
six.
The blocked half. A target Len(inbox) > 0 that blocks — the inbox is empty — is matched by
the source's receive blocking, provided the mailbox channel is drained too: the invariant gives
F_s(c) = inbox ++ F_t(c), and with inbox empty and F_t(c) empty the source queue is empty,
which is exactly when receive blocks. hdrain is what the algorithm level supplies from
relayBlocking; here it is a hypothesis at the path the invariant resolves the channel to.
The receive elimination, in the framework's own terms: one source receive refines the
group it compiles to — the inbox-length guard, then the two consumption assignments — at this pass's
trace relation. Still the adjacent ordering; reorder_assigns_guard is what moves the assignments to
where the pass actually emits them.
terminating is receive_reducing_sim, aborting is receive_aborting_sim with the ≼[Rτ]
obligation trivial (an abort emits nothing, and the empty trace is a prefix of everything), and
diverging is vacuous: no statement diverges, so the target composite is empty and the framework
supplies that component itself.
The compiled guards' own reorder #
Lemmas/Reorder.lean moves an assignment past a guard by substituting into it. That covers every
guard the source wrote, but not the ones the pass invented: stepStatement emits the k-th
receive's guard as Len(inbox) > k rather than as a substituted Len(Tail…(inbox)) > 0, so no
substitution relates the two orderings there. The equation below is that relation, proved
semantically instead — a consumption pair commutes past a compiled guard by bumping its index.
Moving one consumption pair past a compiled guard costs the guard one on its index: before the
pair the inbox is one element longer, so Len(inbox) > n afterwards is Len(inbox) > n + 1 before.
An equation, with only r.name ≠ inbox assumed. Both sides evaluate the two assignments at exactly
the same pair of memories — only the guard moves — and either side can run at all only if the pair
can, which is what forces the inbox to hold a sequence and makes the Len law apply.
The pair's element type τ and the guard's τ' are independent: each compiled guard carries the
element type of its own channel, and the pending pairs carry theirs. Nothing in the proof couples
them — the type annotation rides along inside the expressions and never reaches the memory.
A compiled guard can only abort where its own consumption pair already does. Len(inbox) > n
has a value whenever inbox holds a sequence (eval_lenGt_inbox), so for it to abort the inbox must
not be readable as one — and then Head(inbox) has no value either (SeqBuiltins.evalHead), which
is one of the four ways assign fails.
This is what spares the aborting reorder a second semantic argument: whatever a guard could have done before the pair ran is already covered by the pair's own first step, so the guard is simply dropped.
The pair's element type τ and the guard's τ' stay independent here for the reason they do in
reorder_consumption_lenGt: evalVar ignores the annotation, so both expressions read the same
memory cell.
One consumption pair past a compiled guard, for the runs that fail.
reorder_consumption_lenGt's aborting twin, and — unlike it — not an equation and not an argument
about indices at all. The guard is a no-op on the runs where it fires, so every failing run of
guard ; pair is a failing run of pair alone; that the guard's own index drops from n + 1 to n
on the far side is then free, because the far side is never reached.
Every pending assignment moved past a compiled guard at once #
reorder_consumption_lenGt moves one pair. What the walk actually meets is the whole accumulator:
stepStatement emits the k-th receive's guard as Len(inbox) > k in a program where the k
earlier pairs have not run yet, and the refinement wants it where they have — at Len(inbox) > 0,
the index receive_refines proves. Moving k pairs across costs the guard k.
That needs to know the accumulator is k pairs, which no type records, hence the predicate below.
What ReceiveState.newInstrs holds after k receives: exactly k consumption pairs over this
inbox, in the order they were appended. Each pair's own channel element type and source span are
its own — only the shared inbox and the target reference being distinct from it matter.
- nil {inbox : String} : ConsumptionPairs inbox 0 []
- snoc {inbox : String} {k : ℕ} {A : List (ComputableGuardedPlusCal.Ref × ComputablePlusCal.Expression × SourceSpan)} {r : ComputableGuardedPlusCal.Ref} {coe : TypedTLAPlus.Coercion} {τ : ComputableTLAPlus.Typ} {pos : SourceSpan} (h : ConsumptionPairs inbox k A) (hne : r.name ≠ inbox) (hcfr : coe.FreshFor {inbox}) (hrLC : ∀ (eᵢ : ComputableTLAPlus.Expression ComputableTLAPlus.Typ), Sum.inr eᵢ ∈ r.args → eᵢ.LC) : ConsumptionPairs inbox (k + 1) (A ++ receiveInstrs r coe inbox τ pos)
Instances For
The consumption assignments processPrecondition emits for an accumulated newInstrs —
Guarded2Network/PlusCal.lean's own st.newInstrs.map …, named so that the reorder lemma and the
precondition spec talk about one list rather than two spellings of it.
The two entries one receive appends to newInstrs: bind the coerced head, then drop it.
inboxVar is a bare free-name node, so trivially locally closed.
Head(e)/Tail(e) are locally closed whenever their argument is: an .opCall of a
.module-headed operator applied to one locally-closed expression.
Head(e)/Tail(e) are locally closed whenever their argument is: an .opCall of a
.module-headed operator applied to one locally-closed expression.
The SubstLC side condition reorder_assigns_guard's family wants, read off a
ConsumptionPairs chain: each pair's right-hand side is a coercion of Head/Tail of the inbox —
locally closed by construction — and each target reference's index expressions are locally closed
because the snoc step carries that (it comes from well-formedness of the source receive).
The whole accumulator past one compiled guard. k pending consumption pairs commute past
Len(inbox) > n, leaving Len(inbox) > n + k in front of them — each pair drops one element from
the inbox, so a guard that ran before them all was asking for k more.
The induction generalizes n: each step hands the next one a guard whose index has already been
bumped.
The whole accumulator past one compiled guard, for the runs that fail.
reorder_pairs_lenGt's aborting twin, and the same induction — Relation.lcomp₁.commute_step takes
the reducing equation the other half already proved, the induction hypothesis one pair further in,
and reorder_consumption_lenGt_abort for the pair itself, and does the algebra once.
The index bookkeeping is the same too: the guard arrives asking for n + (k + 1) and the step hands
its successor n + 1, which is why n is generalized.
One consumption pair past a compiled guard, for the runs that block.
reorder_consumption_lenGt's blocking twin — the guard's index drops one across the pair, since the
pair removes one element from the inbox. Unlike the aborting twin the guard is not a no-op here: it
really moves from Len(inbox) > n + 1 to Len(inbox) > n. The pair supplies the sequence fact
(Head(inbox) has a value only when the inbox is a non-empty sequence), so no separate hypothesis
about the inbox is needed.
The whole accumulator past one compiled guard, for the runs that block.
reorder_pairs_lenGt's blocking twin, the same Relation.lcomp₁.commute_step induction as the
aborting one, with reorder_consumption_lenGt_block for the pair. The ∘ᵣ₁ side is listAborting
throughout: a consumption assignment never blocks, so the only failure the guard's block can become
across the pairs is one of them aborting.
One receive's adjacent target: its inbox-length guard, then the two consumption assignments
it contributes. Named because the walk's receive step meets it twice — once reducing, once
aborting — and because it is receive_refines's target.
Equations
- One or more equations did not get rendered due to their size.
Instances For
One receive's adjacent target: its inbox-length guard, then the two consumption assignments
it contributes. Named because the walk's receive step meets it twice — once reducing, once
aborting — and because it is receive_refines's target.
Equations
- One or more equations did not get rendered due to their size.
Instances For
receive_refines at the two named groups, with the trailing Relation.Idle/∅ the list forms
carry discharged. Nothing new — the same theorem, in the shape the walk's invariant states.
What the walk needs of the source block, in source terms. No with in the block binds a
name that a consumption pair generated by one of the block's receives would read.
Stated over receiveInstrs rather than over the accumulator itself because the accumulator only
exists once the walk has run; AccFresh below is the running form, and this is what re-establishes
it each time a receive grows the accumulator.
A syntactic freshness condition, so it stays a hypothesis — discharging it needs well-scopedness and
the passes before this one. WellScopedIn requires a with's bound name to be absent from the
enclosing scope, and everything a pair reads — the inbox, and the Head/Tail operator names that
Expression.freeVars counts like any other variable — is in that scope.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Fewer statements can only make the condition easier: it quantifies over pairs drawn from the list on both sides. What lets the walk hand each step the condition for the suffix it is looking at.
A compiled guard is an await or a with — everything stepStatement emits. Named so the
blocking clause of WalkInv and its fifo-locality argument can quantify over it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Substituting into a guard leaves it a guard — substGuardStmt maps await/with to await/
with.
The mailbox channel is empty, at whatever path its args resolve to in the state's memory —
the target-state shadow of relayBlocking, and what makes a receive's blocking transfer across
relatesTo. Restricts the target reduce set of the walk's blocking clause,
{x ∈ listBlocking results | Drained mbox x}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
rfresh assembled from its two sources. The receive half comes from well-formedness, where
the executable restriction checks put it; the two conditions on the generated inbox come from
whoever generated it, which is Thread.toNetwork and not this file.
The split is deliberate and follows the shape of the problem: one half is a property of the source
program that a front-end pass rejects, the other is a property of a name this pass invents. Nothing
in Algorithm.WellScoped could establish the second — inbox does not occur in the source at
all.
The statements of a branch's precondition, [] when it has none. What the freshness hypotheses
below quantify over — Block.toList cannot, an Option having no toList of the right shape.
Equations
Instances For
The precondition's blockBlocking as a list — Block.aborting_eq_listAborting at
preconditionList, both cases of the Option.
The precondition's blockBlocking as a list — Block.aborting_eq_listAborting at
preconditionList, both cases of the Option.
The Network side: the compiled block's blockBlocking as a list over its toList.