SingleProofsOTP

This module provides the per-instruction lemmas of the One-Time-Pad proof.

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

The precondition shared by the per-instruction One-Time-Pad proofs, 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 help_I_pre' {x : UInt64} (p k c l : UInt64) : iPre' p k c l → c + (l - x) ≠ p + (l - x)

theorem help_I_pre'' {x : UInt64} (p k c l : UInt64) : iPre' p k c l → c + (l - x) ≠ k + (l - x)

theorem help_I_pre''' (p k c l i x : UInt64) : iPre' p k c l → i < l - x → x ≤ l → c + (l - x) ≠ k + i

theorem help_I_pre'''' (p k c l i x : UInt64) : iPre' p k c l → i < l - x → x ≤ l → c + (l - x) ≠ p + i

theorem help_I_pre''''' (p k c l i x : UInt64) : iPre' p k c l → i.toNat < (l - x).toNat → x ≤ l → c + (l - x) ≠ c + i

def otpCode (p k c l : UInt64) : Code

The One-Time-Pad program, parameterised by the plaintext p, key k, ciphertext c, and length l memory addresses.

Equations

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

theorem sw_otp {x : UInt64} (p k c l : UInt64) : c? ⦃(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 ∧ x[5] = mem[x[0]] ∧ x[6] = mem[x[1]] ∧ x[7] = x[5] ^^^ x[6] ∧ x[3] = x ∧ iPre' p k c l) ∧ ¬⸨terminated⸩ = true⦄ 8 ↦ ⟨{9} | {n : UInt64 | n ≠ 9}⟩⦃(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 ∧ x[5] = mem[x[0]] ∧ x[6] = mem[x[1]] ∧ x[7] = x[5] ^^^ x[6] ∧ x[3] = x ∧ iPre' p k c l) ∧ ¬⸨terminated⸩ = true⦄

theorem inc_otp_0 {x : UInt64} (p k c l : UInt64) : c? ⦃(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 ∧ x[5] = mem[x[0]] ∧ x[6] = mem[x[1]] ∧ x[7] = x[5] ^^^ x[6] ∧ x[3] = x ∧ iPre' p k c l) ∧ ¬⸨terminated⸩ = true⦄ 9 ↦ ⟨{10} | {n : UInt64 | n ≠ 10}⟩⦃(x[3] > 0 ∧ (∀ i ≤ l - x[3], mem[c + i] = mem[p + i] ^^^ mem[k + i]) ∧ x[0] = p + (l - (x[3] - 1)) ∧ x[1] = k + (l - x[3]) ∧ x[2] = c + (l - x[3]) ∧ x[3] ≤ l ∧ x[5] = mem[x[0] - 1] ∧ x[6] = mem[x[1]] ∧ x[7] = x[5] ^^^ x[6] ∧ x[3] = x ∧ iPre' p k c l) ∧ ¬⸨terminated⸩ = true⦄

theorem inc_otp_1 {x : UInt64} (p k c l : UInt64) : c? ⦃(x[3] > 0 ∧ (∀ i ≤ l - x[3], mem[c + i] = mem[p + i] ^^^ mem[k + i]) ∧ x[0] = p + (l - (x[3] - 1)) ∧ x[1] = k + (l - x[3]) ∧ x[2] = c + (l - x[3]) ∧ x[3] ≤ l ∧ x[5] = mem[x[0] - 1] ∧ x[6] = mem[x[1]] ∧ x[7] = x[5] ^^^ x[6] ∧ x[3] = x ∧ iPre' p k c l) ∧ ¬⸨terminated⸩ = true⦄ 10 ↦ ⟨{11} | {n : UInt64 | n ≠ 11}⟩⦃(x[3] > 0 ∧ (∀ i ≤ l - x[3], mem[c + i] = mem[p + i] ^^^ mem[k + i]) ∧ x[0] = p + (l - (x[3] - 1)) ∧ x[1] = k + (l - (x[3] - 1)) ∧ x[2] = c + (l - x[3]) ∧ x[3] ≤ l ∧ x[5] = mem[x[0] - 1] ∧ x[6] = mem[x[1] - 1] ∧ x[7] = x[5] ^^^ x[6] ∧ x[3] = x ∧ iPre' p k c l) ∧ ¬⸨terminated⸩ = true⦄

theorem inc_otp_2 {x : UInt64} (p k c l : UInt64) : c? ⦃(x[3] > 0 ∧ (∀ i ≤ l - x[3], mem[c + i] = mem[p + i] ^^^ mem[k + i]) ∧ x[0] = p + (l - (x[3] - 1)) ∧ x[1] = k + (l - (x[3] - 1)) ∧ x[2] = c + (l - x[3]) ∧ x[3] ≤ l ∧ x[5] = mem[x[0] - 1] ∧ x[6] = mem[x[1] - 1] ∧ x[7] = x[5] ^^^ x[6] ∧ x[3] = x ∧ iPre' p k c l) ∧ ¬⸨terminated⸩ = true⦄ 11 ↦ ⟨{12} | {n : UInt64 | n ≠ 12}⟩⦃(x[3] > 0 ∧ (∀ i ≤ l - x[3], mem[c + i] = mem[p + i] ^^^ mem[k + i]) ∧ x[0] = p + (l - (x[3] - 1)) ∧ x[1] = k + (l - (x[3] - 1)) ∧ x[2] = c + (l - (x[3] - 1)) ∧ x[3] ≤ l ∧ x[5] = mem[x[0] - 1] ∧ x[6] = mem[x[1] - 1] ∧ x[7] = x[5] ^^^ x[6] ∧ x[3] = x ∧ iPre' p k c l) ∧ ¬⸨terminated⸩ = true⦄

theorem dec_otp {x : UInt64} (p k c l : UInt64) : c? ⦃(x[3] > 0 ∧ (∀ i ≤ l - x[3], mem[c + i] = mem[p + i] ^^^ mem[k + i]) ∧ x[0] = p + (l - (x[3] - 1)) ∧ x[1] = k + (l - (x[3] - 1)) ∧ x[2] = c + (l - (x[3] - 1)) ∧ x[3] ≤ l ∧ x[5] = mem[x[0] - 1] ∧ x[6] = mem[x[1] - 1] ∧ x[7] = x[5] ^^^ x[6] ∧ x[3] = x ∧ iPre' p k c l) ∧ ¬⸨terminated⸩ = true⦄ 12 ↦ ⟨{13} | {n : UInt64 | n ≠ 12 + 1}⟩⦃((∀ 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 ∧ x[5] = mem[x[0] - 1] ∧ x[6] = mem[x[1] - 1] ∧ x[7] = x[5] ^^^ x[6] ∧ x[3] < x ∧ iPre' p k c l) ∧ ¬⸨terminated⸩ = true⦄

theorem j_otp {x : UInt64} (p k c l : UInt64) : c? ⦃((∀ 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 ∧ x[5] = mem[x[0] - 1] ∧ x[6] = mem[x[1] - 1] ∧ x[7] = x[5] ^^^ x[6] ∧ x[3] < x ∧ iPre' p k c l) ∧ ¬⸨terminated⸩ = true⦄ 13 ↦ ⟨{4} ∪ {14} | {n : UInt64 | n ≠ 4} \ {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⦄

theorem beqz_otp {x : UInt64} (p k c l : UInt64) : c? ⦃(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 ∧ x[3] = x ∧ iPre' p k c l) ∧ ¬⸨terminated⸩ = true⦄ 4 ↦ ⟨{5} | {n : UInt64 | n ≤ 4} ∪ {n : UInt64 | n > 5}⟩⦃(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 ∧ x[3] = x ∧ iPre' p k c l) ∧ ¬⸨terminated⸩ = true⦄