Semantic equations for Guarded PlusCal: how Block.reducing/.aborting/.diverging decompose
along Block's list-like interface (end/cons/concat/prepend), and how they commute with an
injective relabelling of the state type.
Everything here is about this language's own semantics, not about the relationship between Guarded and Network PlusCal.
Nothing in this file mentions values or the expression layer: the Block combinators are generic
over the statement family α, the state family β, and the behavior monoid γ, so
NetworkPlusCal's own semantics reuses these lemmas verbatim rather than restating them.
There are no Reduce/Abort/Diverge instances resolving the semantics behind a notation, so
each lemma takes the step relation explicitly.
How much is queued #
The measure a divergence argument needs. A receiving thread's relay moves one message out of a
channel and into a process's inbox, so it strictly decreases the total; only a send increases
it. A target run that relays forever without ever sending is therefore impossible — which is what
says a target cannot diverge on .rx steps alone, and so what lets a source answering those steps
with no step of its own still be said to diverge.
How many messages are queued, across every channel at once.
Equations
- F.size = ∑ k ∈ Finmap.keys F, ((Finmap.lookup k F).getD []).length
Instances For
Popping the head of one queue drops the count by exactly one. The relay's effect on the
measure, and the only fact about FIFOs.size anything needs.
Path resolution is deterministic #
Ref.args resolves to a List (PathStep V) through EvalStep, and a ChanKey is a channel's
name paired with that list — so a reference names the FIFO it reads only if the resolution is
unique. It is, because ExprSemantics.evalUnique says an expression has at most one value; the
two lemmas below are that fact lifted over one segment and over a whole path.
One path segment resolves to at most one PathStep.
A whole Ref.args resolves to at most one path.
List.Forall₂ (EvalStep Ξ Ω M) and ComputableTLAPlus.ResolvesPath are one relation in two shapes.
The statement semantics resolves a Ref.args with the former; ExprSemantics.evalExcept states the
EXCEPT law against the latter, having been declared before EvalStep exists. Nothing else bridges
them, so anything relating an assign to the substitution standing for it
(Guarded2Network/Lemmas/Reorder.lean) passes through here.
A list of reference segments resolves exactly when each of its index expressions has a value.
The list-level content of Ref.not_pathAborts_iff below, separate because the induction runs on the
list while Ref.pathAborts is stated about a whole Ref.
Ref.pathAborts with the filterMap gone: some index segment of the reference has no value.
The definition filters the .inr segments out of Ref.args to say that; every consumer wants the
membership back in terms of Ref.args itself, which is what Ref.freeVars's own lemmas are stated
against.
The positive reading of "the path does not abort": every index segment has a value, so the whole
Ref.args resolves. Eval being a relation is what makes this classical — "has no derivation" only
yields a value by excluded middle — and it is what lets an assign be shown to step whenever it
does not abort (Guarded2Network/Lemmas/Reorder.lean).
Constructor-intro lemmas #
Restate each constructor's Statement.reducing/.aborting case as a named lemma whose
hypothesis is exactly that case's own body — proved by trivial (the two sides are defeq).
Exist so a caller can apply a fixed name per constructor instead of unfolding the raw
Set-membership definition inline. multicast has no semantics yet, and no aborting counterpart
for skip/goto exists, since both are always ∅ there.
Duplicated between GuardedPlusCal/NetworkPlusCal rather than stated once generically:
Statement.reducing/.aborting are two separate defs (one per language, on two separate
inductives), and the proof is trivial either way — not worth a shared-idle/test refactor
of Semantics/Denotational.lean for.
Reduction #
A non-terminal block is its own statement list. The two are the same fold; this is the only
place that has to say so, and it is what lets a proof about a Block be carried out on
Block.toList — which is the shape a pass's walk over the block produces.
Abortion and divergence #
aborting and diverging share their shape exactly — both are "this element goes wrong, or it
steps and the rest does" — so the two families of lemmas below are literal mirrors of each other.
A run goes wrong wherever its list splits: either the prefix does, or it runs and the suffix
does. Block.listReducing_append's twin, and every Block equation below is this one plus
Relation.lcomp₁.union_lcomp₂.
A run goes wrong wherever its list splits: either the prefix does, or it runs and the suffix
does. Block.listReducing_append's twin, and every Block equation below is this one plus
Relation.lcomp₁.union_lcomp₂.
A non-terminal block is its own statement list. The two are the same fold; this is the only
place that has to say so, and it is what lets a proof about a Block be carried out on
Block.toList — which is the shape a pass's walk over the block produces.
A prefixed block goes wrong either inside the prefix or, having run it, inside the block. The
shape a refinement against a block whose prefix a pass generated (Guarded2Network's consumption
assignments) is stated in.
Block.diverging is Block.aborting. "This element goes wrong, or it steps and the rest
does" is one shape, and the two definitions spell it identically. Saying it as an equation is what
keeps the two families of lemmas below
from drifting apart — each is now the aborting one under the diverging name, and none of them is a
second proof.
A non-terminal block is its own statement list. The two are the same fold; this is the only
place that has to say so, and it is what lets a proof about a Block be carried out on
Block.toList — which is the shape a pass's walk over the block produces.
A prefixed block goes wrong either inside the prefix or, having run it, inside the block. The
shape a refinement against a block whose prefix a pass generated (Guarded2Network's consumption
assignments) is stated in.
If nothing at the leaf diverges, nothing built from it does either — propagated through the
fold. What lets a language whose statements never diverge (Statement.diverging = ∅, both
GuardedPlusCal and NetworkPlusCal) conclude the same fact at block shape without restating the
induction once per language.
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, and a branch's aborting in the uniform composed shape a
StrongRefinement.Comp produces.
No statement diverges.
No block diverges either — Statement.diverging_eq_empty propagated through the fold.
A possibly-empty list of Guarded statements — see NetworkPlusCal.Statement.listReducing,
which this mirrors. Guarded2Network's per-statement reorder lemmas lift to a list of consumption
assignments through this wrapper, on the Guarded side exactly as on the Network one.
Equations
- GuardedPlusCal.Statement.listReducing Ξ Ω A = GuardedPlusCal.Block.listReducing (fun ⦃x : Bool⦄ => GuardedPlusCal.Statement.reducing Ξ Ω) A
Instances For
A possibly-empty list of Guarded statements — see NetworkPlusCal.Statement.listReducing,
which this mirrors. Guarded2Network's per-statement reorder lemmas lift to a list of consumption
assignments through this wrapper, on the Guarded side exactly as on the Network one.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A statement run splits wherever its list does — Block.listReducing_append at a statement
list.
A statement run splits wherever its list does — Block.listReducing_append at a statement
list.
A possibly-empty list of Guarded guards, blocked: some prefix reduces to a state at which the
next guard blocks. Block.listAborting at the blocking/reducing leaves — the list counterpart of
Statement.blockBlocking, mirroring Statement.listAborting.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A statement run splits wherever its list does — Block.listReducing_append at a statement
list.
A blocked guard emits nothing — every case of Statement.blocking fixes the trace at 1.
A guard's reducing step emits nothing — await/with/receive are all silent.
Going wrong in a guard emits nothing — every case of Statement.aborting at guard class fixes
the trace at 1.
And a blocked guard block emits nothing — the list of guards is silent throughout.
Going wrong in a guard list emits nothing — every guard, whether it steps or aborts, is silent.
A blocked branch's abort — which is entirely in its (guard) precondition — is silent.
No execution statement blocks — Statement.blocking is ∅ at guard class false — so no block
of them does either. What lets a branch's blocking semantics forget its action entirely.
The match on the precondition, discharged, for blocking: the action block never blocks
(Statement.blockBlocking_eq_empty), so a branch is blocked exactly when its precondition is. The
counterpart of AtomicBranch.aborting_eq.
A blocked branch emits nothing — its precondition is all guards, and guards are silent.
The match on the precondition, discharged: .none composes with the identity relation and
contributes no aborting runs of its own, which is exactly what Option.elim says. The uniform form
is what a StrongRefinement.Comp of a precondition half and an action half produces, so this is the
bridge between the definition and every proof about it.