def bits_sb

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bitsrel.bend:112

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/crypto/secp256k1/limbs.bend as LV
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as BY

112# the bits of n limbs below 2^16
113def bits_sb(+one: Nat, +h1: {one == 1n : Nat}, n: Nat, xs: List<&2, Nat>, +h: {FS.limbs16(one, n, xs) == True{} : Bool}) -> {L.bits(xs) == sb(Nat.mul(n, 16n), 0n, LV.ev(xs)) : List<&2, Nat>}:
114  match n xs:
115    case 0n Nil{}:
116      {==}
117    case 0n x <> t:
118      Empty.absurd({L.bits(x <> t) == sb(Nat.mul(0n, 16n), 0n, LV.ev(x <> t)) : List<&2, Nat>}, Lg.false_true(h))
119    case 1n+k Nil{}:
120      Empty.absurd({L.bits([]) == sb(Nat.mul(1n+k, 16n), 0n, LV.ev([])) : List<&2, Nat>}, Lg.false_true(h))
121    case 1n+ +k +x <> +t:
122      +hx = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), h)
123      +ht = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), h)
124      +f16 = BY.fits_one(16n, one, h1, x, hx)
125      %Equal.sym(Nat, Nat.add(16n, Nat.mul(k, 16n)), Nat.add(Nat.mul(k, 16n), 16n), NA.add_comm(16n, Nat.mul(k, 16n))) : {List.append(&2, Nat, L.bits(t), L.bits_of(16n, x)) == sb(_, 0n, Nat.add(x, C.shift(16n, LV.ev(t)))) : List<&2, Nat>}
126      %Equal.sym(List<&2, Nat>, sb(Nat.add(Nat.mul(k, 16n), 16n), 0n, Nat.add(x, C.shift(16n, LV.ev(t)))), List.append(&2, Nat, sb(Nat.mul(k, 16n), 16n, Nat.add(x, C.shift(16n, LV.ev(t)))), sb(16n, 0n, Nat.add(x, C.shift(16n, LV.ev(t))))), sb_split(Nat.mul(k, 16n), 16n, Nat.add(x, C.shift(16n, LV.ev(t))))) : {List.append(&2, Nat, L.bits(t), L.bits_of(16n, x)) == _ : List<&2, Nat>}
127      %Equal.sym(List<&2, Nat>, sb(Nat.mul(k, 16n), 16n, Nat.add(x, C.shift(16n, LV.ev(t)))), sb(Nat.mul(k, 16n), 0n, LV.ev(t)), sb_hi(Nat.mul(k, 16n), x, LV.ev(t), f16)) : {List.append(&2, Nat, L.bits(t), L.bits_of(16n, x)) == List.append(&2, Nat, _, sb(16n, 0n, Nat.add(x, C.shift(16n, LV.ev(t))))) : List<&2, Nat>}
128      %Equal.sym(List<&2, Nat>, L.bits(t), sb(Nat.mul(k, 16n), 0n, LV.ev(t)), bits_sb(one, h1, k, t, ht)) : {List.append(&2, Nat, _, L.bits_of(16n, x)) == List.append(&2, Nat, sb(Nat.mul(k, 16n), 0n, LV.ev(t)), sb(16n, 0n, Nat.add(x, C.shift(16n, LV.ev(t))))) : List<&2, Nat>}
129      %Equal.sym(List<&2, Nat>, L.bits_of(16n, x), sb(16n, 0n, x), bits_of_sb(16n, x)) : {List.append(&2, Nat, sb(Nat.mul(k, 16n), 0n, LV.ev(t)), _) == List.append(&2, Nat, sb(Nat.mul(k, 16n), 0n, LV.ev(t)), sb(16n, 0n, Nat.add(x, C.shift(16n, LV.ev(t))))) : List<&2, Nat>}
130      %Equal.sym(List<&2, Nat>, sb(16n, 0n, Nat.add(x, C.shift(16n, LV.ev(t)))), sb(16n, 0n, x), sb_lo(16n, 0n, x, LV.ev(t))) : {List.append(&2, Nat, sb(Nat.mul(k, 16n), 0n, LV.ev(t)), sb(16n, 0n, x)) == List.append(&2, Nat, sb(Nat.mul(k, 16n), 0n, LV.ev(t)), _) : List<&2, Nat>}
131      {==}