~/bend-docscommunity

proofs/crypto/subtle/laws.bend open laws/TODOs

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

3 imports
import Base
import ../../../src/crypto/subtle.bend as Subtle
import ../../../spec/crypto/subtle.bend as Spec

Laws

law Eq.value openits proof in laws_crypto.bend does not pass the checker (fails)source · line 8 · raw

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

eq returns the reference list equality.

law Eq.sound openits proof in laws_crypto.bend does not pass the checker (fails)source · line 14 · raw

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

eq is True only for equal lists.

law Eq.refl openits proof in laws_crypto.bend does not pass the checker (fails)source · line 21 · raw

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

eq is True on equal lists.