def or_le

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/xbits.bend:122

import Base
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/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as SN
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M

122def or_le(+n: Nat, +x: Word(n), +m: Word(n)) -> {Nat.is_le(WD.uw(n, Word.or(n, x, m)), Nat.add(WD.uw(n, x), WD.uw(n, m))) == True{} : Bool}:
123  match n x m:
124    case 0n WNil{} WNil{}:
125      {==}
126    case 1n+ +p WCon{+a, +t1} WCon{+b, +t2}:
127      +u1 = WD.uw(p, t1)
128      +u2 = WD.uw(p, t2)
129      +d1 = N.double_le(WD.uw(p, Word.or(p, t1, t2)), Nat.add(u1, u2), or_le(p, t1, t2))
130      +d2 = L.subst(Nat, z => {Nat.is_le(Nat.double(WD.uw(p, Word.or(p, t1, t2))), z) == True{} : Bool}, Nat.double(Nat.add(u1, u2)), Nat.add(Nat.double(u1), Nat.double(u2)), NA.double_add(u1, u2), d1)
131      +s = M.le_add2(SN.bit_value(Bool.or(a, b)), Nat.double(WD.uw(p, Word.or(p, t1, t2))), Nat.add(SN.bit_value(a), SN.bit_value(b)), Nat.add(Nat.double(u1), Nat.double(u2)), bit_or_le(a, b), d2)
132      L.subst(Nat, z => {Nat.is_le(Nat.add(SN.bit_value(Bool.or(a, b)), Nat.double(WD.uw(p, Word.or(p, t1, t2)))), z) == True{} : Bool}, Nat.add(Nat.add(SN.bit_value(a), SN.bit_value(b)), Nat.add(Nat.double(u1), Nat.double(u2))), Nat.add(Nat.add(SN.bit_value(a), Nat.double(u1)), Nat.add(SN.bit_value(b), Nat.double(u2))), M.add4(SN.bit_value(a), SN.bit_value(b), Nat.double(u1), Nat.double(u2)), s)