1 # Pointwise semantics of the actual ordered in-place map traversal. A bounded 2 # cursor visits each address once, so later stores preserve earlier results. 3 import Base 4 import ../traversal_array.bend as Traversal 5 import ../traversal_loop.bend as Loop 6 import ./traversal_array_refinement.bend as ArrayLaws 7 import ./storage_tree_model.bend as Tree 8 import ./storage_shape.bend as Shape 9 import ./storage_readback.bend as StorageReadback 10 import ./nat_to_u32_bounds.bend as Bounds 11 import ./nat_order.bend as Order 12 import ./natural_addition.bend as Addition 13 import ./u32_comparison.bend as Comparison 14 import ./nat_interval.bend as Interval 15 import ./nat_division.bend as Division 16 import ./word_encoding.bend as WordEncoding 17 18 def output(~Element: Data,~Context: Data,state: Traversal.State<&2,&2,Unit,Tree.Tree,Context>) -> Tree.Tree: 19 Traversal.State{reader,output,position,context} = state 20 output 21 22 def run_indexed(~Element: Data,~Context: Data,~operation: Context -> U32 -> Element -> Element,count: Nat,position: U32,context: Context,input: Tree.Tree) -> Tree.Tree: 23 output(~Element,~Context,Loop.run(~Traversal.State<&2,&2,Unit,Tree.Tree,Context>,~ArrayLaws.model_map_step(~Element,~Context,~operation), 24 count,Traversal.State{Unit{},input,position,context})) 25 26 def capacity_indexed(~Element: Data,~Context: Data,~operation: Context -> U32 -> Element -> Element,count: Nat,+position: U32,+context: Context,+input: Tree.Tree) -> 27 {Tree.capacity(Element,run_indexed(~Element,~Context,~operation,count,position,context,input)) == Tree.capacity(Element,input) : U32}: 28 match count: 29 case 0n: {==} 30 case 1n+rest: 31 +value = operation(context,position,Tree.read(Element,input,position)) 32 +written = Tree.write(Element,input,position,value) 33 Equal.trans(U32,Tree.capacity(Element,run_indexed(~Element,~Context,~operation,rest,(position + 1 : U32),context,written)),Tree.capacity(Element,written),Tree.capacity(Element,input), 34 capacity_indexed(~Element,~Context,~operation,rest,(position + 1 : U32),context,written),StorageReadback.write_capacity(~Element,input,position,value)) 35 36 def balanced_indexed(~Element: Data,~Context: Data,~operation: Context -> U32 -> Element -> Element,count: Nat,+position: U32,+context: Context,+input: Tree.Tree,+depth: Nat, 37 evidence: Shape.Balanced(Element,depth,input)) -> Shape.Balanced(Element,depth,run_indexed(~Element,~Context,~operation,count,position,context,input)): 38 match count: 39 case 0n: evidence 40 case 1n+rest: 41 +value = operation(context,position,Tree.read(Element,input,position)) 42 balanced_indexed(~Element,~Context,~operation,rest,(position + 1 : U32),context,Tree.write(Element,input,position,value),depth,Shape.write(Element,depth,input,position,value,evidence)) 43 44 def address_inside(+position: Nat,+capacity: U32,+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool}, 45 +inside: {Nat.is_lt(position,U32.to_nat(capacity)) == True{} : Bool}) -> {U32.is_lt(U32.from_nat(position),capacity) == True{} : Bool}: 46 Bounds.native_bound(position,capacity,Bounds.roundtrip(position,capacity,capacity_ok,Bounds.strict_le(position,U32.to_nat(capacity),inside)),inside) 47 48 def unchanged_full(~Element: Data,+depth: Nat,+input: Tree.Tree,+position: U32,+query: U32,+value: Element,+capacity: U32, 49 +capacity_equal: {Tree.capacity(Element,input) == capacity : U32},balanced: Shape.Balanced(Element,depth,input),limit: {Nat.is_le(depth,31n) == True{} : Bool}, 50 position_inside: {U32.is_lt(position,capacity) == True{} : Bool},query_inside: {U32.is_lt(query,capacity) == True{} : Bool},different: {U32.is_eq(position,query) == False{} : Bool}) -> 51 {Tree.read(Element,Tree.write(Element,input,position,value),query) == Tree.read(Element,input,query) : Element}: 52 StorageReadback.read_preserved_full(~Element,depth,input,position,query,value,balanced,limit, 53 %Equal.sym(U32,Tree.capacity(Element,input),capacity,capacity_equal) : {U32.is_lt(position,_) == True{} : Bool} position_inside, 54 %Equal.sym(U32,Tree.capacity(Element,input),capacity,capacity_equal) : {U32.is_lt(query,_) == True{} : Bool} query_inside,different) 55 56 def outside_indexed(~Element: Data,~Context: Data,~operation: Context -> U32 -> Element -> Element,count: Nat,+position: Nat,+query: U32,+context: Context,+input: Tree.Tree,+depth: Nat,+capacity: U32, 57 +capacity_equal: {Tree.capacity(Element,input) == capacity : U32},+balanced: Shape.Balanced(Element,depth,input),+limit: {Nat.is_le(depth,31n) == True{} : Bool}, 58 +capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},+room: {Nat.is_le(Nat.add(position,count),U32.to_nat(capacity)) == True{} : Bool}, 59 +query_inside: {U32.is_lt(query,capacity) == True{} : Bool},+separate: Interval.Outside) -> 60 {Tree.read(Element,run_indexed(~Element,~Context,~operation,count,U32.from_nat(position),context,input),query) == Tree.read(Element,input,query) : Element}: 61 match count: 62 case 0n: {==} 63 case 1n+ +rest: 64 +value = operation(context,U32.from_nat(position),Tree.read(Element,input,U32.from_nat(position))) 65 +written = Tree.write(Element,input,U32.from_nat(position),value) 66 +position_inside = Order.room_index(position,rest,U32.to_nat(capacity),room) 67 +different = { 68 %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} 69 %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))) : 70 {Nat.is_eq(_,U32.to_nat(query)) == False{} : Bool} 71 %Order.equal_symmetric(U32.to_nat(query),position) : {_ == False{} : Bool} 72 Interval.outside_head(position,rest,U32.to_nat(query),separate) : {U32.is_eq(U32.from_nat(position),query) == False{} : Bool}} 73 %Equal.sym(U32,(U32.from_nat(position) + 1 : U32),U32.from_nat(1n+position),Bounds.add_one(U32.from_nat(position))) : 74 {Tree.read(Element,run_indexed(~Element,~Context,~operation,rest,_,context,written),query) == Tree.read(Element,input,query) : Element} 75 Equal.trans(Element,Tree.read(Element,run_indexed(~Element,~Context,~operation,rest,U32.from_nat(1n+position),context,written),query),Tree.read(Element,written,query),Tree.read(Element,input,query), 76 outside_indexed(~Element,~Context,~operation,rest,1n+position,query,context,written,depth,capacity, 77 Equal.trans(U32,Tree.capacity(Element,written),Tree.capacity(Element,input),capacity,StorageReadback.write_capacity(~Element,input,U32.from_nat(position),value),capacity_equal), 78 Shape.write(Element,depth,input,U32.from_nat(position),value,balanced),limit,capacity_ok,Order.advance_room(position,rest,U32.to_nat(capacity),room),query_inside, 79 Interval.outside_tail(position,rest,U32.to_nat(query),separate)), 80 unchanged_full(~Element,depth,input,U32.from_nat(position),query,value,capacity,capacity_equal,balanced,limit,address_inside(position,capacity,capacity_ok,position_inside),query_inside,different)) 81 82 def inside_indexed(~Element: Data,~Context: Data,~operation: Context -> U32 -> Element -> Element,count: Nat,+position: Nat,index: Nat,+context: Context,+input: Tree.Tree,+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))) 130 131 # Unary maps use the same indexed induction with an unused position. 132 def run(~Element: Data,~Context: Data,~operation: Context -> Element -> Element,count: Nat,position: U32,context: Context,input: Tree.Tree) -> Tree.Tree: 133 run_indexed(~Element,~Context,~ArrayLaws.unindexed(~Element,~Context,~operation),count,position,context,input) 134 135 def capacity(~Element: Data,~Context: Data,~operation: Context -> Element -> Element,count: Nat,+position: U32,+context: Context,+input: Tree.Tree) -> 136 {Tree.capacity(Element,run(~Element,~Context,~operation,count,position,context,input)) == Tree.capacity(Element,input) : U32}: 137 capacity_indexed(~Element,~Context,~ArrayLaws.unindexed(~Element,~Context,~operation),count,position,context,input) 138 139 def balanced(~Element: Data,~Context: Data,~operation: Context -> Element -> Element,count: Nat,+position: U32,+context: Context,+input: Tree.Tree,+depth: Nat, 140 evidence: Shape.Balanced(Element,depth,input)) -> Shape.Balanced(Element,depth,run(~Element,~Context,~operation,count,position,context,input)): 141 balanced_indexed(~Element,~Context,~ArrayLaws.unindexed(~Element,~Context,~operation),count,position,context,input,depth,evidence) 142 143 def inside(~Element: Data,~Context: Data,~operation: Context -> Element -> Element,count: Nat,+position: Nat,index: Nat,+context: Context,+input: Tree.Tree,+depth: Nat,+capacity: U32, 144 +capacity_equal: {Tree.capacity(Element,input) == capacity : U32},+balanced: Shape.Balanced(Element,depth,input),+limit: {Nat.is_le(depth,30n) == True{} : Bool}, 145 +capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},+room: {Nat.is_le(Nat.add(position,count),U32.to_nat(capacity)) == True{} : Bool}, 146 +selected: {Nat.is_lt(index,count) == True{} : Bool}) -> 147 {Tree.read(Element,run(~Element,~Context,~operation,count,U32.from_nat(position),context,input),U32.from_nat(Nat.add(position,index))) == 148 operation(context,Tree.read(Element,input,U32.from_nat(Nat.add(position,index)))) : Element}: 149 inside_indexed(~Element,~Context,~ArrayLaws.unindexed(~Element,~Context,~operation),count,position,index,context,input,depth,capacity,capacity_equal,balanced,Order.successor(depth,30n,limit),capacity_ok,room,selected) 150 151 def unchanged(~Element: Data,+depth: Nat,+input: Tree.Tree,+position: U32,+query: U32,+value: Element,+capacity: U32, 152 +capacity_equal: {Tree.capacity(Element,input) == capacity : U32},balanced: Shape.Balanced(Element,depth,input),limit: {Nat.is_le(depth,30n) == True{} : Bool}, 153 position_inside: {U32.is_lt(position,capacity) == True{} : Bool},query_inside: {U32.is_lt(query,capacity) == True{} : Bool},different: {U32.is_eq(position,query) == False{} : Bool}) -> 154 {Tree.read(Element,Tree.write(Element,input,position,value),query) == Tree.read(Element,input,query) : Element}: 155 unchanged_full(~Element,depth,input,position,query,value,capacity,capacity_equal,balanced,Order.successor(depth,30n,limit),position_inside,query_inside,different)