~/jendhub

def comp_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/negate.bend:104

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend as Negate
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

104# comp(x) + x + 1 = 2^(16 n) for n limbs below 2^16
105def comp_v(+one: Nat, +h1: {one == 1n : Nat}, n: Nat, xs: List<&2, Nat>, +h: {FS.limbs16(one, n, xs) == True{} : Bool}) -> {Nat.add(Nat.add(LV.ev(L.comp(xs)), LV.ev(xs)), one) == LV.pos(n, one) : Nat}:
106  match n xs:
107    case 0n Nil{}:
108      {==}
109    case 0n x <> t:
110      Empty.absurd({Nat.add(Nat.add(LV.ev(L.comp(x <> t)), LV.ev(x <> t)), one) == LV.pos(0n, one) : Nat}, Lg.false_true(h))
111    case 1n+k Nil{}:
112      Empty.absurd({Nat.add(Nat.add(LV.ev(L.comp([])), LV.ev([])), one) == LV.pos(1n+k, one) : Nat}, Lg.false_true(h))
113    case 1n+ +k +x <> +t:
114      +hx = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), h)
115      +ht = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), h)
116      %Equal.sym(Nat, LV.pos(k, one), Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one), Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one), LV.pos(k, one), comp_v(one, h1, k, t, ht))) : {Nat.add(Nat.add(Nat.add(L.comp1(x), C.shift(16n, LV.ev(L.comp(t)))), Nat.add(x, C.shift(16n, LV.ev(t)))), one) == C.shift(16n, _) : Nat}
117      %Equal.sym(Nat, Nat.add(x, C.shift(16n, LV.ev(t))), Nat.add(C.shift(16n, LV.ev(t)), x), NA.add_comm(x, C.shift(16n, LV.ev(t)))) : {Nat.add(Nat.add(Nat.add(L.comp1(x), C.shift(16n, LV.ev(L.comp(t)))), _), one) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
118      %Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), C.shift(16n, LV.ev(L.comp(t)))), Nat.add(C.shift(16n, LV.ev(t)), x)), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x))), NA.add_assoc(L.comp1(x), C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x))) : {Nat.add(_, one) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
119      %Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x))), one), Nat.add(L.comp1(x), Nat.add(Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x)), one)), NA.add_assoc(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x)), one)) : {_ == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
120      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x)), one), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(Nat.add(C.shift(16n, LV.ev(t)), x), one)), NA.add_assoc(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), x), one)) : {Nat.add(L.comp1(x), _) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
121      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, LV.ev(t)), x), one), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(x, one)), NA.add_assoc(C.shift(16n, LV.ev(t)), x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), _)) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
122      %Equal.sym(Nat, Nat.add(x, one), Nat.add(one, x), NA.add_comm(x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), _))) == C.shift(16n, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one)) : Nat}
123      %Equal.sym(Nat, Nat.add(Nat.add(LV.ev(L.comp(t)), LV.ev(t)), one), Nat.add(LV.ev(L.comp(t)), Nat.add(LV.ev(t), one)), NA.add_assoc(LV.ev(L.comp(t)), LV.ev(t), one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == C.shift(16n, _) : Nat}
124      %Equal.sym(Nat, C.shift(16n, Nat.add(LV.ev(L.comp(t)), Nat.add(LV.ev(t), one))), Nat.add(C.shift(16n, LV.ev(L.comp(t))), C.shift(16n, Nat.add(LV.ev(t), one))), WW.shift_add(16n, LV.ev(L.comp(t)), Nat.add(LV.ev(t), one))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == _ : Nat}
125      %Equal.sym(Nat, C.shift(16n, Nat.add(LV.ev(t), one)), Nat.add(C.shift(16n, LV.ev(t)), C.shift(16n, one)), WW.shift_add(16n, LV.ev(t), one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), _) : Nat}
126      %Equal.sym(Nat, C.shift(16n, one), Nat.add(Nat.add(L.comp1(x), x), one), Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), x), one), C.shift(16n, one), comp1_o(one, h1, x, hx))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), _)) : Nat}
127      %Equal.sym(Nat, Nat.add(Nat.add(L.comp1(x), x), one), Nat.add(L.comp1(x), Nat.add(x, one)), NA.add_assoc(L.comp1(x), x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), _)) : Nat}
128      %Equal.sym(Nat, Nat.add(x, one), Nat.add(one, x), NA.add_comm(x, one)) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(L.comp1(x), _))) : Nat}
129      %Equal.sym(Nat, Nat.add(C.shift(16n, LV.ev(t)), Nat.add(L.comp1(x), Nat.add(one, x))), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x))), NA.add_swap(C.shift(16n, LV.ev(t)), L.comp1(x), Nat.add(one, x))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == Nat.add(C.shift(16n, LV.ev(L.comp(t))), _) : Nat}
130      %Equal.sym(Nat, Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))), Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))), NA.add_swap(C.shift(16n, LV.ev(L.comp(t))), L.comp1(x), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) : {Nat.add(L.comp1(x), Nat.add(C.shift(16n, LV.ev(L.comp(t))), Nat.add(C.shift(16n, LV.ev(t)), Nat.add(one, x)))) == _ : Nat}
131      {==}

Uses (21)

Used by (1)