def and_le

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/below.bend:19

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as SR
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/math/typed/width.bend as WI
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA

19# x & m <= m
20def and_le(+w: Nat, +a: Nat, +b: Nat) -> {Nat.is_le(SR.and_bits(w, a, b), b) == True{} : Bool}:
21  match w:
22    case 0n:
23      N.zero_le(b)
24    case 1n+p:
25      +hb = WI.hb(b)
26      +h1 = WA.mul_le1(C.bit(a), C.bit(b), WI.bit_le1(a))
27      +h2 = N.double_le(SR.and_bits(p, C.half(a), C.half(b)), C.half(b), and_le(p, C.half(a), C.half(b)))
28      +h3 = N.le_trans(Nat.add(Nat.mul(C.bit(a), C.bit(b)), Nat.double(SR.and_bits(p, C.half(a), C.half(b)))), Nat.add(C.bit(b), Nat.double(SR.and_bits(p, C.half(a), C.half(b)))), Nat.add(C.bit(b), Nat.double(C.half(b))),
29        WI.le_add_r(Nat.mul(C.bit(a), C.bit(b)), C.bit(b), Nat.double(SR.and_bits(p, C.half(a), C.half(b))), h1),
30        N.le_add_left(Nat.double(SR.and_bits(p, C.half(a), C.half(b))), Nat.double(C.half(b)), C.bit(b), h2))
31      %Equal.sym(Nat, b, Nat.add(C.bit(b), Nat.double(C.half(b))), hb) : {Nat.is_le(Nat.add(Nat.mul(C.bit(a), C.bit(b)), Nat.double(SR.and_bits(p, C.half(a), C.half(b)))), _) == True{} : Bool}
32      h3