def AWT

lawful-bytes@0.1.1.0 · proof_fast_append.bend:395

import Base
import lawful-bytes@0.1.1.0/proof_core.bend as C
import lawful-arrays@0.1.0.0/proof_tree.bend as P
import lawful-arrays@0.1.0.0/proof_index.bend as I

395# The tree append.words leaves: p is the word read next (hi), lo the word
396# before it, td the dst block, di the dst word written, sh the shift in bits.
397def AWT(n: Nat, +ts: P.Tree<U32>, +p: U32, +lo: U32, +td: P.Tree<U32>, +si: U32, +di: U32, +sh: Nat) -> P.Tree<U32>:
398  match n:
399    case 0n:
400      td
401    case 1n+k:
402      +hi = C.WD(ts, p)
403      AWT(k, ts, (si + 2 : U32), hi, I.set_tree(U32, td, di, U32.or(U32.shrn(lo, sh), U32.shln(hi, Nat.sub(32n, sh)))), (si + 1 : U32), (di + 1 : U32), sh)