def nonzero_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/listops.bend:53

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/crypto/secp256k1/limbs.bend as LV

53def nonzero_v(xs: List<&2, Nat>, +acc: Nat) -> {Nat.is_eq(L.nonzero(xs, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(LV.ev(xs), 0n)) : Bool}:
54  match xs:
55    case Nil{}:
56      Equal.sym(Bool, Bool.and(Nat.is_eq(acc, 0n), True{}), Nat.is_eq(acc, 0n), and_true_r(Nat.is_eq(acc, 0n)))
57    case +x <> +t:
58      %Equal.sym(Bool, Nat.is_eq(L.nonzero(t, Nat.add(acc, x)), 0n), Bool.and(Nat.is_eq(Nat.add(acc, x), 0n), Nat.is_eq(LV.ev(t), 0n)), nonzero_v(t, Nat.add(acc, x))) : {_ == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n)) : Bool}
59      %Equal.sym(Bool, Nat.is_eq(Nat.add(acc, x), 0n), Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), is_eq_add0(acc, x)) : {Bool.and(_, Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n)) : Bool}
60      %Equal.sym(Bool, Nat.is_eq(Nat.add(x, C.shift(16n, LV.ev(t))), 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(C.shift(16n, LV.ev(t)), 0n)), is_eq_add0(x, C.shift(16n, LV.ev(t)))) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), _) : Bool}
61      %Equal.sym(Bool, Nat.is_eq(C.shift(16n, LV.ev(t)), 0n), Nat.is_eq(LV.ev(t), 0n), sh_eq0(LV.ev(t))) : {Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)) == Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), _)) : Bool}
62      %Equal.sym(Bool, Bool.and(Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n)), Nat.is_eq(LV.ev(t), 0n)), Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))), and_assoc(Nat.is_eq(acc, 0n), Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))) : {_ == Bool.and(Nat.is_eq(acc, 0n), Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(LV.ev(t), 0n))) : Bool}
63      {==}