def lo16_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bounds.bend:47

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/limbs.bend as L
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

47def lo16_lt(+one: Nat, +h1: {one == 1n : Nat}, +s: Nat) -> {Nat.is_lt(L.lo16(s), C.shift(16n, one)) == True{} : Bool}:
48  %Equal.sym(Nat, Nat.mul(Nat.mod(Nat.div(s, 256n), 256n), 256n), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), LV.m256(Nat.mod(Nat.div(s, 256n), 256n))) : {Nat.is_lt(Nat.add(Nat.mod(s, 256n), _), C.shift(16n, one)) == True{} : Bool}
49  %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(Nat.mod(s, 256n), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n))), _) == True{} : Bool}
50  I.digit_lt(8n, one, h1, Nat.mod(s, 256n), Nat.mod(Nat.div(s, 256n), 256n), C.shift(8n, one), mod256_lt(one, h1, s), mod256_lt(one, h1, Nat.div(s, 256n)))