Statement-level refinement: what Guarded2Network does to a single action statement, and the two
transfer lemmas every later proof leans on.
Evaluation transfer. The pass introduces exactly one name, inbox, and it is fresh
(freshName's $ separator makes collision with a source name impossible). So any source
expression evaluates the same in the target's memory, which differs only at inbox: that is
relatesTo.eval_iff.
Reference arguments. A reference's index path is evaluated by a List.Forall₂ over
EvalStep. Naming that relation — Ref.EvalArgs — and giving it its own congruence lemma keeps
the Forall₂ nesting out of every use site.
Evaluation transfer #
Binding a name the expression cannot read leaves its value alone. The one-name case of
ExprSemantics.evalLocal, which is the only case the pass ever needs: it introduces inbox and
nothing else.
Related states evaluate a source expression to the same values, provided the expression does
not mention inbox — which no source expression does, inbox being freshly generated.
The same for a process that receives nothing: there the memories are equal outright and the freshness hypothesis has nothing to say.
Both cases at once, with the freshness hypothesis stated so that it is vacuous when there is no
mailbox — the form a lemma quantified over an arbitrary mbox needs.
Reference arguments #
A reference's index path, evaluated. Named, rather than left as the raw List.Forall₂ it
unfolds to, so that transferring it between memories is one lemma about EvalArgs instead of a
Forall₂-induction at every use site.
Equations
- Guarded2Network.Ref.EvalArgs Ξ Ω M r path = List.Forall₂ (GuardedPlusCal.EvalStep Ξ Ω M) r.args path
Instances For
A path resolves to at most one value — EvalStep.path_inj, at the named relation.
Every index expression of a reference reads only names the reference itself reads. The bridge
from a freshness fact about a Ref to one about each of its index expressions, which is what
congr_of_fresh needs per Forall₂ step.
A reference whose path resolves has no aborting index. Ref.pathAborts and Ref.EvalArgs
are the two halves of one question — does the access path have a value — so they cannot both hold,
and every place a refinement invariant says the mailbox channel resolves is a place the target's
"index expression has no value" abort is unreachable.
Memories agreeing on everything a reference reads resolve its path identically. The
List.Forall₂ nesting is discharged once, here, and no later proof sees it.
Stated over the names read rather than over a single excepted name, because that is the form a
block needs — a block writes one name per statement, so "all but one" is never the shape on offer
past the first step. congr_of_fresh below is the one-name case.
The one-name case of congr_of_agree: memories agreeing away from inbox resolve a reference's
path identically, provided the reference does not read inbox.
Ref.EvalArgs.congr_of_fresh at related states, with the freshness hypothesis in the guarded
shape — vacuous when the process has no mailbox, where the memories agree outright. The EvalArgs
counterpart of relatesTo.eval_iff', and what keeps a simulation from having to know whether the
process receives before it can move a resolved path across.
Transferring a memory update #
assign (and, on the source side, receive) writes through Memory.update. Simulating that step
means running the same update in the other memory and finding the results still related — which
holds because the two memories agree at the written name, so they read the same old value, compute
the same new one, and insert it.
An update that succeeds in one memory succeeds in any memory agreeing with it at the written
name — both read the same old value and compute the same new one — and the results then agree
there too. Everywhere else the two results agree exactly where the originals did, which is
Memory.lookup_update_ne and needs no hypothesis at all.
An update touches only the name it writes. What keeps the refinement invariant's other
components — the mailbox channel's resolved path, and inbox's own contents — undisturbed by an
assign to some third variable.
An update fails in one memory exactly when it fails in any memory agreeing at the written name:
both read the same old value and run the same updatePath on it. The aborting counterpart of
Memory.update_transfer.
Transporting the relation across a memory write, the third of the transport lemmas
(relatesTo.label_congr and .fifo_push are the other two, in Guarded2Network/Lemmas/ Relation.lean; this one lives here because it needs Ref.EvalArgs.congr_of_fresh).
Both sides write the same name to the same value, which is what assign and with each do. The
name must be neither the generated inbox — else the target's mailbox contents would move — nor one
the mailbox channel is indexed by — else the key the invariant pins would move out from under it.
Both conditions arrive from Fresh already in the guarded shape, so no use site case-splits on
mbox.
Action statements #
convertActionStmt maps each of the seven action constructors to its namesake in the target
language, and the two Statement.reducing definitions agree character-for-character on those
cases (the only differences in the whole def are the type name, one comment, and Guarded's extra
receive case). So the semantics is not merely preserved but definitionally equal, and one
cases … <;> rfl proves each semantic component.
The one name a statement writes, if any. Needed by Fresh below: the refinement invariant pins
one resolved channel key, so a statement that overwrote a variable the mailbox channel is indexed
by would move that key out from under it.
Equations
- Guarded2Network.Statement.writtenName? (GuardedPlusCal.Statement.assign r e) = some r.name
- Guarded2Network.Statement.writtenName? (GuardedPlusCal.Statement.receive c r coe) = some r.name
- Guarded2Network.Statement.writtenName? (GuardedPlusCal.Statement.with x_1 ann bound e) = some x_1
- Guarded2Network.Statement.writtenName? x✝ = none
Instances For
What a statement must avoid for the pass's inbox not to disturb it: it cannot read inbox,
inbox cannot be self — print/send read self to tag the event they emit, which is a name the
semantics reads on its own and so is invisible to a freshness condition stated over the statement's
free variables — it cannot write a name the mailbox channel is indexed by, and it cannot bind
inbox. All hold of any real compilation: freshName's $ separator puts inbox outside the
source program's namespace entirely.
Stated for every guard class, not just the action one: the last clause exists only for with, which
is guard-class, and the block-level refinement needs the same predicate on both halves of a
branch.
Equations
- One or more equations did not get rendered due to their size.
Instances For
assign and send each read one reference and one expression, and Statement.freeVars is the
union of the two halves' free variables. Every branch of the two simulation lemmas below splits
Fresh's first component this way, so the split is named once here.
The workhorse behind action_refines: an action statement's semantics is closed under
relatesTo. Given a target step out of σₜ and a source state related to it, the source takes the
same step — same trace, results still related.
Phrased on one language's semantics because convertActionStmt_reducing' already says the target's
semantics is the source's; action_refines below is what states the result in the framework's own
terms. Each piece built above is spent here: eval_iff' for the statements that evaluate an
expression, relatesTo.evalArgs_iff for those that resolve a reference, Memory.update_transfer
and relatesTo.mem_congr for assign, relatesTo.fifo_push for send, and
relatesTo.label_congr for the four that do none of those.
Nothing here splits on mbox. Every hypothesis Fresh supplies is already guarded by
mbox = .some (c, inbox), and every fact taken off sim — mem_agree', eval_iff',
evalArgs_iff, fifo_split and the transport lemmas — holds in both cases.
The aborting counterpart of reducing'_sim, and the simpler statement: an abort emits nothing,
so the source aborts on the same trace rather than on a prefix of the target's. Each constructor's
abort disjuncts transfer one by one — a failed evaluation stays failed (eval_iff'), an unresolvable
index path stays unresolvable, a missing FIFO stays missing (relatesTo.fifo_lookup_none), and a
failed update stays failed.
The guard class #
Statement.reducing_sim covers the action constructors. The two guard constructors the pass
copies across — with and await — need the same fact, and get their own lemma rather than a
generalization of that one: the third guard constructor is receive, which emphatically does
not preserve relatesTo, and a statement quantified over the class would have to carve it out by
hand at every use.
Statement.reducing_sim for the guard class. await reads an expression and changes nothing;
with additionally binds a name, and the binding is invisible to the invariant exactly because
Fresh says the bound name is neither inbox nor read by the mailbox channel's index path.
Statement.aborting_sim for the guard class. Both constructors abort on exactly two things —
the expression having no value, or having one of the wrong shape — and both transfer by
relatesTo.eval_iff', in the aborting case through ExprSemantics.aborts_congr.
guardAborting'_sim for the blocked case. await blocks on a non-TRUE boolean, with on a
present-but-empty set; both conditions are about the guard expression's value, which
relatesTo.eval_iff' carries across. receive is excluded — its blocking is not relatesTo-stable
(a message can sit in the mailbox unrelayed), and is handled at the algorithm level where the channel
is known drained.
The guard-class statements the two languages share #
with and await exist in both languages with the same fields and the same meaning. There is no
conversion function to state this against — one cannot exist, receive having no image — and
stepStatement writes the target constructor out directly. So what the refinement needs is not
that a conversion preserves semantics but that the two constructors denote the same relation,
which they do on the nose.
Six rfls rather than one lemma over a conversion, and that is the honest shape: the fact is
per-constructor, and the class of statements it covers is not the image of any function.
The two languages' with/await denote the same reducing/aborting/blocking/diverging relation
on the nose — stepStatement writes the target constructor out directly, and there is no conversion
function to state this against (receive has no image).
The two languages' with/await denote the same reducing/aborting/blocking/diverging relation
on the nose — stepStatement writes the target constructor out directly, and there is no conversion
function to state this against (receive has no image).
The two languages' with/await denote the same reducing/aborting/blocking/diverging relation
on the nose — stepStatement writes the target constructor out directly, and there is no conversion
function to state this against (receive has no image).
The two languages' with/await denote the same reducing/aborting/blocking/diverging relation
on the nose — stepStatement writes the target constructor out directly, and there is no conversion
function to state this against (receive has no image).
The two languages' with/await denote the same reducing/aborting/blocking/diverging relation
on the nose — stepStatement writes the target constructor out directly, and there is no conversion
function to state this against (receive has no image).
The two languages' with/await denote the same reducing/aborting/blocking/diverging relation
on the nose — stepStatement writes the target constructor out directly, and there is no conversion
function to state this against (receive has no image).
The two languages' with/await denote the same reducing/aborting/blocking/diverging relation
on the nose — stepStatement writes the target constructor out directly, and there is no conversion
function to state this against (receive has no image).
The two languages' with/await denote the same reducing/aborting/blocking/diverging relation
on the nose — stepStatement writes the target constructor out directly, and there is no conversion
function to state this against (receive has no image).
convertActionStmt refines, statement by statement, at this pass's
own trace relation (equality — Guarded2Network/Lemmas/Trace.lean).
The three components come out very differently. terminating is the whole of reducing'_sim;
aborting is aborting'_sim with the ≼[Rτ] obligation trivial, an abort emitting the empty
trace; diverging is vacuous, a statement having no non-terminating semantics at all — divergence
enters only at the block and algorithm layers.
A with or an await refines itself, the two languages'
constructors denoting the same relation (with_reducing'_eq and friends). Stated on the source
semantics for the same reason action_refines is stated through convertActionStmt: the target's
semantics is the source's, and saying so once keeps the two languages out of the proof.