Negate.comp_v: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend as Negate
Lines 104-131 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend&start_line=104&end_line=131

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

# comp(x) + x + 1 = 2^(16 n) for n limbs below 2^16
def 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}:
  match n xs:
    case 0n Nil{}:
      {==}
    case 0n x <> t:
      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))
    case 1n+k Nil{}:
      Empty.absurd({Nat.add(Nat.add(LV.ev(L.comp([])), LV.ev([])), one) == LV.pos(1n+k, one) : Nat}, Lg.false_true(h))
    case 1n+ +k +x <> +t:
      +hx = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), h)
      +ht = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, k, t), h)
      %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}
      %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}
      %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}
      %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}
      %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}
      %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}
      %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}
      %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}
      %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}
      %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}
      %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}
      %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}
      %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}
      %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}
      %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}
      {==}

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=ev
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend&name=comp1_o
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_swap
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=shift_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=limbs16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=comp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=comp1