def ok16

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/lits.bend:28

import Base

28def ok16(+w: Nat, n: Nat, xs: List<&2, Nat>) -> Bool:
29  match n xs:
30    case 0n Nil{}: True{}
31    case 0n x <> t: False{}
32    case 1n+k Nil{}: False{}
33    case 1n+k x <> t: Bool.and(Nat.is_lt(x, Nat.add(Nat.add(Nat.add(Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))), Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w)))), Nat.add(Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))), Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))))), Nat.add(Nat.add(Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))), Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w)))), Nat.add(Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))), Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))))))), ok16(w, k, t))