def limb_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bytes.bend:176

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/src/crypto/secp256k1/bytes.bend as B
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/secp256k1/semiring.bend as SR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I

176# y 256 + x < 2^16 for bytes x, y
177def limb_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32) -> {Nat.is_lt(Nat.add(Nat.mul(B.byte(y), 256n), B.byte(x)), C.shift(16n, one)) == True{} : Bool}:
178  %Equal.sym(Nat, Nat.mul(B.byte(y), 256n), C.shift(8n, B.byte(y)), LV.m256(B.byte(y))) : {Nat.is_lt(Nat.add(_, B.byte(x)), C.shift(16n, one)) == True{} : Bool}
179  %Equal.sym(Nat, Nat.add(C.shift(8n, B.byte(y)), B.byte(x)), Nat.add(B.byte(x), C.shift(8n, B.byte(y))), NA.add_comm(C.shift(8n, B.byte(y)), B.byte(x))) : {Nat.is_lt(_, C.shift(16n, one)) == True{} : Bool}
180  %Equal.sym(Nat, C.shift(16n, one), C.shift(8n, C.shift(8n, one)), Equal.sym(Nat, C.shift(8n, C.shift(8n, one)), C.shift(16n, one), SR.shift_shift(8n, 8n, one))) : {Nat.is_lt(Nat.add(B.byte(x), C.shift(8n, B.byte(y))), _) == True{} : Bool}
181  I.digit_lt(8n, one, h1, B.byte(x), B.byte(y), C.shift(8n, one), byte_lt1(one, h1, x), byte_lt1(one, h1, y))