def po_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/pow.bend:74

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

74def po_zero(+x: List<&2, U32>, +acc: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}) -> {F.pow_ones(x, 0n, acc) == acc : List<&2, U32>}:
75  match x:
76    case Nil{}:
77      {==}
78    case Con{h, t}:
79      {==}