def sq_four

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/fieldpow.bend:258

import Base
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/src/crypto/secp256k1/field.bend as F
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/semiring.bend as SR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend as BV

258# hv of the bits of p + 1 is 4 hv(sqrt bits)
259def sq_four(+one: Nat) -> {BV.hv(L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), one, 0n) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}:
260  %Equal.sym(List<&2, Nat>, L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), List.append(&2, Nat, F.sqrt_bits(), [0n, 0n]), sq_split()) : {BV.hv(_, one, 0n) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
261  %Equal.sym(Nat, BV.hv(List.append(&2, Nat, F.sqrt_bits(), [0n, 0n]), one, 0n), BV.hv([0n, 0n], one, BV.hv(F.sqrt_bits(), one, 0n)), BV.hv_app(one, F.sqrt_bits(), 0n, [0n, 0n])) : {_ == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
262  %Equal.sym(Nat, Nat.mul(0n, one), 0n, SR.zero_mul(one)) : {Nat.add(_, Nat.double(Nat.add(Nat.mul(0n, one), Nat.double(BV.hv(F.sqrt_bits(), one, 0n))))) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
263  %Equal.sym(Nat, Nat.mul(0n, one), 0n, SR.zero_mul(one)) : {Nat.add(0n, Nat.double(Nat.add(_, Nat.double(BV.hv(F.sqrt_bits(), one, 0n))))) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
264  %Equal.sym(Nat, Nat.double(BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), NA.double_self(BV.hv(F.sqrt_bits(), one, 0n))) : {Nat.add(0n, Nat.double(Nat.add(0n, _))) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
265  %Equal.sym(Nat, Nat.add(0n, Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), SR.zero_add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) : {Nat.add(0n, Nat.double(_)) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
266  %Equal.sym(Nat, Nat.double(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), NA.double_self(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) : {Nat.add(0n, _) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
267  %Equal.sym(Nat, Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))), NA.add_assoc(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) : {Nat.add(0n, _) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
268  %Equal.sym(Nat, Nat.add(0n, Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))))), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))), SR.zero_add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))))) : {_ == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
269  %Equal.sym(Nat, Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))), NA.add_assoc(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) : {Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) == _ : Nat}
270  {==}