def swap_choose

stelliferous@0.0.2.0 · proofs/storage_witness.bend:94

import Base

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