def ramp

bend-osdev-bytes@0.1.1.0 · check.bend:19

import Base

19# n bytes 0, 1, 2, ... (mod 256), built tail-recursively
20def ramp(n: Nat, acc: List<&2, U32>) -> List<&2, U32>:
21  match n:
22    case 0n:
23      acc
24    case 1n+(+p):
25      ramp(p, Con{U32.and(U32.from_nat(p), 255), acc})