Commuting an assignment past a guard.
processPrecondition compiles a receive into an await on the inbox plus two consumption
assignments, and those assignments are not emitted where the receive was: they are prepended to
the branch's action block, so they end up after every guard the precondition still has to run
(stepBranch). What keeps that sound is that each guard is rewritten on the way past —
substGuards substitutes every already-processed assignment's effect into it. This file says
those two moves cancel.
The guard constructor is not split on: with and await differ only in which field carries the
guard expression. The split that remains is the real one — reducing and aborting are different
statements, and only the first is an equation.
The pass's substitution, and what it does to evaluation #
substGuardStmt's with case. Stated here rather than in Guarded2Network/PlusCal.lean for the
same reason convertActionStmt's semantic equations are (Guarded2Network/Lemmas/Statement.lean):
the pass file holds the pass, the proof files hold what is proved about it.
substGuardStmt's with case. Stated here rather than in Guarded2Network/PlusCal.lean for the
same reason convertActionStmt's semantic equations are (Guarded2Network/Lemmas/Statement.lean):
the pass file holds the pass, the proof files hold what is proved about it.
No assignments accumulated yet, so nothing is substituted.
substGuards peels its head first — it is a foldr, so the first accumulated assignment is
the outermost substitution. That direction is what makes the iterated reorder below come out: the
assignments run left to right, and each one is pushed past the guard in the order it was emitted.
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.
Equations
- One or more equations did not get rendered due to their size.
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 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.
Every statement consumptions emits is an assignment — the trivial reading of its definition,
in the shape NetworkPlusCal.Statement.listReducing_fifos_of_assigns asks for.
What Expression.substRef r rhs needs of its inputs to be sound: the right-hand side is
locally closed, and so is every index expression of the reference (a compound r splices them into
the synthesized EXCEPT). ExprSemantics.evalSubstRef's two Expression.LC premises, bundled so
the reorder lemmas thread one hypothesis. Independent of the guard, so it passes through
substGuardStmt/substGuards untouched.
Equations
- Guarded2Network.SubstLC r rhs = (ComputableTLAPlus.Expression.LC rhs ∧ ∀ (eᵢ : ComputablePlusCal.Expression), Sum.inr eᵢ ∈ r.args → ComputableTLAPlus.Expression.LC eᵢ)
Instances For
ExprSemantics.evalSubstRef at the shape the statement semantics writes reference paths in —
List.Forall₂ (EvalStep M) rather than ResolvesPath, bridged by EvalStep.resolvesPath_iff. Every
branch of the two reorder lemmas needs the transfer in this form, so the conversion happens once.
The same transfer for a guard that has no value at all: an assignment cannot make an expression start or stop aborting, once the substitution has been applied to it.
Freshness #
Only the with case has a side condition, and only one: the name it binds. The bound name is
written into the memory the assignment also writes, so unless the two names are distinct the writes
do not commute; and it is in scope for the assignment's own right-hand side on one side of the
equation but not the other. await binds nothing and needs neither.
What a guard statement must avoid for an assignment to commute past it. Phrased as an
implication from S's shape rather than by cases on S, so a caller that does not know which
constructor it has can still discharge it — the same shape Guarded2Network/Lemmas/Statement.lean's
Fresh uses for the mailbox.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Substitution leaves a guard's freshness alone: substGuardStmt rewrites the guard expression
and nothing else, so the bound name a with carries — the only thing GuardFresh looks at — comes
through unchanged. What lets the iterated reorder discharge each step's side condition from the
hypothesis about the original statement.
Substitution leaves a guard's freshness alone: substGuardStmt rewrites the guard expression
and nothing else, so the bound name a with carries — the only thing GuardFresh looks at — comes
through unchanged. What lets the iterated reorder discharge each step's side condition from the
hypothesis about the original statement.
Two memories differing only at x agree away from x — Ref.EvalArgs.congr_of_fresh's
hypothesis, at the one shape a with produces it in.
A reference's own name is one of the names it reads, so freshness against the whole reference already says the bound name is not the one being written.
Memories agreeing away from a name the reference does not read cannot disagree about whether its
path resolves. Every index expression of the reference reads only names the reference reads
(Ref.freeVars_of_mem_args), so evalLocal applies segment by segment.
Memories agreeing away from a name the reference does not read cannot disagree about whether its
path resolves. Every index expression of the reference reads only names the reference reads
(Ref.freeVars_of_mem_args), so evalLocal applies segment by segment.
An assignment either aborts or takes a step. The four aborting clauses are jointly the exact
complement of "the reference resolves, the right-hand side has a value, and the update succeeds", so
assign has no third, blocking outcome — unlike a guard, which is why the aborting reorder below
is an inclusion where the reducing one is an equation. Classical, twice over: Aborts and
Ref.not_pathAborts_iff both turn "no derivation exists" into a value.
Binding a name the assignment neither reads nor writes cannot make it abort — each of the four
clauses transfers back to the unbound memory. Only this direction is needed: the aborting reorder
moves an abort that happened after a with's bind to before it.
The pair #
Reducing. An assignment commutes with a following guard, provided the guard's substituted form is what runs on the other side. An equation, not an inclusion: every run of one side is a run of the other, with the same trace — both sides take two silent steps.
The with case is where Memory being a Finmap is load-bearing. The two sides bind the same two
names to the same two values in opposite orders, so the memories they reach are equal only once
insertion order stops being observable (ComputableTLAPlus.Memory).
Iterated. The pass never substitutes one assignment: substGuards folds every
consumption assignment accumulated so far into the guard, and emits them, in list order, after it. So
the single-assignment equation lifts to the whole list — which is the form
stepPrecondition's proof needs, substGuards being what stepStatement applies.
The foldr in substGuards is what makes the induction come out: its head is the outermost
substitution and the first assignment to run, so peeling one entry peels one factor off each side
at once.
An await binds nothing, so nothing can clash with it. GuardFresh's whole content is about a
with's binder; on the other guard constructor it holds outright.
reorder_assign_guard, restated under its old "flat encoding" name. Now that LocalState
itself is flat, the two statements are the same fact word for word — nothing to bridge. Kept as a
separate name only because reorder_assigns_guard' below still calls it that; not worth a rename
sweep across every call site in this phase.
reorder_assigns_guard in the flat encoding. The list induction is redone rather than
transported: the unprimed-to-primed bridge is stated for a composition of two statements, and a
list has no such shape at its nil end — Relation.Idle on LocalState relates states carrying a
label, which no image of an unprimed relation ever does. Each step of the induction does have the
shape, which is why this proof is the unprimed one verbatim with reorder_assign_guard' swapped
in.
Aborting. The same commutation for the runs that fail — and here only an inclusion. Every
way the compiled order guard[subst] ; assign can abort is a way the source order assign ; guard
can, but not conversely: a guard has a third outcome an assignment does not, since it can block. A
state where the assignment aborts and the substituted guard blocks is a source abort and not a target
one, so the two sets are not equal.
Each union member is handled once. A target abort in the guard becomes a source assignment step
followed by the same abort, or an abort of that assignment (assign_aborts_or_steps — there is no
third case). A target abort in the assignment becomes an immediate source abort, the guard having
no way to change whether the assignment fails.
reorder_assign_guard_abort, restated under its old "flat encoding" name — see
reorder_assign_guard' for why the name survives unrenamed.
The whole accumulator past one source-written guard, for the runs that fail.
reorder_assigns_guard''s aborting twin, and an inclusion for the same reason the one-assignment
case is: the compiled order can only abort where the source order can.
The induction is reorder_assigns_guard''s, with Relation.lcomp₁.commute_step in place of the
rw chain — the algebra of moving an abort set past a composition is the same at every step, and
saying it once is what keeps the two orderings' bookkeeping out of this proof.
One consumption pair past a source-written guard, for the runs that block.
reorder_assign_guard_abort's blocking twin. Blocking is terminal — the guard never reaches the
assignment — so the only input is the substituted guard blocking, and it becomes either the
assignment aborting (it could not run) or the assignment running and the plain guard blocking after
(assign_aborts_or_steps — the substitution is the assignment).
The whole accumulator past one source-written guard, for the runs that block.
reorder_assigns_guard_abort''s blocking twin — the accumulated pairs either abort somewhere or run
in full and leave the plain guard blocking.
The consumption assignments are total. From any state, the whole list either reduces to some
state or aborts — an assign has no third outcome (assign_aborts_or_steps), and the fifo map is
untouched throughout. What the blocking walk feeds WalkInv's reducing/aborting refinement: at the
point a compiled guard blocks, the pending pairs have not run, and this is how they are completed so
the refinement applies.