~/jendhub

def and_le

bend-collections-laws-crypto@1.0.0.0 · proofs/math/hash/hash.bend:30

import bend-collections-laws-crypto@1.0.0.0/proofs/math/hash/hash.bend as Hash
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD

30# masking never exceeds the mask
31def and_le(+n: Nat, +x: Word(n), +m: Word(n)) -> {Nat.is_le(WD.uw(n, Word.and(n, x, m)), WD.uw(n, m)) == True{} : Bool}:
32  match n x m:
33    case 0n WNil{} WNil{}:
34      {==}
35    case 1n+p WCon{a, t1} WCon{b, t2}:
36      add_le(S.bit_value(Bool.and(a, b)), S.bit_value(b), Nat.double(WD.uw(p, Word.and(p, t1, t2))), Nat.double(WD.uw(p, t2)), bit_and_le(a, b), N.double_le(WD.uw(p, Word.and(p, t1, t2)), WD.uw(p, t2), and_le(p, t1, t2)))

Uses (14)

Used by (1)