~/jendhub

def ad.ae.w64

bend-osdev-aead@0.1.0.0 · aegis128.bend:202

import bend-osdev-aead@0.1.0.0/aegis128.bend as Aegis128
import Base
import bend-osdev-word64@0.1.0.0/word64.bend as W

202# n as a 64-bit word, counted up (W64.from_nat divides by 2^32, a literal
203# the checker would expand when a proof meets it)
204def ad.ae.w64(n: Nat, acc: W.W64) -> W.W64:
205  match n:
206    case 0n:
207      acc
208    case 1n+p:
209      ad.ae.w64(p, W.W64.add(acc, W.W64.one()))

Uses (4)

Used by (1)