StorageWitness.swap_choose: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_witness.bend as StorageWitness
Lines 94-109 of stelliferous@0.0.2.0/proofs/storage_witness.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&start_line=94&end_line=109

import Base

# Base passes the branch z (i < n/2) computed by its caller; any z is covered
# here, and each child receives the comparison against its own half.
def swap_choose(-Element: Data,-depth: Nat,-left: Array<Element>,-right: Array<Element>,
  +capacity: U32,+index: U32,-value: Element,choose_left: Bool,
  left_balanced: Witness(Element,depth,left),right_balanced: Witness(Element,depth,right),
  left_result: Swapped<Element,depth,Array.swap.go(Element,left,U32.shr(capacity),index,value,U32.is_lt(index,U32.shr(U32.shr(capacity))))>,
  right_result: Swapped<Element,depth,Array.swap.go(Element,right,U32.shr(capacity),U32.sub(index,U32.shr(capacity)),value,
    U32.is_lt(U32.sub(index,U32.shr(capacity)),U32.shr(U32.shr(capacity))))>) ->
  Swapped<Element,1n+depth,Array.swap.go(Element,ANode{left,right},capacity,index,value,choose_left)>:
  match choose_left:
    case True{}:
      swap_left(Element,depth,right,Array.swap.go(Element,left,U32.shr(capacity),index,value,U32.is_lt(index,U32.shr(U32.shr(capacity)))),
        left_result,right_balanced)
    case False{}:
      swap_right(Element,depth,left,Array.swap.go(Element,right,U32.shr(capacity),U32.sub(index,U32.shr(capacity)),value,
        U32.is_lt(U32.sub(index,U32.shr(capacity)),U32.shr(U32.shr(capacity)))),left_balanced,right_result)

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.swap.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Swapped
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=Witness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=swap_left
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=swap_right