The swap preserves the meaning (module FrontSem)

In a model where the swappable operations commute, value and log-weight alike (Swap.Lawful; for add, whose log-weight is 0), a program and any program with some swappable lines swapped (SwapLine) have the same trace values, semantics and log-weight. The theorems about a typed swap therefore hold for the program as written: density, concordance with the swap's inverse program, and bijectivity. swapArgs emits a swap (swapArgs_swap).

inductive RoleFlow.SwapLine {S : Type} {Sg : Sig S} [Swap Sg] : Line Sg → Line Sg → Prop

l' is l, or l = o(a, b) and l' = o(b, a) for a swappable o.

• refl {S : Type} {Sg : Sig S} [Swap Sg] (l : Line Sg) : SwapLine l l
• swap {S : Type} {Sg : Sig S} [Swap Sg] {as bs : List S} (o : Sg.Op as bs) (hs : Swap.swappable o = true) (a b : ℕ) : SwapLine { as := as, bs := bs, op := o, args := [a, b] } { as := as, bs := bs, op := o, args := [b, a] }

theorem RoleFlow.SwapLine.symm {S : Type} {Sg : Sig S} [Swap Sg] {l l' : Line Sg} : SwapLine l l' → SwapLine l' l

theorem RoleFlow.swapLine_swapIf {S : Type} {Sg : Sig S} [Swap Sg] (s : Bool) (l : Line Sg) : SwapLine l (swapIf s l)

theorem RoleFlow.swapLines_swap {S : Type} {Sg : Sig S} [Swap Sg] (sw : ℕ → Bool) (i : ℕ) (ls : List (Line Sg)) : List.Forall₂ SwapLine ls (swapLines sw i ls)

theorem RoleFlow.swapArgs_swap {S : Type} {Sg : Sig S} [Swap Sg] (P : Prog Sg) : List.Forall₂ SwapLine P.lines (swapArgs P).lines

The front end emits a swap.

theorem RoleFlow.ctxAfter_swap {S : Type} {Sg : Sig S} [Swap Sg] {ls ls' : List (Line Sg)} (hs : List.Forall₂ SwapLine ls ls') (Γ : List S) : ctxAfter Γ ls' = ctxAfter Γ ls

theorem RoleFlow.SwapLine.args {S : Type} {Sg : Sig S} [Swap Sg] {Γ : List S} {l l' : Line Sg} (hl : SwapLine l l') (h : Args Γ l.args l.as) : Args Γ l'.args l'.as

theorem RoleFlow.linesWF_swap {S : Type} {Sg : Sig S} [Swap Sg] {Γ : List S} {ls ls' : List (Line Sg)} (hs : List.Forall₂ SwapLine ls ls') (h : LinesWF Γ ls) : LinesWF Γ ls'

def RoleFlow.Swap.Lawful {S : Type} {Sg : Sig S} [Swap Sg] [Sorts S] (M : Model Sg) : Prop

A model is lawful for the swaps if every swappable operation commutes, in its value and its log-weight.

Equations

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

theorem RoleFlow.stepLine_swap {S : Type} {Sg : Sig S} [Swap Sg] [Sorts S] {M : Model Sg} (hM : Swap.Lawful M) {Γ as bs : List S} (o : Sg.Op as bs) (hs : Swap.swappable o = true) (a b : ℕ) (h : Args Γ [a, b] as) (h' : Args Γ [b, a] as) (v : Val Γ) : stepLine M { as := as, bs := bs, op := o, args := [b, a] } h' v = stepLine M { as := as, bs := bs, op := o, args := [a, b] } h v

o(b, a) steps to the same value as o(a, b).

theorem RoleFlow.trace_swap {S : Type} {Sg : Sig S} [Swap Sg] [Sorts S] {M : Model Sg} (hM : Swap.Lawful M) {Γ : List S} {ls ls' : List (Line Sg)} (hs : List.Forall₂ SwapLine ls ls') (h : LinesWF Γ ls) (h' : LinesWF Γ ls') (v : Val Γ) {i : ℕ} {s : S} (hi : (ctxAfter Γ ls)[i]? = some s) (hi' : (ctxAfter Γ ls')[i]? = some s) : (trace M ls' h' v).get i hi' = (trace M ls h v).get i hi

theorem RoleFlow.logwLines_swap {S : Type} {Sg : Sig S} [Swap Sg] [Sorts S] {M : Model Sg} (hM : Swap.Lawful M) {Γ : List S} {ls ls' : List (Line Sg)} (hs : List.Forall₂ SwapLine ls ls') (h : LinesWF Γ ls) (h' : LinesWF Γ ls') (ρ : List Role) (v : Val Γ) : logwLines M ls' h' ρ v = logwLines M ls h ρ v

Programs

@[reducible, inline]

abbrev RoleFlow.Prog.swap {S : Type} {Sg : Sig S} (P : Prog Sg) (ls : List (Line Sg)) : Prog Sg

A swap of P.

Equations

• P.swap ls = { wts := P.wts, ins := P.ins, outs := P.outs, lines := ls, ret := P.ret }

theorem RoleFlow.Prog.wf_swap {S : Type} {Sg : Sig S} [Swap Sg] {P : Prog Sg} {ls : List (Line Sg)} (hs : List.Forall₂ SwapLine P.lines ls) (h : P.WF) : (P.swap ls).WF

theorem RoleFlow.Prog.wf_of_swap {S : Type} {Sg : Sig S} [Swap Sg] {P : Prog Sg} {ls : List (Line Sg)} (hs : List.Forall₂ SwapLine P.lines ls) (h : (P.swap ls).WF) : P.WF

The written program is well formed if a swap is.

theorem RoleFlow.Prog.sem_swap {S : Type} {Sg : Sig S} [Swap Sg] {P : Prog Sg} {ls : List (Line Sg)} [Sorts S] {M : Model Sg} (hM : Swap.Lawful M) (hs : List.Forall₂ SwapLine P.lines ls) (h : P.WF) (h' : (P.swap ls).WF) (θ : Val P.wts) (x : Val P.ins) : sem M (P.swap ls) h' θ x = sem M P h θ x

theorem RoleFlow.Prog.logw_swap {S : Type} {Sg : Sig S} [Swap Sg] {P : Prog Sg} {ls : List (Line Sg)} {ρ : List Role} [Sorts S] {M : Model Sg} (hM : Swap.Lawful M) (hs : List.Forall₂ SwapLine P.lines ls) (h : P.WF) (h' : (P.swap ls).WF) (θ : Val P.wts) (x : Val P.ins) : logw M (P.swap ls) h' ρ θ x = logw M P h ρ θ x

theorem RoleFlow.Prog.density_swap {S : Type} {Sg : Sig S} [Swap Sg] {P : Prog Sg} {ls : List (Line Sg)} {ρ : List Role} [Sorts S] {M : Model Sg} (hM : Swap.Lawful M) (hs : List.Forall₂ SwapLine P.lines ls) (hT : (P.swap ls).Typed ρ) (θ : Val P.wts) : Cov (vol P.ins) (vol P.outs) (sem M P ⋯ θ) fun (x : Val P.ins) => expw (logw M P ⋯ ρ θ x)

Density of the written program, from a typed swap.

theorem RoleFlow.Prog.inverse_sem_swap {S : Type} {Sg : Sig S} [Swap Sg] {P : Prog Sg} {ls : List (Line Sg)} {ρ : List Role} [Sorts S] {M : Model Sg} (hM : Swap.Lawful M) (hs : List.Forall₂ SwapLine P.lines ls) (hT : (P.swap ls).Typed ρ) (θ : Val P.wts) (x : Val P.ins) : sem M ((P.swap ls).inverse ρ) ⋯ θ (sem M P ⋯ θ x) = x

Concordance: the swap's inverse program undoes the written program.

theorem RoleFlow.Prog.bijective_swap {S : Type} {Sg : Sig S} [Swap Sg] {P : Prog Sg} {ls : List (Line Sg)} {ρ : List Role} [Sorts S] {M : Model Sg} (hM : Swap.Lawful M) (hs : List.Forall₂ SwapLine P.lines ls) (hT : (P.swap ls).Typed ρ) (hR : M.RightLaw) (θ : Val P.wts) : Function.Bijective (sem M P ⋯ θ)

Bijectivity of the written program, from a typed swap, under the right law.