ProofFastAppend.AWT: def of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppend
Lines 395-403 of lawful-bytes@0.1.1.0/proof_fast_append.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_fast_append.bend&start_line=395&end_line=403

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

# The tree append.words leaves: p is the word read next (hi), lo the word
# before it, td the dst block, di the dst word written, sh the shift in bits.
def AWT(n: Nat, +ts: P.Tree<U32>, +p: U32, +lo: U32, +td: P.Tree<U32>, +si: U32, +di: U32, +sh: Nat) -> P.Tree<U32>:
  match n:
    case 0n:
      td
    case 1n+k:
      +hi = C.WD(ts, p)
      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)

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shrn
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=set_tree
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=WD