def comp1_v

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

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/src/crypto/secp256k1/limbs.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV

84# comp1(x) + x + 1 = 2^16 for x < 2^16
85def comp1_v(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.add(Nat.add(L.comp1(x), x), 1n) == C.shift(16n, one) : Nat}:
86  +lo = Nat.mod(x, 256n)
87  +hi = Nat.div(x, 256n)
88  +hl = N.lt_succ_le(lo, 255n, NR.dm_lt(255n, x))
89  +hh = N.lt_succ_le(hi, 255n, hi_byte_lt(one, h1, x, hx))
90  %Equal.sym(Nat, x, Nat.add(Nat.mul(Nat.div(x, 256n), 256n), Nat.mod(x, 256n)), NR.dm_eq(255n, x)) : {Nat.add(Nat.add(Nat.add(Nat.sub(255n, Nat.mod(x, 256n)), Nat.mul(Nat.sub(255n, Nat.div(x, 256n)), 256n)), _), 1n) == C.shift(16n, one) : Nat}
91  %Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(255n, Nat.mod(x, 256n)), Nat.mul(Nat.sub(255n, Nat.div(x, 256n)), 256n)), Nat.add(Nat.mul(Nat.div(x, 256n), 256n), Nat.mod(x, 256n))), Nat.add(Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), 256n)), combine(Nat.sub(255n, Nat.mod(x, 256n)), Nat.sub(255n, Nat.div(x, 256n)), Nat.div(x, 256n), Nat.mod(x, 256n), 256n)) : {Nat.add(_, 1n) == C.shift(16n, one) : Nat}
92  %Equal.sym(Nat, 256n, C.shift(8n, one), Equal.sym(Nat, C.shift(8n, one), 256n, LV.b8(one, h1))) : {Nat.add(Nat.add(Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), _)), 1n) == C.shift(16n, one) : Nat}
93  %Equal.sym(Nat, Nat.add(Nat.mod(x, 256n), Nat.sub(255n, Nat.mod(x, 256n))), 255n, N.sub_add(255n, Nat.mod(x, 256n), hl)) : {Nat.add(Nat.add(_, Nat.mul(Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
94  %Equal.sym(Nat, Nat.add(Nat.div(x, 256n), Nat.sub(255n, Nat.div(x, 256n))), 255n, N.sub_add(255n, Nat.div(x, 256n), hh)) : {Nat.add(Nat.add(255n, Nat.mul(_, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
95  %Equal.sym(Nat, 255n, Nat.sub(C.shift(8n, one), 1n), Equal.sym(Nat, Nat.sub(C.shift(8n, one), 1n), 255n, e255(one, h1))) : {Nat.add(Nat.add(_, Nat.mul(255n, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
96  %Equal.sym(Nat, 255n, Nat.sub(C.shift(8n, one), 1n), Equal.sym(Nat, Nat.sub(C.shift(8n, one), 1n), 255n, e255(one, h1))) : {Nat.add(Nat.add(Nat.sub(C.shift(8n, one), 1n), Nat.mul(_, C.shift(8n, one))), 1n) == C.shift(16n, one) : Nat}
97  %Equal.sym(Nat, Nat.add(Nat.add(Nat.sub(C.shift(8n, one), 1n), Nat.mul(Nat.sub(C.shift(8n, one), 1n), C.shift(8n, one))), 1n), Nat.mul(C.shift(8n, one), C.shift(8n, one)), digit_max(C.shift(8n, one), bb_pos(one, h1))) : {_ == C.shift(16n, one) : Nat}
98  bb_sq(one, h1)