proofs/crypto/subtle/word.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend as MWord

2 imports

import Base
import ../../lib/logic.bend as L

Laws

law and_true proved
Also proved in bend-mathlib as bool.and_true: `import bend-mathlib@0.7.2.0/bool.bend as MBool`, then `MBool.and_true`.
source · line 8 · raw

@+b:Bool -> {Bool.and(b, True{}) == b : Bool}

law and_false proved
Also proved in bend-mathlib as bool.and_false: `import bend-mathlib@0.7.2.0/bool.bend as MBool`, then `MBool.and_false`.
source · line 19 · raw

@+b:Bool -> {Bool.and(b, False{}) == False{} : Bool}

law and_assoc proved
Also proved in bend-mathlib as bool.and_assoc: `import bend-mathlib@0.7.2.0/bool.bend as MBool`, then `MBool.and_assoc`.
source · line 30 · raw

@+a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}

law fin_eq provedsource · line 44 · raw

@+ab:Bool -> @+bb:Bool -> @+t:Cmp -> {Cmp.is_eq(Word.cmp.fin(ab, bb, t)) == Bool.and(Cmp.is_eq(t), Cmp.is_eq(Bool.cmp(ab, bb))) : Bool}

A comparison is EQ exactly when the tails compare EQ and the heads agree.

law bits_or provedsource · line 59 · raw

@+a:Bool -> @+b:Bool -> @+x:Bool -> @+y:Bool -> {Bool.and(Bool.and(a, b), Cmp.is_eq(Bool.cmp(Bool.or(x, y), False{}))) == Bool.and(Bool.and(a, Cmp.is_eq(Bool.cmp(x, False{}))), Bool.and(b, Cmp.is_eq(Bool.cmp(y, False{})))) : Bool}

law bits_xor provedsource · line 84 · raw

@+k:Bool -> @+x:Bool -> @+y:Bool -> {Bool.and(k, Cmp.is_eq(Bool.cmp(Bool.xor(x, y), False{}))) == Bool.and(k, Cmp.is_eq(Bool.cmp(x, y))) : Bool}

law bit_eq proved
Also proved in bend-mathlib as bool.eq_of_cmp_eq: `import bend-mathlib@0.7.2.0/bool.bend as MBool`, then `MBool.eq_of_cmp_eq`.
source · line 101 · raw

@+x:Bool -> @+y:Bool -> @+h:{Cmp.is_eq(Bool.cmp(x, y)) == True{} : Bool} -> {x == y : Bool}

law bit_refl provedsource · line 118 · raw

@+k:Bool -> @+x:Bool -> {Bool.and(k, Cmp.is_eq(Bool.cmp(x, x))) == k : Bool}

law or_zero provedsource · line 131 · raw

@+n:Nat -> @+x:Word(n) -> @+y:Word(n) -> {Cmp.is_eq(Word.cmp(n, Word.or(n, x, y), Word.zero(n))) == Bool.and(Cmp.is_eq(Word.cmp(n, x, Word.zero(n))), Cmp.is_eq(Word.cmp(n, y, Word.zero(n)))) : Bool}

zero(x | y) == zero(x) && zero(y)

law xor_zero provedsource · line 165 · raw

@+n:Nat -> @+x:Word(n) -> @+y:Word(n) -> {Cmp.is_eq(Word.cmp(n, Word.xor(n, x, y), Word.zero(n))) == Cmp.is_eq(Word.cmp(n, x, y)) : Bool}

zero(x ^ y) == (x == y)

law cmp_sound provedsource · line 191 · raw

@+n:Nat -> @+x:Word(n) -> @+y:Word(n) -> @+h:{Cmp.is_eq(Word.cmp(n, x, y)) == True{} : Bool} -> {x == y : Word(n)}

law cmp_refl provedsource · line 218 · raw

@+n:Nat -> @+x:Word(n) -> {Cmp.is_eq(Word.cmp(n, x, x)) == True{} : Bool}

law u32_or_zero provedsource · line 239 · raw

@+x:U32 -> @+y:U32 -> {U32.is_eq(U32.or(x, y), 0) == Bool.and(U32.is_eq(x, 0), U32.is_eq(y, 0)) : Bool}

law u32_xor_zero provedsource · line 249 · raw

@+x:U32 -> @+y:U32 -> {U32.is_eq(U32.xor(x, y), 0) == U32.is_eq(x, y) : Bool}

law u32_sound proved
Also proved in bend-mathlib as string.u32_eq_of_is_eq: `import bend-mathlib@0.7.2.0/string.bend as MString`, then `MString.u32_eq_of_is_eq`.
source · line 259 · raw

@+x:U32 -> @+y:U32 -> @+h:{U32.is_eq(x, y) == True{} : Bool} -> {x == y : U32}

law u32_refl provedsource · line 271 · raw

@+x:U32 -> {U32.is_eq(x, x) == True{} : Bool}