From one compiled block to one process step.
Lemmas/AtomicBlock.lean leaves a compiled block as List.Forall₂ BranchRefines over its
branches. The process layer schedules a label, and the block that label names denotes the union
of its branches (GuardedPlusCal.Process.codeTable), so what the process layer needs is that
union simulated — some target branch's step answered by some source branch's step. That is
blockRefines_step below, and it is nothing more than BranchRefines.refines.terminating applied
at the branch List.Forall₂.exists_left picks out.
The other half of the same bridge runs the other way: relatesTo_of_procRelatesTo turns the
algorithm-level invariant, once a process has been picked, into the local relatesTo the block
layer is stated against, and procRelatesTo_of_relatesTo turns the block's result back. Both
halves need pref to be a parameter of relatesTo — that is what it is for
(Lemmas/Relation.lean).
The indexed/flat boundary is crossed here too. CodeTable.reducing is stated at the indexed
LocalState, every refinement lemma at the flat LocalState, and
GuardedPlusCal.LocalState.sem_glue₃/.abort_glue₂ are what say those are the same fact.
AtomicBranch.reducing_evalArgs against the freshness bundle the block level already
carries. BranchesFresh quantifies its precondition clause over preconditionList, the locality
argument over the Block.toList of a precondition that is present; the two are the same list, and
saying so is the whole of this lemma.
Picking a process projects the invariant. One instance's procRelatesTo, together with the
one FIFO equation algRelatesTo carries, is relatesTo on that instance's local state.
This is what the whole pref parameter exists for. relatesTo reads pref at every key but this
instance's own channel, where it uses the instance's own inbox instead — and that is exactly the
clause ib already pins (hkey). So the projection is a repackaging, with no side condition and
nothing to choose.
Stated against algRelatesTo's witnesses rather than against algRelatesTo itself, which a caller
has already destructured to get at the instance.
And putting the process back. The block layer hands back relatesTo at the post-state; this
turns it into the procRelatesTo and the two FIFO clauses the algorithm-level witness is rebuilt
from, with the new InboxState read off relatesTo's own existential.
hstable is where Lemmas/Locality.lean is spent, and it is a soundness hypothesis rather than a
convenience. relatesTo's post-state names some key its own cpath resolves to; without knowing
that the old key still resolves, nothing forces the two to agree, and an instance whose key moved
would leave its old key's drained prefix accounted to nobody — algRelatesTo would then be false,
not merely unprovable. With it, Ref.EvalArgs.inj pins the new key to the old, which is what makes
hsame — and through it every key-phrased clause of algRelatesTo — survive the step.
The label set is handed in rather than derived: which labels the source schedules next is the process layer's business, and this only threads it through.
A compiled block's step is answered by the source block's. A block denotes the union of its
branches, so a target step is a step of some compiled branch; List.Forall₂.exists_left names the
source branch it was compiled from, and that branch's own refinement answers it.
The conclusion is Terminating's two disjuncts with the branch existentially quantified inside
each — which is the shape the process layer wants, since a source process step is likewise "some
branch of the block at the scheduled label".
blockRefines_step at the indexed encoding the process layer states its steps in.
GuardedPlusCal.LocalState.sem_glue₃/.abort_glue₂ and their NetworkPlusCal twins are the whole
of the difference; nothing about the refinement changes.
The target's post-state is ⟨M₂', F₂', .some l'⟩, so the flat one carries some l' — and
relatesTo.label_eq then hands the source the same l', which is what makes the two processes
schedule the same label next. That agreement is the reason BranchRefines carries last_eq at
all.
And where a compiled block goes wrong, the source block does too. blockRefines_step's
twin, and simpler for the same reason Aborting is simpler than Terminating: an abort has no
post-state, so there is nothing to relate afterwards and no witness to rebuild.
blockRefines_abort at the indexed encoding, exactly as blockRefines_step_indexed is for
blockRefines_step.
The block half of the algorithm-level per-step obligation. One instance takes a step of a
compiled code thread's block; the source instance answers with a step of the block it was compiled
from, and the whole algRelatesTo witness is rebuilt around it.
The two disjuncts are Terminating's, with the branch existentially quantified inside each and the
new state sets spelled out — the same shape rx_step states its (much shorter) conclusion in, and
what the process layer needs to assemble Algebra.step.
Everything is one instance's business, which is what makes the proof go: p's own step is
blockRefines_step_indexed, and every other instance's clause survives because its ib entry and
its key are untouched. The clauses phrased over keys — keys_inj, and pref being empty where
nobody receives — need that this instance's key did not move either, which is hstable's job inside
procRelatesTo_of_relatesTo and ultimately Lemmas/Locality.lean's.
The label a code block leaves at needs no condition — a .rx thread owns none, so L_s = L_t is
preserved whatever it is; the scheduled label label need not even be shown to be in L₁, the
caller building the source Algebra.step doing that.
The pass at this level: one process, compiled #
The other half of the process layer, above Thread.toNetwork. Everything above is about a
process step; everything below is about
Process.toNetwork — what a compiled process owes its source syntactically, so that
algRelatesTo.step_or_stutter/.immediateAbort can dispatch a target label off it into a code
thread's or a receiving thread's.
This is the rung where freshName first matters. Thread.toNetwork is handed its inbox;
Process.toNetwork invents it, one per process and shared by every thread. So a freshness
hypothesis can no longer be stated at the name — there is no name until the pass has run — and is
instead quantified over every name the pass could have produced (ProcessFresh). Generated is
what makes that dischargeable: the front end knows no source identifier contains $, so it proves
the implication for every counter value at once.
The source-side freshness obligation at this level. Every branch of the process is fresh for
any name the pass could generate as its inbox.
Quantified over the generated name rather than stated at one, because Process.toNetwork invents it
— see the section note above. c₀, the process's single channel, stays a parameter: it is a fact
about the source program, which BranchesFresh.rfresh pins and well-formedness discharges.
mbox is a function of the generated name for the same reason. Which mailbox a process gets is
settled before the pass runs — .none if it never receives, .some (c₀, ·) if it does — but the
name filling the · is not, so the caller supplies the shape and the pass supplies the name.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A generated inbox is never self, which is load-bearing rather than hygiene:
CodeTable.procReducing requires the memory to bind selfName, and the source memory agrees with
the target's only away from the generated name — algRelatesTo.step_or_stutter/.immediateAbort
spend this to rewrite that lookup through unchanged (procMailbox_inbox_ne_selfName).
Pure arithmetic on the shape of the name, needing nothing from the source program: selfName is
"self", four characters, and any generated name is its six-character prefix plus a counter.
A process that never receives is ProcessFresh at .none for nothing, whatever name the pass
generates — BranchesFresh.none_of_no_receive at every branch, which is what says the .none
mailbox costs the front end nothing to supply.
A process one of whose threads receives — the source-side condition the pass's registration
promise is conditioned on, and the one the algorithm level reads off well-formedness: after
checkReceiveChannels, a process has a mailbox exactly when this holds of it.
Equations
Instances For
What one compiled process owes its source.
threads is the refinement: a compiled process's threads are the receiving loops the pass
registered, followed by the compiled code threads, and those refine the source's pairwise. The
RxOnly conjunct names which channel and inbox each receiving loop drains.
name_eq is load-bearing rather than bookkeeping. Algorithm.algebra resolves its table by looking
the process up under its name, so a compiled process found under a different name would answer
with the empty table for every label. self needs nothing from here — it is Prod.snd on both
sides.
id_eq/idShape_eq are owed to Algorithm.init rather than to the per-step refinement argument:
they are what say the compiled algorithm has the same instances. The rest of what init wants — the
entry labels a receiving thread adds, and the inbox local the pass declares — is not here, and is
the initial-state obligation's own business.
- threads : ∃ (rxs : List (NetworkPlusCal.Thread ComputableTLAPlus.Typ ComputablePlusCal.Expression)) (codes : List (NetworkPlusCal.Thread ComputableTLAPlus.Typ ComputablePlusCal.Expression)) (news : List (String × ComputableTLAPlus.Typ × Bool × Option (Bool × ComputablePlusCal.Expression))), p'.threads = rxs ++ codes ∧ (p'.localState = let __src := p.localState; { «variables» := p.localState.variables ++ news, channels := __src.channels, fifos := __src.fifos }) ∧ RxOnly mbox c₀ inbox rxs ∧ List.Forall₂ (ThreadRefines Ξ Ω mbox pref) p.threads codes ∧ (ProcessReceives p → rxs ≠ []) ∧ (∀ e ∈ news, InboxLocal inbox e) ∧ (news = [] ↔ rxs = [])
The registered receive loops, then the compiled code threads — and a source process that receives at all has at least one of the former. That conjunct is what connects the two directions:
RxOnlysays a registered thread means the process has a mailbox, and this says a process with something to receive has a thread registered to drain it.The locals ride in the same existential rather than in a field of their own, because what makes them usable is
news = [] ↔ rxs = []— therxsbound here.Algorithm.initspends both directions: at.none,RxOnlyforcesrxs = []and so no extra local, leaving the two memories equal; at.some,MailboxUsedforcesrxs ≠ []and so aninboxdeclared, which is what binds it in the compiled instance's initial memory. - inbox_generated : Generated "inbox" inbox
The mailbox this is all stated against is a name the pass generated.
And the compiled process answers to the same name,
id, and instance shape.
Instances For
The mailbox a compiled process's receiving threads drain — procMailbox's answer at a
resolved instance, read off the compiled process.
Why not p'.mailbox. The process does carry a declared mailbox, and Process.toNetwork copies
it across; it is just not a Mailbox. Two of the three things this type holds are missing from it.
The inbox is not there at all — the pass generates it (freshName "inbox") and writes it into the
threads it builds and the local it declares, never back into the field. And the channel is
Option (String × List Expr) where a Mailbox holds a ComputableGuardedPlusCal.Ref — no
baseType, and args without the String ⊕ · summand that relatesTo evaluates with EvalStep.
So this is not a search past information already in hand: the receiving thread is the only place the
generated inbox exists. What the declared field is good for is the decision — whether a process
has a mailbox at all — and that is exactly what enters below as a hypothesis, discharged by the front
end rather than guessed from the compiled output.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The owned labels are the source's. A .rx thread owns no label; a code thread owns its
source thread's blocks' labels unchanged.
The entry labels are the source's. A .rx thread owns no label, so it contributes nothing;
a code thread starts at its source thread's first block.
A compiled process contributes the same instances. Process.identities reads nothing but
«=|∈» and id, and Process.toNetwork copies both across.
Owed to Algorithm.init, which quantifies over the instances each declared process contributes: the
two algorithms have to declare the same ones, or the states being related would not even be indexed
alike.
And the initializers split the same way the locals do — the source's, then the pass's own for
the inbox.
Process.inits is initsOf over the declared locals and ProcessRefines reports the target's locals
as the source's with the pass's appended, so the split itself is initsOf_append. The other two
halves are about what was appended: an InboxLocal carries an initializer, so it survives initsOf
rather than being filtered out, and RxOnly ties "a thread was registered" to the mailbox in both
directions — a registered thread forces .some, and hused (the front end's MailboxUsed at this
process) forces a registration from .some.
Owed to Algorithm.init: a compiled instance's initial memory is the source's with inbox written
on top, and this is what says which extra initializers wrote it, and when there are none.
The branches at a label #
ProcessRefines.branchesRefine wants two branch lists — the source's at a label and the
target's — and Process.codeTable lets a label denote the union of every block carrying it.
Nothing in the front end rejects two blocks with one label (WellFormedness/Labelling.lean checks
only that every
goto target exists), so these are concatenations over all such blocks rather than one block's
branches. That is the whole reason BranchesRefine is weaker than List.Forall₂.
Every block the source process labels l, across all of its threads.
Equations
- Guarded2Network.srcBlocksAt p l = List.filter (fun (x : ComputableGuardedPlusCal.AtomicBlock) => x.label == l) p.threads.flatten
Instances For
And every branch of those blocks — the source side ProcessRefines.branchesRefine and
tgt_reducing_le's siblings are stated against.
Equations
- Guarded2Network.srcBranchesAt p l = List.flatMap (fun (x : ComputableGuardedPlusCal.AtomicBlock) => x.branches) (Guarded2Network.srcBlocksAt p l)
Instances For
The blocks of a compiled process's code threads. Its receiving threads contribute none: an
.rx thread's body is the relay, which Thread.rxStep gives directly rather than as a block.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every branch of the compiled blocks labelled l — the target side ProcessRefines.branchesRefine
and tgt_reducing_le's siblings are stated against.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Membership in srcBranchesAt, in the thread/block/branch form every consumer wants.
And in tgtBranchesAt. The .code is not incidental: it is what says the block came from a
compiled code thread rather than from a relay.
A compiled step at a code label is a step of one of that label's compiled branches. The
.rx threads add nothing to Process.codeTable's reducing — their step is in relay — so this
is a straight unfolding.
The same where it goes wrong.
And a source branch at a label is schedulable at it. The converse direction of the same unfolding, and it needs no side condition: the source language has no second summand to rule out.
The same where it goes wrong.
The refinement, at a label rather than at a block — what algRelatesTo.step_or_stutter
resolves at every prefix function to build a BranchesRefine fact for the code case.
Three exists_lefts stacked: a compiled branch sits in a compiled block, which sits in a compiled
code thread, which is some source thread's; the block correspondence carries blk'.label = blk.label,
so the source block is at the same label and its branches are the ones to match against. The
labels agreeing is what makes this a statement about a label at all — otherwise the two
concatenations would be over unrelated blocks.
The source→target direction of branchesRefine — every source branch at a label has a
compiled one, refined. What procBlockTransfer needs: the source blocking semantics is universal
over a block's branches, so it has to reach each one's compilation.
Equations
- Guarded2Network.SrcBranchesRefine Ξ Ω mbox pref brs brs' = ∀ Br ∈ brs, ∃ Br' ∈ brs', Guarded2Network.BranchRefines Ξ Ω mbox pref Br Br'
Instances For
A compiled block blocks at a label ⟹ every one of that label's compiled branches blocks.
The ∀-elimination of NetworkPlusCal.Process.codeTable's blocking clause, in the
thread/block/branch form.
And its converse. Every source branch at a label blocking ⟹ the source block blocks there —
the ∀-introduction of GuardedPlusCal.Process.codeTable's blocking clause.
The receiving side of the dispatch #
A receiving thread's step is Process.codeTable's relay, not a labelled entry. All this side
needs is that the thread is one the pass registered, on the channel and inbox the invariant is
stated against.
A .some rxMailbox names a real receiving thread. rxMailbox is a findSome? over the
threads, so a .some answer is one of them matching. What procBlockTransfer uses to reach the
drained-channel fact relayBlocking states per .rx thread.
Any receiving thread of a compiled process is one the pass registered, and so is on the
process's own channel and inbox — which in turn means the process has a mailbox naming both.
The primitive the receiving side is built from. algRelatesTo.step_or_stutter/.immediateAbort
read the mailbox and its freshness off its first two components.
A process with a mailbox has the one the ladder is stated against. ProcessRefines carries
c₀ and inbox as indices without ever saying they are the mailbox's two components — nothing below
needs that, Fresh .none being vacuous and mbox a parameter throughout. A process that actually
receives does say it: the thread it registered is an .rx on exactly those two (IsRxThread), and
threads' registration clause is what says there is one to look at.
Wanted wherever a .some mailbox has to be taken apart — procMailbox_inbox_ne_selfName needs the
inbox to be the generated one, which is a field of this structure and not of an arbitrary
Mailbox.
The mailbox the refinement was proved at is the one the compiled process wears. What lets
procMailbox be computed from the compiled algorithm rather than witnessed alongside it.
Both directions of the pass's mailbox contract meet here, and neither is free. RxOnly gives one:
it forces mbox = .some on every registered thread, so a process related at .none has none
registered, every one of its threads is a .code, and the search finds nothing. The other is
threads' registration clause — a process that receives has a thread registered to drain its
channel — and carrying that up from stepBranch, the only writer of rxThreads, is what the ghost
in Registered is for.
hused is the front end's, and is where the declared mailbox does its work. Nothing in the pass
rules out being handed a .some mailbox for a process that never receives; checkReceiveChannels
does, by rejecting a receive with no declaration and dropping a declaration no receive uses.
dedupLocalsByName #
Process.toNetwork runs the per-thread locals through it before declaring them: every receiving
thread of a process independently proposes that process's one inbox, and the declaration must
appear once. Two facts about it are wanted, and both are about the underlying foldl with an
arbitrary accumulator rather than about the [] it starts at.
One process, compiled. The inbox generated, the walk over the threads, and the compiled
process read off the accumulator.
The inbox is existential in the conclusion for the reason Generated exists: a postcondition
cannot name the counter the program started at, and nothing above needs the number — only that there
is a single name, shared by every thread of this process, that no source identifier can equal.