What a step leaves alone.
The refinement invariant pins one resolved channel key, ⟨c.name, cpath⟩, and cpath is read
out of the source's memory. So a source step that moved that key would move the key the
invariant names — and at the algorithm level, where each instance's key is what its inbox is
accounted against, a moved key leaves the old key's drained prefix belonging to nobody. The
algorithm-level invariant would then be false, not merely unprovable.
It cannot happen, and Fresh is why: a statement writes at most one name, and Fresh says that
name is not one the mailbox channel is indexed by. This file is that argument, one level at a time
— statement, block, branch — ending at AtomicBranch.reducing_evalArgs, which is the form the
process layer needs.
Stated over Statement.writtenName? rather than over Fresh directly: locality is a fact about
the language, freshness a condition this pass arranges, and keeping them apart means the
induction is done once against the smaller statement.
One statement writes one name. Every other binding is exactly where it was.
Statement.writtenName? is the whole content: the three constructors that answer .some are the
three that touch memory (assign and receive through Memory.update, with through an insert),
and the rest are .none and leave the memory alone outright.
A statement list writes only what its statements write — Block.reducing_locality on the
list form the precondition walk is stated against.
A block writes only what its statements write. The same left-to-right induction
actionBlock_refines runs, with one Statement.reducing_locality per step and the intermediate
lookups chained.
And a branch writes only what its two blocks write. A branch is its precondition composed
with its action; a missing precondition is Relation.Idle, which writes nothing at all.
The key the invariant pins cannot move. A branch whose every statement is Fresh for the
mailbox leaves the mailbox channel's resolved path exactly where it was: a statement writes one
name, and Fresh's third clause says that name is not one the channel is indexed by.
This is what the algorithm level needs and has no other source for. Each instance's inbox is
accounted against its key, so a step that moved the key would leave the old key's drained prefix
belonging to no instance at all — algRelatesTo would be false after the step, not merely
unprovable. Every other hypothesis this pass carries is about keeping a proof going; this one is
about the statement being true.
A guard or a plain assignment leaves the channels untouched — the only Network statements
that reach a fifo are send and multicast, and the compiled precondition together with its
consumption assignments is neither.
A guard or a plain assignment leaves the channels untouched — the only Network statements
that reach a fifo are send and multicast, and the compiled precondition together with its
consumption assignments is neither.
The list form for the compiled guards.
And for the consumption assignments.