The pass, as Compiler.Correctness states a pass: the compiled algorithm's initial states are covered by related source ones, and its behaviour refines the source's. Everything below this file proves it; this file is only the packaging.

Two program types, and both are forced.

SourceProgram bundles an algorithm with the front-end facts about it. Compiler.Correctness quantifies over every program of its source type, so a hypothesis hoisted outside — ∀ algo, AlgorithmFresh mbox c₀ algo — would ask one mailbox assignment to be fresh for every algorithm at once, which no assignment is. The statement would hold vacuously and say nothing. Bundling puts each algorithm next to its own mbox/c₀, which is how every rung below already reads them.

TargetProgram is a phantom index: the pass's output is an algorithm and nothing more, but the framework's Reduce/Abort/Diverge classes take the semantics as an outParam, so the program type has to determine the value universe its semantics is taken in. ComputableNetworkPlusCal. Algorithm does not mention V; TargetProgram V Ξ Ω does.

The two program types

structure Guarded2Network.FrontEnd {V : Type u} [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) (mbox : String → String → Mailbox) (c₀ : String → ComputableGuardedPlusCal.Ref) (algo : ComputableGuardedPlusCal.Algorithm) : Prop

Everything the front end owes this pass, at one algorithm. Three syntactic conditions and one semantic: AlgorithmFresh (the generated inbox collides with nothing the source uses), MailboxUsed (a declared mailbox is one its process receives on, checkReceiveChannels), Nodup on the process names (duplicateProcessName) — and InitKeys, the key a receiving instance starts on, which is the one thing here no checker establishes.

keys quantifies over the FIFO map because InitKeys.declared is stated against it: which map an initial state carries is not fixed until that state is chosen. The other two clauses do not mention it, so nothing is lost by letting the witness depend on it.

• fresh : AlgorithmFresh mbox c₀ algo

  The generated inbox is fresh for every branch of every process.

• used : MailboxUsed mbox algo

  A process with a mailbox is a process that receives.

• names : (List.map (fun (x : GuardedPlusCal.Process ComputableTLAPlus.Typ ComputablePlusCal.Expression) => x.name) algo.processes).Nodup

  No two processes share a name.

• keys (F : GuardedPlusCal.FIFOs V) : ∃ (key : String × V → GuardedPlusCal.ChanKey V), InitKeys Ξ Ω c₀ algo F key

  Each receiving instance starts on a key that resolves, exists, and is its own.

• wellScopedEnv : Ξ.WellScoped

  Every operator body in Ξ is closed over its parameters — ExprSemantics.evalLocal's side condition. Holds for any Ξ the checker populates.

structure Guarded2Network.SourceProgram (V : Type u) [ComputableTLAPlus.ExprSemantics V] (Ξ : ComputableTLAPlus.OperatorEnv) (Ω : ComputableTLAPlus.Model V) : Type u

A source program of this pass: an algorithm, the mailbox and channel assignment its processes are read at, and the front end's facts about all three. See this file's module doc for why the facts are bundled into the type rather than hoisted into a hypothesis.

• algo : ComputableGuardedPlusCal.Algorithm

  The algorithm itself.

• mbox : String → String → Mailbox

  Which mailbox each process name gets, as a function of the name the pass will generate.

• c₀ : String → ComputableGuardedPlusCal.Ref

  Which channel each process name receives on.

• wellFormed : FrontEnd Ξ Ω self.mbox self.c₀ self.algo

  And the front end's guarantees about them.

def Guarded2Network.TargetProgram (_V : Type u) (_Ξ : ComputableTLAPlus.OperatorEnv) (_Ω : ComputableTLAPlus.Model _V) : Type

A target program of this pass — a compiled algorithm, indexed by the value universe its semantics is taken in. The index is phantom; see this file's module doc for why it is there.

Equations

• Guarded2Network.TargetProgram _V _Ξ _Ω = ComputableNetworkPlusCal.Algorithm

Their semantics, as the framework indexes it

@[implicit_reducible]

instance Guarded2Network.instReduceSourceProgramSetProdAlgStateStringTrace {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} : Reduce (SourceProgram V Ξ Ω) (Set (GuardedPlusCal.AlgState (String × V) V × GuardedPlusCal.Trace V × GuardedPlusCal.AlgState (String × V) V))

The reduce slot of the refinement is the terminating semantics ⟦A⟧⁺ — Algebra.reducing (every partial run) cut to runs that end in a done configuration. See Algebra.terminating.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Guarded2Network.instAbortSourceProgramSetProdAlgStateStringTrace {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} : Abort (SourceProgram V Ξ Ω) (Set (GuardedPlusCal.AlgState (String × V) V × GuardedPlusCal.Trace V))

Equations

• Guarded2Network.instAbortSourceProgramSetProdAlgStateStringTrace = { abort := fun (s : Guarded2Network.SourceProgram V Ξ Ω) => (GuardedPlusCal.Algorithm.algebra Ξ Ω s.algo).aborting }

@[implicit_reducible]

instance Guarded2Network.instDivergeSourceProgramSetProdAlgStateStringTrace {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} : Diverge (SourceProgram V Ξ Ω) (Set (GuardedPlusCal.AlgState (String × V) V × GuardedPlusCal.Trace V))

Equations

• Guarded2Network.instDivergeSourceProgramSetProdAlgStateStringTrace = { div := fun (s : Guarded2Network.SourceProgram V Ξ Ω) => (GuardedPlusCal.Algorithm.algebra Ξ Ω s.algo).diverging }

@[implicit_reducible]

instance Guarded2Network.instBlockSourceProgramSetProdAlgStateStringTrace {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} : Block (SourceProgram V Ξ Ω) (Set (GuardedPlusCal.AlgState (String × V) V × GuardedPlusCal.Trace V))

Equations

• Guarded2Network.instBlockSourceProgramSetProdAlgStateStringTrace = { block := fun (s : Guarded2Network.SourceProgram V Ξ Ω) => (GuardedPlusCal.Algorithm.algebra Ξ Ω s.algo).blocking }

@[implicit_reducible]

instance Guarded2Network.instReduceTargetProgramSetProdAlgStateStringTrace {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} : Reduce (TargetProgram V Ξ Ω) (Set (GuardedPlusCal.AlgState (String × V) V × GuardedPlusCal.Trace V × GuardedPlusCal.AlgState (String × V) V))

The reduce slot is the terminating semantics ⟦A⟧⁺, as for the source.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Guarded2Network.instAbortTargetProgramSetProdAlgStateStringTrace {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} : Abort (TargetProgram V Ξ Ω) (Set (GuardedPlusCal.AlgState (String × V) V × GuardedPlusCal.Trace V))

Equations

• Guarded2Network.instAbortTargetProgramSetProdAlgStateStringTrace = { abort := fun (algo' : Guarded2Network.TargetProgram V Ξ Ω) => (NetworkPlusCal.Algorithm.algebra Ξ Ω algo').aborting }

@[implicit_reducible]

instance Guarded2Network.instDivergeTargetProgramSetProdAlgStateStringTrace {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} : Diverge (TargetProgram V Ξ Ω) (Set (GuardedPlusCal.AlgState (String × V) V × GuardedPlusCal.Trace V))

Equations

• Guarded2Network.instDivergeTargetProgramSetProdAlgStateStringTrace = { div := fun (algo' : Guarded2Network.TargetProgram V Ξ Ω) => (NetworkPlusCal.Algorithm.algebra Ξ Ω algo').diverging }

@[implicit_reducible]

instance Guarded2Network.instBlockTargetProgramSetProdAlgStateStringTrace {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} : Block (TargetProgram V Ξ Ω) (Set (GuardedPlusCal.AlgState (String × V) V × GuardedPlusCal.Trace V))

Equations

• Guarded2Network.instBlockTargetProgramSetProdAlgStateStringTrace = { block := fun (algo' : Guarded2Network.TargetProgram V Ξ Ω) => (NetworkPlusCal.Algorithm.algebra Ξ Ω algo').blocking }

def Guarded2Network.compile {V : Type u} [ComputableTLAPlus.ExprSemantics V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} (s : SourceProgram V Ξ Ω) : G2NM (TargetProgram V Ξ Ω)

The pass itself, at those two types. Algorithm.toNetwork never looks at anything a SourceProgram carries beyond the algorithm — the rest is what the proof reads.

Equations

• Guarded2Network.compile s = s.algo.toNetwork

The theorem

theorem Guarded2Network.correct {V : Type u} [ComputableTLAPlus.ExprSemantics V] [SeqBuiltins V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} [DecidableEq V] : Compiler.Correctness (fun (x : SourceProgram V Ξ Ω) (algo' : TargetProgram V Ξ Ω) => algRelatesTo Ξ Ω (procMailbox algo')) compile (fun (s : SourceProgram V Ξ Ω) => GuardedPlusCal.Algorithm.init Ξ Ω s.algo) (NetworkPlusCal.Algorithm.init Ξ Ω)

Guarded2Network is a correct pass. The whole development meets here.

The relation is algRelatesTo at the mailbox read off the compiled algorithm — which is why Compiler.Correctness indexes its relation by the target program, and why both halves live inside one triple. The init half is Algorithm.init_refines, the refinement half is Algorithm.toNetwork_refines, and triple_forall is what lets one run of the pass answer both at every prefix function at once.

theorem Guarded2Network.correct' {V : Type u} [ComputableTLAPlus.ExprSemantics V] [SeqBuiltins V] {Ξ : ComputableTLAPlus.OperatorEnv} {Ω : ComputableTLAPlus.Model V} [DecidableEq V] : Compiler.Correct compile (fun (s : SourceProgram V Ξ Ω) => GuardedPlusCal.Algorithm.init Ξ Ω s.algo) (NetworkPlusCal.Algorithm.init Ξ Ω)

And so it is correct in the composable form, which is what a whole-pipeline statement chains (Compiler.Correct.comp).