proofs/crypto/aead/subtle_eq.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/subtle_eq.bend as Subtle_eq

5 imports

import Base
import ../../../src/crypto/subtle.bend as Subtle
import ../../../spec/crypto/subtle.bend as SS
import ../../lib/logic.bend as L
import ../subtle/word.bend as SW

Laws

law step provedsource · line 10 · raw

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

law fold provedsource · line 25 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+acc:U32 -> {Bool.and(Nat.is_eq(List.length(&2, U32, a), List.length(&2, U32, b)), U32.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/subtle.diff(a, b, acc), 0)) == Bool.and(U32.is_eq(acc, 0), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/subtle.equal(a, b)) : Bool}

law equal_sound provedsource · line 49 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/subtle.equal(a, b) == True{} : Bool} -> {a == b : List<&2, U32>}

law equal_refl provedsource · line 67 · raw

@+a:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/subtle.equal(a, a) == True{} : Bool}

law eq_value provedsource · line 78 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/subtle.eq(a, b) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/subtle.equal(a, b) : Bool}