def which_c

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/final.bend:317

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend as Li
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/step.bend as ST

317def which_c(+one: Nat, +h1: {one == 1n : Nat}, +h: List<&2, U32>, +hh: {ST.inv(h) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(qq(h), 0n) == c : Bool}) -> Or({Li.freeze(h) == Li.take(16n, h) : List<&2, U32>}, {Li.freeze(h) == Li.take(16n, gg(h)) : List<&2, U32>}):
318  match c:
319    case True{}: Inl{which0(one, h1, h, hh, hc)}
320    case False{}: Inr{which1(one, h1, h, hh, hc)}