def bits_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bitsv.bend:111

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/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/logic.bend as Lg
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/math/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV

111# the bits of n limbs below 2^16 spell their value
112def bits_v(+one: Nat, +h1: {one == 1n : Nat}, n: Nat, xs: List<&2, Nat>, +e: Nat, +hx: {FS.limbs16(one, n, xs) == True{} : Bool}) -> {hv(L.bits(xs), one, e) == Nat.add(LV.pos(n, e), FS.digits(one, xs)) : Nat}:
113  match n xs:
114    case 0n Nil{}:
115      %Equal.sym(Nat, Nat.add(e, 0n), e, NA.add_zero(e)) : {e == _ : Nat}
116      {==}
117    case 0n x <> t:
118      Empty.absurd({hv(L.bits(x <> t), one, e) == Nat.add(LV.pos(0n, e), FS.digits(one, x <> t)) : Nat}, Lg.false_true(hx))
119    case 1n+k Nil{}:
120      Empty.absurd({hv(L.bits([]), one, e) == Nat.add(LV.pos(1n+k, e), FS.digits(one, [])) : Nat}, Lg.false_true(hx))
121    case 1n+ +k +x <> +t:
122      +hx0 = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), hx)
123      +ht = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), hx)
124      %Equal.sym(Nat, hv(List.append(&2, Nat, L.bits(t), L.bits_of(16n, x)), one, e), hv(L.bits_of(16n, x), one, hv(L.bits(t), one, e)), hv_app(one, L.bits(t), e, L.bits_of(16n, x))) : {_ == Nat.add(C.shift(16n, LV.pos(k, e)), Nat.add(Nat.mul(one, x), C.shift(16n, FS.digits(one, t)))) : Nat}
125      %Equal.sym(Nat, hv(L.bits_of(16n, x), one, hv(L.bits(t), one, e)), Nat.add(C.shift(16n, hv(L.bits(t), one, e)), Nat.mul(one, x)), bits_of_v(one, h1, 16n, x, hv(L.bits(t), one, e), hx0)) : {_ == Nat.add(C.shift(16n, LV.pos(k, e)), Nat.add(Nat.mul(one, x), C.shift(16n, FS.digits(one, t)))) : Nat}
126      %Equal.sym(Nat, hv(L.bits(t), one, e), Nat.add(LV.pos(k, e), FS.digits(one, t)), bits_v(one, h1, k, t, e, ht)) : {Nat.add(C.shift(16n, _), Nat.mul(one, x)) == Nat.add(C.shift(16n, LV.pos(k, e)), Nat.add(Nat.mul(one, x), C.shift(16n, FS.digits(one, t)))) : Nat}
127      %Equal.sym(Nat, Nat.add(LV.pos(k, e), FS.digits(one, t)), Nat.add(FS.digits(one, t), LV.pos(k, e)), NA.add_comm(LV.pos(k, e), FS.digits(one, t))) : {Nat.add(C.shift(16n, _), Nat.mul(one, x)) == Nat.add(C.shift(16n, LV.pos(k, e)), Nat.add(Nat.mul(one, x), C.shift(16n, FS.digits(one, t)))) : Nat}
128      %Equal.sym(Nat, C.shift(16n, Nat.add(FS.digits(one, t), LV.pos(k, e))), Nat.add(C.shift(16n, FS.digits(one, t)), C.shift(16n, LV.pos(k, e))), WW.shift_add(16n, FS.digits(one, t), LV.pos(k, e))) : {Nat.add(_, Nat.mul(one, x)) == Nat.add(C.shift(16n, LV.pos(k, e)), Nat.add(Nat.mul(one, x), C.shift(16n, FS.digits(one, t)))) : Nat}
129      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, FS.digits(one, t)), C.shift(16n, LV.pos(k, e))), Nat.mul(one, x)), Nat.add(C.shift(16n, FS.digits(one, t)), Nat.add(C.shift(16n, LV.pos(k, e)), Nat.mul(one, x))), NA.add_assoc(C.shift(16n, FS.digits(one, t)), C.shift(16n, LV.pos(k, e)), Nat.mul(one, x))) : {_ == Nat.add(C.shift(16n, LV.pos(k, e)), Nat.add(Nat.mul(one, x), C.shift(16n, FS.digits(one, t)))) : Nat}
130      %Equal.sym(Nat, Nat.add(Nat.mul(one, x), C.shift(16n, FS.digits(one, t))), Nat.add(C.shift(16n, FS.digits(one, t)), Nat.mul(one, x)), NA.add_comm(Nat.mul(one, x), C.shift(16n, FS.digits(one, t)))) : {Nat.add(C.shift(16n, FS.digits(one, t)), Nat.add(C.shift(16n, LV.pos(k, e)), Nat.mul(one, x))) == Nat.add(C.shift(16n, LV.pos(k, e)), _) : Nat}
131      %Equal.sym(Nat, Nat.add(C.shift(16n, LV.pos(k, e)), Nat.add(C.shift(16n, FS.digits(one, t)), Nat.mul(one, x))), Nat.add(C.shift(16n, FS.digits(one, t)), Nat.add(C.shift(16n, LV.pos(k, e)), Nat.mul(one, x))), NA.add_swap(C.shift(16n, LV.pos(k, e)), C.shift(16n, FS.digits(one, t)), Nat.mul(one, x))) : {Nat.add(C.shift(16n, FS.digits(one, t)), Nat.add(C.shift(16n, LV.pos(k, e)), Nat.mul(one, x))) == _ : Nat}
132      {==}