def adc_ok

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/adc.bend:22

import Base

22def adc_ok(xs: List<&2, U32>, ys: List<&2, U32>, zs: List<&2, U32>, +c: Nat, +co: Nat) -> Bool:
23  match xs ys zs:
24    case Nil{} Nil{} Nil{}:
25      Nat.is_eq(c, co)
26    case Con{x, xt} Con{y, yt} Con{z, zt}:
27      +s = Nat.add(Nat.add(U32.to_nat(x), U32.to_nat(y)), c)
28      Bool.and(Nat.is_eq(Nat.mod(s, 256n), U32.to_nat(z)), adc_ok(xt, yt, zt, Nat.div(s, 256n), co))
29    case _ _ _:
30      False{}