OtpProof

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

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

• iPre p k c l = (p < k ∧ k < c ∧ c.toNat + l.toNat < UInt64.size ∧ p + l - 1 < k ∧ k + l - 1 < c)

theorem proof_otp_loopBody (p k c l : UInt64) (s : MState) : s.code = mriscx main: la x 0, p la x 1, k la x 2, c li x 3, l .loop: beqz x 3, finish lw x 5, x 0 lw x 6, x 1 xor x 7, x 5, x 6 sw x 7, x 2 inc x 0 inc x 1 inc x 2 dec x 3 j [anonymous] finish: end → 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), mriscx main: la x 0, p la x 1, k la x 2, c li x 3, l .loop: beqz x 3, finish lw x 5, x 0 lw x 6, x 1 xor x 7, x 5, x 6 sw x 7, x 2 inc x 0 inc x 1 inc x 2 dec x 3 j [anonymous] finish: end ⦃x[3] > 0 ∧ (((∀ i < l - x[3], mem[c + i] = mem[p + i] ^^^ mem[k + i]) ∧ x[0] = p + (l - x[3]) ∧ x[1] = k + (l - x[3]) ∧ x[2] = c + (l - x[3]) ∧ x[3] ≤ l ∧ iPre p k c l) ∧ ¬⸨terminated⸩ = true) ∧ x[3] = x⦄ 4 ↦ ⟨{4} ∪ {14} | {n : UInt64 | n ≠ 14} \ ({n : UInt64 | n ≥ 4} ∩ {n : UInt64 | n < 14})⟩⦃x[3] < x ∧ (((∀ i < l - x[3], mem[c + i] = mem[p + i] ^^^ mem[k + i]) ∧ x[0] = p + (l - x[3]) ∧ x[1] = k + (l - x[3]) ∧ x[2] = c + (l - x[3]) ∧ x[3] ≤ l ∧ iPre p k c l) ∧ ¬⸨terminated⸩ = true) ∧ ⸨pc⸩ = 4⦄

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.

theorem proof_otp_loop (p k c l l' : UInt64) (h_l' : l' ∈ {4}) : mriscx main: la x 0, p la x 1, k la x 2, c li x 3, l .loop: beqz x 3, finish lw x 5, x 0 lw x 6, x 1 xor x 7, x 5, x 6 sw x 7, x 2 inc x 0 inc x 1 inc x 2 dec x 3 j [anonymous] finish: end ⦃(x[0] = p ∧ x[1] = k ∧ x[2] = c ∧ x[3] = l ∧ iPre p k c l) ∧ ¬⸨terminated⸩ = true⦄ l' ↦ ⟨{14} | {n : UInt64 | n ≠ 14} \ ({n : UInt64 | n ≥ 4} ∩ {n : UInt64 | n < 14})⟩⦃∀ i < l, mem[c + i] = mem[p + i] ^^^ mem[k + i] ∧ ¬⸨terminated⸩ = true⦄

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.

theorem proof_otp (p k c l : UInt64) : mriscx main: la x 0, p la x 1, k la x 2, c li x 3, l .loop: beqz x 3, finish lw x 5, x 0 lw x 6, x 1 xor x 7, x 5, x 6 sw x 7, x 2 inc x 0 inc x 1 inc x 2 dec x 3 j [anonymous] finish: end ⦃(p < k ∧ k < c ∧ c.toNat + l.toNat < UInt64.size ∧ p + l - 1 < k ∧ k + l - 1 < c) ∧ ¬⸨terminated⸩ = true⦄ 0 ↦ ⟨{14} | {n : UInt64 | n > 14} ∪ {0}⟩⦃∀ i < l, mem[c + i] = mem[p + i] ^^^ mem[k + i] ∧ ¬⸨terminated⸩ = true⦄