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) : 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 ∧ st.getRegisterAt 5 = st.getMemoryAt (st.getRegisterAt 0) ∧ st.getRegisterAt 6 = st.getMemoryAt (st.getRegisterAt 1) ∧ st.getRegisterAt 7 = st.getRegisterAt 5 ^^^ st.getRegisterAt 6 ∧ st.getRegisterAt 3 = x ∧ iPre' p k c l) ∧ ¬st.terminated = true) (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 ∧ st.getRegisterAt 5 = st.getMemoryAt (st.getRegisterAt 0) ∧ st.getRegisterAt 6 = st.getMemoryAt (st.getRegisterAt 1) ∧ st.getRegisterAt 7 = st.getRegisterAt 5 ^^^ st.getRegisterAt 6 ∧ st.getRegisterAt 3 = x ∧ iPre' p k c l) ∧ ¬st.terminated = true) 8 {9} {n : UInt64 | n ≠ 9} (otpCode p k c l)

theorem inc_otp_0 {x : UInt64} (p k c l : 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 ∧ st.getRegisterAt 5 = st.getMemoryAt (st.getRegisterAt 0) ∧ st.getRegisterAt 6 = st.getMemoryAt (st.getRegisterAt 1) ∧ st.getRegisterAt 7 = st.getRegisterAt 5 ^^^ st.getRegisterAt 6 ∧ st.getRegisterAt 3 = x ∧ iPre' p k c l) ∧ ¬st.terminated = true) (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 - 1)) ∧ st.getRegisterAt 1 = k + (l - st.getRegisterAt 3) ∧ st.getRegisterAt 2 = c + (l - st.getRegisterAt 3) ∧ st.getRegisterAt 3 ≤ l ∧ st.getRegisterAt 5 = st.getMemoryAt (st.getRegisterAt 0 - 1) ∧ st.getRegisterAt 6 = st.getMemoryAt (st.getRegisterAt 1) ∧ st.getRegisterAt 7 = st.getRegisterAt 5 ^^^ st.getRegisterAt 6 ∧ st.getRegisterAt 3 = x ∧ iPre' p k c l) ∧ ¬st.terminated = true) 9 {10} {n : UInt64 | n ≠ 10} (otpCode p k c l)

theorem inc_otp_1 {x : UInt64} (p k c l : 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 - 1)) ∧ st.getRegisterAt 1 = k + (l - st.getRegisterAt 3) ∧ st.getRegisterAt 2 = c + (l - st.getRegisterAt 3) ∧ st.getRegisterAt 3 ≤ l ∧ st.getRegisterAt 5 = st.getMemoryAt (st.getRegisterAt 0 - 1) ∧ st.getRegisterAt 6 = st.getMemoryAt (st.getRegisterAt 1) ∧ st.getRegisterAt 7 = st.getRegisterAt 5 ^^^ st.getRegisterAt 6 ∧ st.getRegisterAt 3 = x ∧ iPre' p k c l) ∧ ¬st.terminated = true) (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 - 1)) ∧ st.getRegisterAt 1 = k + (l - (st.getRegisterAt 3 - 1)) ∧ st.getRegisterAt 2 = c + (l - st.getRegisterAt 3) ∧ st.getRegisterAt 3 ≤ l ∧ st.getRegisterAt 5 = st.getMemoryAt (st.getRegisterAt 0 - 1) ∧ st.getRegisterAt 6 = st.getMemoryAt (st.getRegisterAt 1 - 1) ∧ st.getRegisterAt 7 = st.getRegisterAt 5 ^^^ st.getRegisterAt 6 ∧ st.getRegisterAt 3 = x ∧ iPre' p k c l) ∧ ¬st.terminated = true) 10 {11} {n : UInt64 | n ≠ 11} (otpCode p k c l)

theorem inc_otp_2 {x : UInt64} (p k c l : 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 - 1)) ∧ st.getRegisterAt 1 = k + (l - (st.getRegisterAt 3 - 1)) ∧ st.getRegisterAt 2 = c + (l - st.getRegisterAt 3) ∧ st.getRegisterAt 3 ≤ l ∧ st.getRegisterAt 5 = st.getMemoryAt (st.getRegisterAt 0 - 1) ∧ st.getRegisterAt 6 = st.getMemoryAt (st.getRegisterAt 1 - 1) ∧ st.getRegisterAt 7 = st.getRegisterAt 5 ^^^ st.getRegisterAt 6 ∧ st.getRegisterAt 3 = x ∧ iPre' p k c l) ∧ ¬st.terminated = true) (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 - 1)) ∧ st.getRegisterAt 1 = k + (l - (st.getRegisterAt 3 - 1)) ∧ st.getRegisterAt 2 = c + (l - (st.getRegisterAt 3 - 1)) ∧ st.getRegisterAt 3 ≤ l ∧ st.getRegisterAt 5 = st.getMemoryAt (st.getRegisterAt 0 - 1) ∧ st.getRegisterAt 6 = st.getMemoryAt (st.getRegisterAt 1 - 1) ∧ st.getRegisterAt 7 = st.getRegisterAt 5 ^^^ st.getRegisterAt 6 ∧ st.getRegisterAt 3 = x ∧ iPre' p k c l) ∧ ¬st.terminated = true) 11 {12} {n : UInt64 | n ≠ 12} (otpCode p k c l)

theorem dec_otp {x : UInt64} (p k c l : 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 - 1)) ∧ st.getRegisterAt 1 = k + (l - (st.getRegisterAt 3 - 1)) ∧ st.getRegisterAt 2 = c + (l - (st.getRegisterAt 3 - 1)) ∧ st.getRegisterAt 3 ≤ l ∧ st.getRegisterAt 5 = st.getMemoryAt (st.getRegisterAt 0 - 1) ∧ st.getRegisterAt 6 = st.getMemoryAt (st.getRegisterAt 1 - 1) ∧ st.getRegisterAt 7 = st.getRegisterAt 5 ^^^ st.getRegisterAt 6 ∧ st.getRegisterAt 3 = x ∧ iPre' p k c l) ∧ ¬st.terminated = true) (fun (st : MState) => ((∀ 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 ∧ st.getRegisterAt 5 = st.getMemoryAt (st.getRegisterAt 0 - 1) ∧ st.getRegisterAt 6 = st.getMemoryAt (st.getRegisterAt 1 - 1) ∧ st.getRegisterAt 7 = st.getRegisterAt 5 ^^^ st.getRegisterAt 6 ∧ st.getRegisterAt 3 < x ∧ iPre' p k c l) ∧ ¬st.terminated = true) 12 {13} {n : UInt64 | n ≠ 12 + 1} (otpCode p k c l)

theorem j_otp {x : UInt64} (p k c l : UInt64) : hoareTripleUp (fun (st : MState) => ((∀ 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 ∧ st.getRegisterAt 5 = st.getMemoryAt (st.getRegisterAt 0 - 1) ∧ st.getRegisterAt 6 = st.getMemoryAt (st.getRegisterAt 1 - 1) ∧ st.getRegisterAt 7 = st.getRegisterAt 5 ^^^ st.getRegisterAt 6 ∧ st.getRegisterAt 3 < x ∧ iPre' p k c l) ∧ ¬st.terminated = true) (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) 13 ({4} ∪ {14}) ({n : UInt64 | n ≠ 4} \ {14}) (otpCode p k c l)

theorem beqz_otp {x : UInt64} (p k c l : 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 ∧ st.getRegisterAt 3 = x ∧ iPre' p k c l) ∧ ¬st.terminated = true) (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 ∧ st.getRegisterAt 3 = x ∧ iPre' p k c l) ∧ ¬st.terminated = true) 4 {5} ({n : UInt64 | n ≤ 4} ∪ {n : UInt64 | n > 5}) (otpCode p k c l)