proofs/crypto/subtle/laws.bend source

proofs/crypto/subtle/laws.bend on the hub · documented module

import Baseimport ../../../src/crypto/subtle.bend as Subtleimport ../../../spec/crypto/subtle.bend as Spec# The clauses of spec/crypto/subtle.bend. Proved in proof.bend.# eq returns the reference list equality.law Eq.value:  for +a: List<&2, U32>  for +b: List<&2, U32>  {Subtle.eq(a, b) == Spec.equal(a, b) : Bool}# eq is True only for equal lists.law Eq.sound:  for +a: List<&2, U32>  for +b: List<&2, U32>  for +h: {Subtle.eq(a, b) == True{} : Bool}  {a == b : List<&2, U32>}# eq is True on equal lists.law Eq.refl:  for +a: List<&2, U32>  {Subtle.eq(a, a) == True{} : Bool}