def inside_indexed
stelliferous@0.0.2.0 · proofs/traversal_map_readback.bend:82
import stelliferous@0.0.2.0/proofs/traversal_map_readback.bend as TraversalMapReadback
import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape
import stelliferous@0.0.2.0/proofs/storage_readback.bend as StorageReadback
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
import stelliferous@0.0.2.0/proofs/nat_interval.bend as Interval
import stelliferous@0.0.2.0/proofs/nat_division.bend as Division
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding
82def inside_indexed(~Element: Data,~Context: Data,~operation: Context -> U32 -> Element -> Element,count: Nat,+position: Nat,index: Nat,+context: Context,+input: Tree.Tree<Element>,+depth: Nat,+capacity: U32,
83 +capacity_equal: {Tree.capacity(Element,input) == capacity : U32},+balanced: Shape.Balanced(Element,depth,input),+limit: {Nat.is_le(depth,31n) == True{} : Bool},
84 +capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},+room: {Nat.is_le(Nat.add(position,count),U32.to_nat(capacity)) == True{} : Bool},
85 +selected: {Nat.is_lt(index,count) == True{} : Bool}) ->
86 {Tree.read(Element,run_indexed(~Element,~Context,~operation,count,U32.from_nat(position),context,input),U32.from_nat(Nat.add(position,index))) ==
87 operation(context,U32.from_nat(Nat.add(position,index)),Tree.read(Element,input,U32.from_nat(Nat.add(position,index)))) : Element}:
88 match count index:
89 case 0n +index:
90 Empty.absurd({Tree.read(Element,input,U32.from_nat(Nat.add(position,index))) == operation(context,U32.from_nat(Nat.add(position,index)),Tree.read(Element,input,U32.from_nat(Nat.add(position,index)))) : Element},
91 WordEncoding.false_true(Equal.trans(Bool,False{},Nat.is_lt(index,0n),True{},Equal.sym(Bool,Nat.is_lt(index,0n),False{},Division.lt_zero(index)),selected)))
92 case 1n+ +rest 0n:
93 +value = operation(context,U32.from_nat(position),Tree.read(Element,input,U32.from_nat(position)))
94 +written = Tree.write(Element,input,U32.from_nat(position),value)
95 +position_inside = Order.room_index(position,rest,U32.to_nat(capacity),room)
96 %Equal.sym(Nat,Nat.add(position,0n),position,Addition.zero_right(position)) :
97 {Tree.read(Element,run_indexed(~Element,~Context,~operation,1n+rest,U32.from_nat(position),context,input),U32.from_nat(_)) == operation(context,U32.from_nat(_),Tree.read(Element,input,U32.from_nat(_))) : Element}
98 %Equal.sym(U32,(U32.from_nat(position) + 1 : U32),U32.from_nat(1n+position),Bounds.add_one(U32.from_nat(position))) :
99 {Tree.read(Element,run_indexed(~Element,~Context,~operation,rest,_,context,written),U32.from_nat(position)) == value : Element}
100 Equal.trans(Element,Tree.read(Element,run_indexed(~Element,~Context,~operation,rest,U32.from_nat(1n+position),context,written),U32.from_nat(position)),Tree.read(Element,written,U32.from_nat(position)),value,
101 outside_indexed(~Element,~Context,~operation,rest,1n+position,U32.from_nat(position),context,written,depth,capacity,
102 Equal.trans(U32,Tree.capacity(Element,written),Tree.capacity(Element,input),capacity,StorageReadback.write_capacity(~Element,input,U32.from_nat(position),value),capacity_equal),
103 Shape.write(Element,depth,input,U32.from_nat(position),value,balanced),limit,capacity_ok,Order.advance_room(position,rest,U32.to_nat(capacity),room),address_inside(position,capacity,capacity_ok,position_inside),
104 Interval.Before{
105 %Equal.sym(Nat,U32.to_nat(U32.from_nat(position)),position,Bounds.roundtrip(position,capacity,capacity_ok,Bounds.strict_le(position,U32.to_nat(capacity),position_inside))) : {Nat.is_lt(_,1n+position) == True{} : Bool}
106 Order.lt_succ(position,position,Order.reflexive(position))}),
107 StorageReadback.read_written(~Element,input,U32.from_nat(position),value))
108 case 1n+ +rest 1n+ +index:
109 +value = operation(context,U32.from_nat(position),Tree.read(Element,input,U32.from_nat(position)))
110 +written = Tree.write(Element,input,U32.from_nat(position),value)
111 +query_position = Nat.add(1n+position,index)
112 +query = U32.from_nat(query_position)
113 +position_inside = Order.room_index(position,rest,U32.to_nat(capacity),room)
114 +query_inside = Bounds.nat_trans(query_position,Nat.add(1n+position,rest),U32.to_nat(capacity),Order.offset_lt(1n+position,index,rest,selected),Order.advance_room(position,rest,U32.to_nat(capacity),room))
115 +different = {
116 %Equal.sym(Bool,U32.is_eq(U32.from_nat(position),query),Nat.is_eq(U32.to_nat(U32.from_nat(position)),U32.to_nat(query)),Comparison.eq(U32.from_nat(position),query)) : {_ == False{} : Bool}
117 %Equal.sym(Nat,U32.to_nat(U32.from_nat(position)),position,Bounds.roundtrip(position,capacity,capacity_ok,Bounds.strict_le(position,U32.to_nat(capacity),position_inside))) : {Nat.is_eq(_,U32.to_nat(query)) == False{} : Bool}
118 %Equal.sym(Nat,U32.to_nat(query),query_position,Bounds.roundtrip(query_position,capacity,capacity_ok,Bounds.strict_le(query_position,U32.to_nat(capacity),query_inside))) : {Nat.is_eq(position,_) == False{} : Bool}
119 Order.less_not_equal(position,query_position,Bounds.nat_trans(position,1n+position,query_position,Order.lt_succ(position,position,Order.reflexive(position)),Order.le_add(1n+position,index))) : {U32.is_eq(U32.from_nat(position),query) == False{} : Bool}}
120 %Equal.sym(Nat,Nat.add(position,1n+index),query_position,Addition.successor_right(position,index)) :
121 {Tree.read(Element,run_indexed(~Element,~Context,~operation,1n+rest,U32.from_nat(position),context,input),U32.from_nat(_)) == operation(context,U32.from_nat(_),Tree.read(Element,input,U32.from_nat(_))) : Element}
122 %Equal.sym(U32,(U32.from_nat(position) + 1 : U32),U32.from_nat(1n+position),Bounds.add_one(U32.from_nat(position))) :
123 {Tree.read(Element,run_indexed(~Element,~Context,~operation,rest,_,context,written),query) == operation(context,query,Tree.read(Element,input,query)) : Element}
124 Equal.trans(Element,Tree.read(Element,run_indexed(~Element,~Context,~operation,rest,U32.from_nat(1n+position),context,written),query),operation(context,query,Tree.read(Element,written,query)),operation(context,query,Tree.read(Element,input,query)),
125 inside_indexed(~Element,~Context,~operation,rest,1n+position,index,context,written,depth,capacity,
126 Equal.trans(U32,Tree.capacity(Element,written),Tree.capacity(Element,input),capacity,StorageReadback.write_capacity(~Element,input,U32.from_nat(position),value),capacity_equal),
127 Shape.write(Element,depth,input,U32.from_nat(position),value,balanced),limit,capacity_ok,Order.advance_room(position,rest,U32.to_nat(capacity),room),selected),
128 Equal.cong(Element,Element,element => operation(context,query,element),Tree.read(Element,written,query),Tree.read(Element,input,query),
129 unchanged_full(~Element,depth,input,U32.from_nat(position),query,value,capacity,capacity_equal,balanced,limit,address_inside(position,capacity,capacity_ok,position_inside),address_inside(query_position,capacity,capacity_ok,query_inside),different)))