Exact laws of structured randomized word-RAM programs

Cslib.WordRAM.ExecRandLaw w c x P T R f μ strengthens Cslib.WordRAM.ExecRandWithin w c x P T R by the exact distribution μ of an observation f : Data r → α of the final data. Its rules compose like those of ExecRandWithin. Along a sequence or a loop iteration, the observation of the first part only has to determine the law of the rest, so the laws compose by PMF.bind (Cslib.WordRAM.ExecRandLaw.seq, Cslib.WordRAM.ExecRandLaw.loop_iter). This lets a proof match a program against a mathematical randomized process step by step, observing only the part of the memory that the process describes.

A compiled program then halts on every path within the time bound, makes at most the given number of rand calls, and has law μ for every observation of its halting configurations that agrees with f (Cslib.WordRAM.ExecRandLaw.program).

Main definitions

• Cslib.WordRAM.ExecRandLaw: pathwise postcondition, worst-case instruction and rand-call budgets, and the exact law of an observation of the final data.

Main results

• Cslib.WordRAM.ExecRandLaw.of_execWithin, Cslib.WordRAM.ExecRandLaw.rand: deterministic code and a single rand instruction.
• Cslib.WordRAM.ExecRandLaw.seq_det, Cslib.WordRAM.ExecRandLaw.seq_det_right, Cslib.WordRAM.ExecRandLaw.rand_seq: deterministic prefixes and suffixes, and a draw followed by deterministic code.
• Cslib.WordRAM.ExecRandLaw.seq, Cslib.WordRAM.ExecRandLaw.branch_pos, Cslib.WordRAM.ExecRandLaw.branch_neg, Cslib.WordRAM.ExecRandLaw.loop_exit, Cslib.WordRAM.ExecRandLaw.loop_iter: composition rules.
• Cslib.WordRAM.ExecRandLaw.rename: renaming registers.
• Cslib.WordRAM.ExecRandLaw.execRandWithin: forgetting the law.
• Cslib.WordRAM.ExecRandLaw.map, Cslib.WordRAM.ExecRandLaw.withBounded, Cslib.WordRAM.ExecRandLaw.withSupport: mapping the observation, and the boundedness and the support of every final observation.
• Cslib.WordRAM.ExecRandLaw.program: the compiled program halts within the bound, respects the call budget and the postcondition, and has the law μ.

def Cslib.WordRAM.ExecRandLaw {B : Basis} {r : ℕ} {α : Type} (w : ℕ) (c : Code B r) (x : Data r) (P : Data r → Prop) (T R : ℕ) (f : Data r → α) (μ : PMF α) : Prop

ExecRandLaw w c x P T R f μ: at word size w, running c from x terminates cleanly on every path, makes at most R rand calls on every path, every supported outcome (y, n) satisfies P y and n ≤ T, and the observation f y of the final data has law μ.

theorem Cslib.WordRAM.ExecRandLaw.execRandWithin {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {c : Code B r} {x : Data r} {P : Data r → Prop} {T R : ℕ} {f : Data r → α} {μ : PMF α} (h : ExecRandLaw w c x P T R f μ) : ExecRandWithin w c x P T R

Forgetting the law leaves an ExecRandWithin specification.

theorem Cslib.WordRAM.ExecRandLaw.mono {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {c : Code B r} {x : Data r} {P Q : Data r → Prop} {T T' R R' : ℕ} {f : Data r → α} {μ : PMF α} (h : ExecRandLaw w c x P T R f μ) (hPQ : ∀ (y : Data r), P y → Q y) (hT : T ≤ T') (hR : R ≤ R') : ExecRandLaw w c x Q T' R' f μ

Weakening the postcondition and the budgets.

theorem Cslib.WordRAM.ExecRandLaw.congr_law {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {c : Code B r} {x : Data r} {P : Data r → Prop} {T R : ℕ} {f : Data r → α} {μ μ' : PMF α} (h : ExecRandLaw w c x P T R f μ) (hμ : μ = μ') : ExecRandLaw w c x P T R f μ'

Rewriting the law along an equality.

theorem Cslib.WordRAM.ExecRandLaw.map {B : Basis} {r : ℕ} {α β : Type} {w : ℕ} {c : Code B r} {x : Data r} {P : Data r → Prop} {T R : ℕ} {f : Data r → α} {μ : PMF α} (h : ExecRandLaw w c x P T R f μ) (g : α → β) : ExecRandLaw w c x P T R (fun (y : Data r) => g (f y)) (PMF.map g μ)

Post-composing the observation with g maps the law by g.

theorem Cslib.WordRAM.ExecRandLaw.withBounded {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {c : Code B r} {x : Data r} {P : Data r → Prop} {T R : ℕ} {f : Data r → α} {μ : PMF α} (h : ExecRandLaw w c x P T R f μ) (hx : Data.Bounded w x) : ExecRandLaw w c x (fun (y : Data r) => P y ∧ Data.Bounded w y) T R f μ

Strengthening the postcondition with word-boundedness, from bounded initial data.

theorem Cslib.WordRAM.ExecRandLaw.withSupport {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {c : Code B r} {x : Data r} {P : Data r → Prop} {T R : ℕ} {f : Data r → α} {μ : PMF α} (h : ExecRandLaw w c x P T R f μ) : ExecRandLaw w c x (fun (y : Data r) => P y ∧ f y ∈ μ.support) T R f μ

Strengthening the postcondition: every final observation lies in the support of the law.

theorem Cslib.WordRAM.ExecRandLaw.withPreserves {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {c : Code B r} {x : Data r} {P : Data r → Prop} {T R : ℕ} {f : Data r → α} {μ : PMF α} {i : Fin r} (h : ExecRandLaw w c x P T R f μ) (hi : Code.Preserves i c) : ExecRandLaw w c x (fun (y : Data r) => P y ∧ y.regs i = x.regs i) T R f μ

Strengthening the postcondition with a register that c never writes.

theorem Cslib.WordRAM.ExecRandLaw.rename {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {c : Code B r} {P : Data r → Prop} {T R : ℕ} {f : Data r → α} {μ : PMF α} {r' : ℕ} {ρ : Fin r → Fin r'} (hρ : Function.Injective ρ) {x' : Data r'} (h : ExecRandLaw w c (Data.comap ρ x') P T R f μ) : ExecRandLaw w (Code.rename ρ c) x' (fun (y' : Data r') => ∃ (y : Data r), P y ∧ y' = Data.extend ρ y x') T R (fun (y' : Data r') => f (Data.comap ρ y')) μ

Renaming along an injective register map ρ: the renamed code observes the registers that ρ chooses and keeps the others.

theorem Cslib.WordRAM.ExecRandLaw.of_execWithin {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {c : Code B r} {x : Data r} {P : Data r → Prop} {T : ℕ} {f : Data r → α} {y : Data r} (h : ExecWithin w c x y T) (hy : P y) : ExecRandLaw w c x P T 0 f (PMF.pure (f y))

Deterministic code reaching y has the point law at the observation of y.

theorem Cslib.WordRAM.ExecRandLaw.rand {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {x : Data r} {P : Data r → Prop} {f : Data r → α} {dst src : Fin r} (hfit : Fits w (x.regs src)) (hk : ∀ (k : Fin (x.regs src + 1)), P (x.set dst ↑k)) : ExecRandLaw w (Code.rand dst src) x P 1 1 f (PMF.map (fun (k : Fin (x.regs src + 1)) => f (x.set dst ↑k)) (Probability.PMF.uniformOfFintype (Fin (x.regs src + 1))))

Code.rand dst src draws k uniformly from [0, x.regs src] and observes x.set dst k.

theorem Cslib.WordRAM.ExecRandLaw.seq {B : Basis} {r : ℕ} {α β : Type} {w : ℕ} {c₁ c₂ : Code B r} {x : Data r} {P Q : Data r → Prop} {T₁ T₂ R₁ R₂ : ℕ} {f : Data r → α} {g : Data r → β} {ν : PMF β} {κ : β → PMF α} (h₁ : ExecRandLaw w c₁ x P T₁ R₁ g ν) (h₂ : ∀ (y : Data r), P y → ExecRandLaw w c₂ y Q T₂ R₂ f (κ (g y))) : ExecRandLaw w (c₁.seq c₂) x Q (T₁ + T₂) (R₁ + R₂) f (ν.bind κ)

Sequencing. If the observation g after c₁ determines the law κ (g y) of the observation f after c₂, the laws compose by PMF.bind.

theorem Cslib.WordRAM.ExecRandLaw.seq_det {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {c₁ c₂ : Code B r} {x : Data r} {Q : Data r → Prop} {T₁ T₂ R : ℕ} {f : Data r → α} {μ : PMF α} {y : Data r} (h₁ : ExecWithin w c₁ x y T₁) (h₂ : ExecRandLaw w c₂ y Q T₂ R f μ) : ExecRandLaw w (c₁.seq c₂) x Q (T₁ + T₂) R f μ

A deterministic prefix leading to y does not change the law of what follows.

theorem Cslib.WordRAM.ExecRandLaw.seq_det_right {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {c₁ c₂ : Code B r} {x : Data r} {P Q : Data r → Prop} {T₁ T₂ R : ℕ} {f : Data r → α} {μ : PMF α} (h₁ : ExecRandLaw w c₁ x P T₁ R f μ) (h₂ : ∀ (y : Data r), P y → ∃ (y' : Data r), ExecWithin w c₂ y y' T₂ ∧ Q y' ∧ f y' = f y) : ExecRandLaw w (c₁.seq c₂) x Q (T₁ + T₂) R f μ

A deterministic suffix that keeps the observation does not change the law.

theorem Cslib.WordRAM.ExecRandLaw.rand_seq {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {c₂ : Code B r} {x : Data r} {P : Data r → Prop} {T₂ : ℕ} {f : Data r → α} {dst src : Fin r} {y : Fin (x.regs src + 1) → Data r} (hfit : Fits w (x.regs src)) (h₂ : ∀ (k : Fin (x.regs src + 1)), ExecWithin w c₂ (x.set dst ↑k) (y k) T₂) (hP : ∀ (k : Fin (x.regs src + 1)), P (y k)) : ExecRandLaw w ((Code.rand dst src).seq c₂) x P (1 + T₂) 1 f (PMF.map (fun (k : Fin (x.regs src + 1)) => f (y k)) (Probability.PMF.uniformOfFintype (Fin (x.regs src + 1))))

A rand instruction followed by deterministic code: drawing k uniformly from [0, x.regs src] leads to y k.

theorem Cslib.WordRAM.ExecRandLaw.branch_pos {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {pos neg : Code B r} {cond : Cond r} {x : Data r} {P : Data r → Prop} {T R : ℕ} {f : Data r → α} {μ : PMF α} (hc : cond.Holds x) (h : ExecRandLaw w pos x P T R f μ) : ExecRandLaw w (Code.branch cond pos neg) x P (T + 1) R f μ

Taking the positive branch adds one instruction and keeps the law.

theorem Cslib.WordRAM.ExecRandLaw.branch_neg {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {pos neg : Code B r} {cond : Cond r} {x : Data r} {P : Data r → Prop} {T R : ℕ} {f : Data r → α} {μ : PMF α} (hc : ¬cond.Holds x) (h : ExecRandLaw w neg x P T R f μ) : ExecRandLaw w (Code.branch cond pos neg) x P (T + 2) R f μ

Taking the negative branch adds two instructions and keeps the law.

theorem Cslib.WordRAM.ExecRandLaw.loop_exit {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {body : Code B r} {cond : Cond r} {x : Data r} {P : Data r → Prop} {f : Data r → α} (hc : ¬cond.Holds x) (hx : P x) : ExecRandLaw w (Code.loop cond body) x P 2 0 f (PMF.pure (f x))

Exiting a loop takes two instructions and observes the current data.

theorem Cslib.WordRAM.ExecRandLaw.loop_iter {B : Basis} {r : ℕ} {α β : Type} {w : ℕ} {body : Code B r} {cond : Cond r} {x : Data r} {P Q : Data r → Prop} {T₁ T₂ R₁ R₂ : ℕ} {f : Data r → α} {g : Data r → β} {ν : PMF β} {κ : β → PMF α} (hc : cond.Holds x) (hb : ExecRandLaw w body x P T₁ R₁ g ν) (hl : ∀ (y : Data r), P y → ExecRandLaw w (Code.loop cond body) y Q T₂ R₂ f (κ (g y))) : ExecRandLaw w (Code.loop cond body) x Q (T₁ + T₂ + 2) (R₁ + R₂) f (ν.bind κ)

One loop iteration. The body's observation g determines the law of the rest of the loop, and the laws compose by PMF.bind.

theorem Cslib.WordRAM.ExecRandLaw.program {B : Basis} {r : ℕ} {α : Type} {w : ℕ} {c : Code B r} {x : Data r} {P : Data r → Prop} {T T' R : ℕ} {f : Data r → α} {μ : PMF α} (h : ExecRandLaw w c x P T R f μ) (out : Fin r) (hT : T + 1 ≤ T') (F : RandCfg r → α) (hF : ∀ (y : Data r), P y → F (RandCfg.halted (y.regs out) y) = f y) : RandHaltsWithin w (c.program out) { pc := 0, data := x } T' ∧ RandCallsBounded w (c.program out) { pc := 0, data := x } T' R ∧ (∀ cfg ∈ OracleComp.support (runRand w (c.program out) T' (RandCfg.running { pc := 0, data := x })), ∃ (y : Data r), cfg = RandCfg.halted (y.regs out) y ∧ P y) ∧ PMF.map F (evalRand w (c.program out) T' { pc := 0, data := x }) = μ

Compiled programs. Compiling c with Code.program out halts on every path within any fuel T' ≥ T + 1, makes at most R rand calls, satisfies the postcondition on the halting data, and every observation F of halting configurations that agrees with f has law μ.