def pub_guard

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/top.bend:149

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE

149def pub_guard(+one: Nat, +p: Nat, +d: Nat, +h: List<&2, U32>, +x: List<&2, U32>, +e: {x == SE.public_body(one, p, d, h) : List<&2, U32>}) -> {x == SE.public_of(one, p, d, h) : List<&2, U32>}:
150  match d:
151    case 0n:
152      e
153    case 1n+ +q:
154      e