proofs/crypto/subtle/proof.bend checks

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

6 imports

import Base
import ../../../src/crypto/subtle.bend as Subtle
import ../../../spec/crypto/subtle.bend as Spec
import ../../lib/logic.bend as L
import ./word.bend as W
import ./laws.bend as Laws

Laws

law step provedsource · line 13 · 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}

Gate for src/crypto/subtle.bend: bend proofs/crypto/subtle/proof.bend.

The accumulator invariant (the shape of HACL*'s lbytes_eq proof): after the common prefix, "lengths agree and the accumulator is zero" is "the starting accumulator is zero and the lists are equal".

law fold provedsource · line 28 · 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 55 · 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 80 · raw

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