def canon_lb

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/reduce.bend:262

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
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/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend as B

262def canon_lb(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +t: List<&2, Nat>, +ht16: {FS.limbs16(one, 16n, t) == True{} : Bool}, b: Nat, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> {FS.limbs16(one, 16n, L.select(b, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t)) == True{} : Bool}:
263  match b:
264    case 0n:
265      +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(t, c), 0n, {==})
266      %Equal.sym(List<&2, Nat>, L.select(0n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t), t, sel_zero(one, 16n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t, hu16, ht16)) : {FS.limbs16(one, 16n, _) == True{} : Bool}
267      ht16
268    case 1n:
269      +hu16 = B.carry_limbs(one, h1, 32n, 16n, L.add(t, c), 0n, {==})
270      %Equal.sym(List<&2, Nat>, L.select(1n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t), L.take(16n, L.carry(32n, L.add(t, c), 0n)), sel_one(one, 16n, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t, hu16, ht16)) : {FS.limbs16(one, 16n, _) == True{} : Bool}
271      hu16
272    case 2n+ +k:
273      Empty.absurd({FS.limbs16(one, 16n, L.select(2n+k, L.take(16n, L.carry(32n, L.add(t, c), 0n)), t)) == True{} : Bool}, N.lt_zero_absurd(k, hb))