def FG2

lawful-bytes@0.1.1.0 · proof_fast_find2.bend:31

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

31def FG2(n: Nat, z: Bool, +wi: U32, +m: U32, +r1: U32, +r2: U32, +t: P.Tree<U32>) -> U32:
32  match n z:
33    case 0n _:
34      4294967295
35    case 1n+k True{}:
36      +m2 = (FA.zb((C.WD(t, (wi + 1 : U32)) .^. r1 : U32)) .|. FA.zb((C.WD(t, (wi + 1 : U32)) .^. r2 : U32)) : U32)
37      FG2(k, U32.is_zero(m2), (wi + 1 : U32), m2, r1, r2, t)
38    case 1n+k False{}:
39      ((wi << 2n : U32) + FA.bidx(m) : U32)