Documentation

LeanPool.MRiscX.Examples.OtpProof

OtpProof #

This module provides the end-to-end One-Time-Pad correctness proof.

source
def iPre (p k c l : UInt64) :
Prop

The precondition of the One-Time-Pad correctness proof, constraining the plaintext p, key k, ciphertext c, and length l addresses.

Equations
Instances For
    source
    theorem proof_otp_loopBody (p k c l : UInt64) (s : MState) :
    s.code = { instructionMap := (13 ↦ Instr.Jump ".loop"; (12 ↦ Instr.Decrement (UInt64.ofNat 3); (11 ↦ Instr.Increment (UInt64.ofNat 2); (10 ↦ Instr.Increment (UInt64.ofNat 1); (9 ↦ Instr.Increment (UInt64.ofNat 0); (8 ↦ Instr.StoreWord (UInt64.ofNat 7) (UInt64.ofNat 2); (7 ↦ Instr.XOR (UInt64.ofNat 7) (UInt64.ofNat 5) (UInt64.ofNat 6); (6 ↦ Instr.LoadWordReg (UInt64.ofNat 6) (UInt64.ofNat 1); (5 ↦ Instr.LoadWordReg (UInt64.ofNat 5) (UInt64.ofNat 0); (4 ↦ Instr.JumpEqZero (UInt64.ofNat 3) "finish"; (3 ↦ Instr.LoadImmediate (UInt64.ofNat 3) l; (2 ↦ Instr.LoadAddress (UInt64.ofNat 2) c; (1 ↦ Instr.LoadAddress (UInt64.ofNat 1) k; (0 ↦ Instr.LoadAddress (UInt64.ofNat 0) p; TMap.empty Instr.Panic)))))))))))))), labels := p("finish" ↦ 14; p(".loop" ↦ 4; p("main" ↦ 0; PMap.empty))) } → s.pc = 4 → (s.getRegisterAt 0 = p ∧ s.getRegisterAt 1 = k ∧ s.getRegisterAt 2 = c ∧ s.getRegisterAt 3 = l ∧ iPre p k c l) ∧ ¬s.terminated = true → ∀ (x : UInt64), hoareTripleUp (fun (st : MState) => st.getRegisterAt 3 > 0 ∧ (((∀ i < l - st.getRegisterAt 3, st.getMemoryAt (c + i) = st.getMemoryAt (p + i) ^^^ st.getMemoryAt (k + i)) ∧ st.getRegisterAt 0 = p + (l - st.getRegisterAt 3) ∧ st.getRegisterAt 1 = k + (l - st.getRegisterAt 3) ∧ st.getRegisterAt 2 = c + (l - st.getRegisterAt 3) ∧ st.getRegisterAt 3 ≤ l ∧ iPre p k c l) ∧ ¬st.terminated = true) ∧ st.getRegisterAt 3 = x) (fun (st : MState) => st.getRegisterAt 3 < x ∧ (((∀ i < l - st.getRegisterAt 3, st.getMemoryAt (c + i) = st.getMemoryAt (p + i) ^^^ st.getMemoryAt (k + i)) ∧ st.getRegisterAt 0 = p + (l - st.getRegisterAt 3) ∧ st.getRegisterAt 1 = k + (l - st.getRegisterAt 3) ∧ st.getRegisterAt 2 = c + (l - st.getRegisterAt 3) ∧ st.getRegisterAt 3 ≤ l ∧ iPre p k c l) ∧ ¬st.terminated = true) ∧ st.pc = 4) 4 ({4} ∪ {14}) ({n : UInt64 | n ≠ 14} \ ({n : UInt64 | n ≥ 4} ∩ {n : UInt64 | n < 14})) { instructionMap := (13 ↦ Instr.Jump ".loop"; (12 ↦ Instr.Decrement (UInt64.ofNat 3); (11 ↦ Instr.Increment (UInt64.ofNat 2); (10 ↦ Instr.Increment (UInt64.ofNat 1); (9 ↦ Instr.Increment (UInt64.ofNat 0); (8 ↦ Instr.StoreWord (UInt64.ofNat 7) (UInt64.ofNat 2); (7 ↦ Instr.XOR (UInt64.ofNat 7) (UInt64.ofNat 5) (UInt64.ofNat 6); (6 ↦ Instr.LoadWordReg (UInt64.ofNat 6) (UInt64.ofNat 1); (5 ↦ Instr.LoadWordReg (UInt64.ofNat 5) (UInt64.ofNat 0); (4 ↦ Instr.JumpEqZero (UInt64.ofNat 3) "finish"; (3 ↦ Instr.LoadImmediate (UInt64.ofNat 3) l; (2 ↦ Instr.LoadAddress (UInt64.ofNat 2) c; (1 ↦ Instr.LoadAddress (UInt64.ofNat 1) k; (0 ↦ Instr.LoadAddress (UInt64.ofNat 0) p; TMap.empty Instr.Panic)))))))))))))), labels := p("finish" ↦ 14; p(".loop" ↦ 4; p("main" ↦ 0; PMap.empty))) }

    The loop-body Hoare proof (one iteration of the OTP loop), extracted from proof_otp_loop to keep each proof body within the size gate.

    source
    theorem proof_otp_loop (p k c l l' : UInt64) (h_l' : l' ∈ {4}) :
    hoareTripleUp (fun (st : MState) => (st.getRegisterAt 0 = p ∧ st.getRegisterAt 1 = k ∧ st.getRegisterAt 2 = c ∧ st.getRegisterAt 3 = l ∧ iPre p k c l) ∧ ¬st.terminated = true) (fun (st : MState) => ∀ i < l, st.getMemoryAt (c + i) = st.getMemoryAt (p + i) ^^^ st.getMemoryAt (k + i) ∧ ¬st.terminated = true) l' {14} ({n : UInt64 | n ≠ 14} \ ({n : UInt64 | n ≥ 4} ∩ {n : UInt64 | n < 14})) { instructionMap := (13 ↦ Instr.Jump ".loop"; (12 ↦ Instr.Decrement (UInt64.ofNat 3); (11 ↦ Instr.Increment (UInt64.ofNat 2); (10 ↦ Instr.Increment (UInt64.ofNat 1); (9 ↦ Instr.Increment (UInt64.ofNat 0); (8 ↦ Instr.StoreWord (UInt64.ofNat 7) (UInt64.ofNat 2); (7 ↦ Instr.XOR (UInt64.ofNat 7) (UInt64.ofNat 5) (UInt64.ofNat 6); (6 ↦ Instr.LoadWordReg (UInt64.ofNat 6) (UInt64.ofNat 1); (5 ↦ Instr.LoadWordReg (UInt64.ofNat 5) (UInt64.ofNat 0); (4 ↦ Instr.JumpEqZero (UInt64.ofNat 3) "finish"; (3 ↦ Instr.LoadImmediate (UInt64.ofNat 3) l; (2 ↦ Instr.LoadAddress (UInt64.ofNat 2) c; (1 ↦ Instr.LoadAddress (UInt64.ofNat 1) k; (0 ↦ Instr.LoadAddress (UInt64.ofNat 0) p; TMap.empty Instr.Panic)))))))))))))), labels := p("finish" ↦ 14; p(".loop" ↦ 4; p("main" ↦ 0; PMap.empty))) }

    The loop branch (program counter 4 to 14) of the One-Time-Pad correctness proof, extracted from proof_otp to keep each proof body within the size gate.

    source
    theorem proof_otp (p k c l : UInt64) :
    hoareTripleUp (fun (st : MState) => (p < k ∧ k < c ∧ c.toNat + l.toNat < UInt64.size ∧ p + l - 1 < k ∧ k + l - 1 < c) ∧ ¬st.terminated = true) (fun (st : MState) => ∀ i < l, st.getMemoryAt (c + i) = st.getMemoryAt (p + i) ^^^ st.getMemoryAt (k + i) ∧ ¬st.terminated = true) 0 {14} ({n : UInt64 | n > 14} ∪ {0}) { instructionMap := (13 ↦ Instr.Jump ".loop"; (12 ↦ Instr.Decrement (UInt64.ofNat 3); (11 ↦ Instr.Increment (UInt64.ofNat 2); (10 ↦ Instr.Increment (UInt64.ofNat 1); (9 ↦ Instr.Increment (UInt64.ofNat 0); (8 ↦ Instr.StoreWord (UInt64.ofNat 7) (UInt64.ofNat 2); (7 ↦ Instr.XOR (UInt64.ofNat 7) (UInt64.ofNat 5) (UInt64.ofNat 6); (6 ↦ Instr.LoadWordReg (UInt64.ofNat 6) (UInt64.ofNat 1); (5 ↦ Instr.LoadWordReg (UInt64.ofNat 5) (UInt64.ofNat 0); (4 ↦ Instr.JumpEqZero (UInt64.ofNat 3) "finish"; (3 ↦ Instr.LoadImmediate (UInt64.ofNat 3) l; (2 ↦ Instr.LoadAddress (UInt64.ofNat 2) c; (1 ↦ Instr.LoadAddress (UInt64.ofNat 1) k; (0 ↦ Instr.LoadAddress (UInt64.ofNat 0) p; TMap.empty Instr.Panic)))))))))))))), labels := p("finish" ↦ 14; p(".loop" ↦ 4; p("main" ↦ 0; PMap.empty))) }