The refinement invariant relating a GuardedPlusCal local state to the NetworkPlusCal state
the pass compiles it into, and the named API every later lemma reaches it through.
What it says. Everything is equal except the one channel the process receives from and the
inbox the pass introduced for it. There, the target has already drained some prefix of the
channel into inbox, so the source's FIFO is the target's inbox followed by the target's FIFO —
F₁[c] = inbox ++ F₂[c]. That single equation is what carries reception across the pass: since
reception is not an observable event (see Behavior in Core/GuardedPlusCal/Semantics/ Denotational.lean), nothing in the trace records where a message went, and this invariant is the
only place saying it went nowhere else.
One channel, not a channel per shape. WellFormedness/Restrictions.lean's
checkReceiveChannels establishes that a process receives from exactly one channel, so mbox
carries one Ref — none for a process that never receives, in which case the two states are
equal outright. The channel is a Ref (name plus an already-resolvable index path) rather than
a raw Expression, so the two syntactic cases c and c[self] collapse into one: EvalStep
resolves Ref.args uniformly, whether the list is empty or not.
Why an API and not a raw ∧-chain. Each projection below names one coordinate of the predicate,
so no proof has to navigate it positionally. A conv … enter into a conjunction is a
rw [show … from rfl] in disguise: it silently depends on the order the conjuncts happen to be
written in, and every reordering of this definition would break proofs that never mention it.
The channel a process receives from, paired with the inbox variable Guarded2Network gave it
— none when the process contains no receive at all and so got neither.
Instances For
Relates a GuardedPlusCal state to the NetworkPlusCal state refining it. Both languages
share one state space (Core/NetworkPlusCal/Semantics/Denotational.lean), so this is a relation on
one type; the ₛ/ₜ naming is what keeps the two roles apart.
Two roles, two treatments. At every channel other than this process's own, the source's queue
is the target's with pref k in front — some other instance's inbox, which this process cannot
observe. That prefix is a parameter rather than an existential on purpose: the algorithm level
needs those keys to come back unchanged after a block runs, and "the same pref on both sides" is
the only way to say so. An existential would let the conclusion re-witness, and the fact would be
true but unstatable. Stating the clause as plain equality (pref k = []) is false as soon as a
second instance receives.
At this process's own channel the prefix is its inbox, tied to the target's memory by
isSeq sv vs and existential — because it is the one prefix the process itself changes, a receive
shrinking it. Keeping it out of pref is what leaves the relation closed under receive, so the
block layer's refinement stays a single-relation StrongRefinement.
A send is insensitive to either — it appends at the back, behind whatever prefix is in front.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Relates a GuardedPlusCal state to the NetworkPlusCal state refining it. Both languages
share one state space (Core/NetworkPlusCal/Semantics/Denotational.lean), so this is a relation on
one type; the ₛ/ₜ naming is what keeps the two roles apart.
Two roles, two treatments. At every channel other than this process's own, the source's queue
is the target's with pref k in front — some other instance's inbox, which this process cannot
observe. That prefix is a parameter rather than an existential on purpose: the algorithm level
needs those keys to come back unchanged after a block runs, and "the same pref on both sides" is
the only way to say so. An existential would let the conclusion re-witness, and the fact would be
true but unstatable. Stating the clause as plain equality (pref k = []) is false as soon as a
second instance receives.
At this process's own channel the prefix is its inbox, tied to the target's memory by
isSeq sv vs and existential — because it is the one prefix the process itself changes, a receive
shrinking it. Keeping it out of pref is what leaves the relation closed under receive, so the
block layer's refinement stays a single-relation StrongRefinement.
A send is insensitive to either — it appends at the back, behind whatever prefix is in front.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Introduction #
A process with no receive has a memory equal to the source's. Its channels still carry the
prefixes other instances have drained, which is why the FIFO hypothesis is not equality.
The receiving case, one hypothesis per conjunct — the introduction form every construction site uses instead of assembling the nested anonymous constructor by hand.
Projections #
One per conjunct, in definition order. label_eq is the only one that holds in both cases, which
is why it sits outside the match in the definition: a block-level lemma needs it without knowing
whether the process receives at all.
Source and target agree on which label the block ended at — in both cases of mbox.
With no mailbox, the memories are equal.
With no mailbox there is no own channel to except, so every key carries pref.
Memory agreement in both cases at once: away from the generated inbox — of which there is none
when the process never receives — the memories agree. This is what lets a simulation over an
arbitrary mbox stop case-splitting on the mailbox to read the memory half.
The equation the whole proof turns on, read uniformly: at every key the source's queue is
the target's behind some prefix — this process's own inbox at its own channel, pref k at every
other. Reception has no trace event, so this is the only statement that a message the target moved
out of a channel is still accounted for.
The prefix is existential because which of the two clauses applies depends on the key, and no
statement below receive cares which. Where a proof needs the prefix pinned it takes the clause it
wants directly, through inbox_seq.
Transport #
A statement-level simulation ends by rebuilding the relation over the state its step produced. Each
kind of change is invisible to some part of the relation, and saying which part once — here, rather
than per constructor — is what lets those proofs stop case-splitting on mbox.
Transporting the FIFO half. A change that keeps every key's prefix working keeps the
relation: the hypothesis is stated over an arbitrary prefix so that one instance of it serves both
FIFO clauses — pref k away from this process's channel, its inbox at it.
Moving both states to the same label. The label sits outside the match precisely so that this
holds without knowing whether the process receives, and the statements that neither write memory nor
push a queue are exactly this lemma.
The queue a send writes to exists in the source exactly when it exists in the target, and
holds the target's contents behind whatever this key's prefix is. Supplies fifo_push's ws.
And the aborting direction: a queue missing in the target is missing in the source, which is
what carries send's "no such channel" abort across the pass.
A send, and the reason the prefix costs nothing: it appends at the back of a queue, behind
whatever has been drained off the front, so the same value lands after the same prefix on both
sides. The key sent to needs no comparison with this process's own channel — the prefix ws is
whichever of the two clauses applies, and the two lookups pin it.
The memories agree on every name but inbox — the pass introduces exactly one variable, and
freshName is what makes "every name but that one" a statement about the source program's names at
all.
This process's own channel, in one package: where it resolves to, what its inbox holds, and
the two FIFO clauses — pref away from that key, the inbox at it. Everything below is stated
against the same cpath this produces, so a proof destructures it once and reuses the witnesses.
The split at this process's own channel, read off a resolved path already in hand.
EvalStep.path_inj is what makes "this process's channel" well defined.
The algorithm level #
relatesTo relates one atomic block's local state. ≋ relates a whole AlgState: every process
instance's own state, plus the one FIFO map they all share.
What the shared FIFO map costs. Each instance has drained a prefix of its own channel into
its own inbox, so the source's FIFO map is the target's with each instance's inbox prepended
to that instance's key — one prepend per key, provided no two instances share a key. They do not:
a process set must index its channel by self (WellFormednessError.mailboxNotIndexedBySelf),
which is exactly what makes keys_inj below hold rather than being an extra hypothesis dragged
through the proof. Without it the source queue at a shared key would have to be some interleaving
of several inboxes with nothing fixing the order, and no relation of this shape could be written
at all.
Why the witnesses are a function, not an existential per instance. InboxState bundles the
key an instance receives on with what its inbox currently holds. Quantifying ib : ι → Option (InboxState V) once, outside the per-instance clauses, is what lets the FIFO clauses talk about
all keys at once — an existential inside each instance's clause would give each instance its own
witness with nothing relating them, and the map-level statement could not be phrased.
Labels. The target has the source's threads plus one .rx thread per channel, but a .rx
thread owns no label and its step leaves the scheduled set untouched, so the two label sets are
equal — procRelatesTo's L₂ = L₁.
What one instance's inbox accounts for: the FIFO key it receives on, and the values it has
already taken off that FIFO but not yet consumed.
- key : GuardedPlusCal.ChanKey V
The resolved key of the channel this instance receives on.
- contents : List V
What the instance's
inboxcurrently holds, in FIFO order.
Instances For
One process instance's state, related. ib is none exactly when mb is: an instance with no
receive got no inbox, and its memory is equal to the source's rather than equal-off-inbox. The
scheduled labels are equal — a .rx thread owns none, so the target adds nothing to the set.
Equations
Instances For
Memory agreement at one instance, in both cases of the mailbox at once — relatesTo.mem_agree'
one level up, and stated the same way so that a caller need not know whether the process receives.
What the algorithm level reads through it is selfName: a process only steps in a memory binding its
own identity (CodeTable.procReducing), the target's does, and the source's agrees with it there
because the pass's generated inbox is not self.
The algorithm-level lift of relatesTo: same instances, each instance's state related, and one
FIFO map split per key.
The split is carried by a pref function — the same one relatesTo takes — with two clauses tying
it to ib: at a key some instance receives on it is that instance's inbox, and where nobody
receives it is empty. That is what makes picking a process hand relatesTo its pref directly,
with no bridge: relatesTo reads pref at every key but the picked process's own, where it uses
its own inbox instead — which is exactly the clause ib already pins.
A key an instance receives on names a channel that exists, and that is not bookkeeping either.
The target's receiving thread aborts on a channel resolving to no FIFO, and the source has no such
thread to abort with — so at a state where an instance's key is absent the aborting half of the
refinement is false. Nothing removes a key (NetworkPlusCal.AtomicBranch.reducing_fifos_mem), so
this rides along; establishing it initially is Algorithm.init's business.
No functionality clause. Instances is ι → Option (ProcState V), so "at most one state per
instance" is definitional on both sides — nothing to carry. The one clause that does still need
stating is that the two sides agree on which instances exist and how they relate, which is the
match below: Ps p/Qs p are either both absent or both present and procRelatesTo-related.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The algorithm-level lift of relatesTo: same instances, each instance's state related, and one
FIFO map split per key.
The split is carried by a pref function — the same one relatesTo takes — with two clauses tying
it to ib: at a key some instance receives on it is that instance's inbox, and where nobody
receives it is empty. That is what makes picking a process hand relatesTo its pref directly,
with no bridge: relatesTo reads pref at every key but the picked process's own, where it uses
its own inbox instead — which is exactly the clause ib already pins.
A key an instance receives on names a channel that exists, and that is not bookkeeping either.
The target's receiving thread aborts on a channel resolving to no FIFO, and the source has no such
thread to abort with — so at a state where an instance's key is absent the aborting half of the
refinement is false. Nothing removes a key (NetworkPlusCal.AtomicBranch.reducing_fifos_mem), so
this rides along; establishing it initially is Algorithm.init's business.
No functionality clause. Instances is ι → Option (ProcState V), so "at most one state per
instance" is definitional on both sides — nothing to carry. The one clause that does still need
stating is that the two sides agree on which instances exist and how they relate, which is the
match below: Ps p/Qs p are either both absent or both present and procRelatesTo-related.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every source instance has a related target instance.
Every target instance has a related source instance — the direction that rules out the target inventing an instance the source never had.
The whole FIFO map, in one statement: every key is the target's queue with pref in front, and
pref is the inbox of the one instance receiving on that key, or empty. The ib witness is shared
with forward/backward, which is what makes this composable with them rather than a separate
fact.
Every key an instance receives on is a channel that exists. Separate from fifos because it is
consumed on its own: it is what says the target's receiving thread cannot abort.
The introduction form: one hypothesis per clause, against a single choice of witnesses. Needs no
Functional hypothesis on either side — Instances being a function, that holds definitionally.
An instance whose process contains no receive has no inbox to account for — so the mailbox
being none (a syntactic fact about the compiled process) forces the witness to be none too, and
none of the FIFO clauses mention that instance. Needs the instance to be present, which is what
forward supplies.