Network PlusCal's own semantic equations, mirroring GuardedPlusCal.Semantics.Lemmas at this
language's Statement.reducing/.aborting/.diverging.
Everything generic — the Block.reducing/.aborting/.diverging equations — lives in
GuardedPlusCal's own semantic lemmas and is used here, not restated: LocalState is shared
between the two languages unchanged, so a refinement relates a GuardedPlusCal block to a
NetworkPlusCal one over that one state type directly, with no encoding to transport across
first.
Constructor-intro lemmas — see GuardedPlusCal.Semantics.Lemmas's Intro section for why #
these exist and why they're duplicated per language rather than shared. No receive here — that
is this language's whole point.
Constructor-elim lemmas #
The mirror image of the section above, for the three constructors Guarded2Network's reorder
lemmas (Guarded2Network/Lemmas/Reorder.lean) have to take apart rather than build: commuting an
assignment past a guard means reading both composites' membership down to their components. A
proof outside this file must not unfold Statement.reducing to do that (LEAN_STYLE.md), so the
decomposition is named here, where the definition lives.
Only the constructors that pass actually needs, and only for this language — the reorder happens
entirely on the target side. Each is := h for the same reason its .intro twin is: the
hypothesis and the conclusion are the same proposition, one written as Set membership and one as
the body that membership unfolds to. Not in the sem rule set: these run backwards, and aesop
applying an elimination lemma to a goal is not what that set is for.
Stated as a bare implication rather than with a named hypothesis, unlike its siblings below:
bound's match sits in the conclusion here, and a hypothesis mentioning bound gets generalized
into that match's motive (match bound, h with), which then no longer matches the definition.
Statement.aborting.with.elim is the same case.
Stated as a bare implication rather than with a named hypothesis, unlike its siblings below:
bound's match sits in the conclusion here, and a hypothesis mentioning bound gets generalized
into that match's motive (match bound, h with), which then no longer matches the definition.
Statement.aborting.with.elim is the same case.
Which values a with may bind, as a predicate on the value instead of a match on bound:
true (a let) admits the expression's own value, false (a nondeterministic pick) any member of
it. Neither the memory nor the FIFOs enter that choice, and that is the whole content of the two
.iff lemmas below.
Equations
Instances For
with's reducing case with the bound match pulled out into BoundValue: one existential over
the value that lands in memory, no case split. .elim above mirrors the definition; this mirrors
what consumers actually do with it. Guarded2Network/Lemmas/Reorder.lean moves this clause between
two memories in both directions, and without the factoring that is four near-identical blocks.
with's aborting case, factored the same way: the state and trace are fixed by the statement,
and what remains is either the guard expression having no value at all or — only under a
nondeterministic pick — its value not being a set. bound = true cannot abort past evaluation,
which the definition says with a False branch and this says by pinning bound to false.
await's aborting case with the state and trace matched once instead of once per union member,
leaving a plain disjunction over what actually went wrong.
assign's aborting case, same factoring: one state match, then the four ways an assignment can
fail — the target name unbound, the right-hand side without a value, an index expression of the
reference without a value, or the update itself rejected by updatePath. Four union members each
repeating σ = ⟨M, F, .none⟩ ∧ ε = 1 is what makes the raw form expensive to take apart.
Statement.listReducing's two equations, so a proof about a generated statement run inducts on
the list without reaching through the wrapper to Block.listReducing.
A statement run splits wherever its list does. Guarded2Network's consumption assignments
accumulate by ++ — one receive appends its pair to what earlier ones left — so every proof about
them meets this shape rather than a cons.
A statement run splits wherever its list does. Guarded2Network's consumption assignments
accumulate by ++ — one receive appends its pair to what earlier ones left — so every proof about
them meets this shape rather than a cons.
A statement run splits wherever its list does. Guarded2Network's consumption assignments
accumulate by ++ — one receive appends its pair to what earlier ones left — so every proof about
them meets this shape rather than a cons.
A blocked guard emits nothing — the Network twin of
GuardedPlusCal.Statement.blocking_trace_eq_one.
No execution statement blocks, so no block of them does — the Network twin of
GuardedPlusCal.Statement.blockBlocking_eq_empty.
A branch is blocked exactly when its precondition is — the Network twin of
GuardedPlusCal.AtomicBranch.blocking_eq_precondition.
A list of Network guards is silent throughout — the twin of
GuardedPlusCal.Statement.listBlocking_trace_eq_one.
A blocked branch emits nothing — the Network twin of
GuardedPlusCal.AtomicBranch.blocking_trace_eq_one.
An await that fires changes nothing and emits nothing, so its step relation sits inside
Relation.Idle. What lets a guard be dropped off the front of a run that fails after it.
What the flat encoding used to bridge #
Now that LocalState itself is flat, a refinement proof needs no translation between an indexed
and a flat state — Statement.reducing/.aborting already are the shape StrongRefinement wants.
What survives from the old bridging section are the facts genuinely about this language: no
statement or block diverges, a branch's aborting in the uniform composed shape a
StrongRefinement.Comp produces, and that a step never removes a channel from the map.
No statement diverges.
No block diverges either — Statement.diverging_eq_empty propagated through the fold.
The match on the precondition, discharged — see GuardedPlusCal.AtomicBranch.aborting_eq.
A branch ends at the label its terminal goto names. AtomicBranch.reducing composes the
precondition onto the action block, and the action block composes its begin onto its last, so the
final state is whatever last produced — and goto is the only statement that produces a label at
all (it is the only terminal constructor, Core/GuardedPlusCal/Syntax.lean).
Stated with the goto's target supplied rather than existentially, because every caller already
knows it: it is read off the source branch through BranchRefines.last_eq, and what is wanted is
that the step agrees with it. This is what lets a caller rule out where a compiled block can jump to
without inspecting the run — Guarded2Network's ProcessRefines.exits, which needs a compiled
code thread never to land on a receiving thread's label.
A statement never removes a channel. send is the only constructor that writes the map, and
it writes at a key it has just read, so its insert only ever overwrites.
Nor does a block. One Statement.reducing_fifos_mem per step of the same left-to-right
induction the locality argument runs.
Nor a branch, precondition and action together — a missing precondition being
Relation.Idle, which writes nothing.