def hi_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/limbs.bend:193

import Base
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/arith.bend as AR
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

193# (s div 256) < 2^k when s < 2^(k + 8)
194def hi_lt(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +s: U32, +h: {Nat.is_lt(v(s), WD.sc(Nat.add(k, 8n), one)) == True{} : Bool}) -> {Nat.is_lt(v(U32.div(s, 256)), WD.sc(k, one)) == True{} : Bool}:
195  %Equal.sym(Nat, v(U32.div(s, 256)), Nat.div(v(s), 256n), div256(s)) : {Nat.is_lt(_, WD.sc(k, one)) == True{} : Bool}
196  +n = v(s)
197  +q = Nat.div(n, 256n)
198  +r = Nat.mod(n, 256n)
199  +e = NR.dm_eq(255n, n)
200  +h2 = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(Nat.add(k, 8n), one)) == True{} : Bool}, n, Nat.add(Nat.mul(q, 256n), r), e, h)
201  +h3 = L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.mul(q, 256n), r), z) == True{} : Bool}, WD.sc(Nat.add(k, 8n), one), WD.sc(k, WD.sc(8n, one)), AR.sc_idx(k, 8n, one), h2)
202  +h4 = L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.mul(q, 256n), r), WD.sc(k, z)) == True{} : Bool}, WD.sc(8n, one), 256n, Equal.sym(Nat, 256n, WD.sc(8n, one), k256(one, h1)), h3)
203  AR.quot_lt(k, one, h1, q, 256n, r, h4)