def last_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/reduce.bend:124

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/u32.bend as U
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as PL

124# a pass of a value below 2^256 carries out 0: the output is the carry's limbs
125def last_zero(+one: Nat, +h1: {one == 1n : Nat}, +a: Nat, +c: Nat, +V: Nat, +hv: {Nat.add(a, LM.shn(32n, c)) == V : Nat}, +hV: {Nat.is_lt(V, LM.shn(32n, one)) == True{} : Bool}, +b: Bool, +hb: {Nat.is_lt(c, one) == b : Bool}) -> {c == 0n : Nat}:
126  match b:
127    case True{}:
128      U.lt_one_zero(c, L.subst(Nat, o => {Nat.is_lt(c, o) == True{} : Bool}, one, 1n, h1, hb))
129    case False{}:
130      +hs = shn_ge(one, c, N.not_lt_le(c, one, hb))
131      +x = N.le_trans(LM.shn(32n, one), LM.shn(32n, c), V, hs, L.subst(Nat, z => {Nat.is_le(LM.shn(32n, c), z) == True{} : Bool}, Nat.add(a, LM.shn(32n, c)), V, hv, PL.le_add_l(a, LM.shn(32n, c))))
132      Empty.absurd({c == 0n : Nat}, L.true_not_false(Nat.is_lt(V, LM.shn(32n, one)), hV, N.le_not_lt(V, LM.shn(32n, one), x)))