1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/list.bend as LL 4 import ../../lib/nat.bend as N 5 import ../../lib/array.bend as AR 6 import ../../../spec/containers/dynamic_array.bend as S 7 import ../../../src/containers/dynamic_array.bend as DA 8 import ../../../src/containers/types/dynamic_array.bend as E 9 import ./state.bend as ST 10 import ./steps.bend as SP 11 import ./trace.bend as TR 12 import ./closed.bend as CL 13 import ./owned_instances.bend as OWN 14 import ./owned_swap.bend as OS 15 import ../../../spec/lib/common.bend as SC 16 import ../../../spec/lib/sequence.bend as V 17 import ../../lib/sequence.bend as VL 18 19 # Dynamic array: public proof entry point. 20 # abstraction ST.abs (Base.Array slots -> item sequence, via AR.freeze) 21 # invariant ST.Inv (the array realizes a shadow satisfying ST.good) 22 # operations SP.step_ok (every operation, errors included) 23 # traces trace_new / trace_with_limit (arbitrary finite op lists) 24 # The element type T is an arbitrary Data type (parametric; no template). 25 26 def view(-T: Data, r: DA.DynArray<&2, T> & List<&2, E.Obs>) -> S.Model & List<&2, E.Obs>: 27 match r: 28 case Tuple{da, os}: 29 (ST.abs(T, da), os) 30 31 def view1(-T: Data, r: DA.DynArray<&2, T> & E.Obs) -> S.Model & E.Obs: 32 match r: 33 case Tuple{da, o}: 34 (ST.abs(T, da), o) 35 36 # ---- initialization ---- 37 38 def new_inv(-T: Data) -> ST.Inv(T, DA.new(T)): 39 (TR.initial(T), ({==}, TR.new_good(T))) 40 41 def new_abs(-T: Data) -> {ST.abs(T, DA.new(T)) == S.new(T) : S.Model}: 42 {==} 43 44 def limit_good(-T: Data, +k: Nat) -> {ST.good(T, TR.limited(T, k)) == True{} : Bool}: 45 ST.good_intro(T, DA.clamp_limit(k, Nat.is_lt(k, 31n)), 0n, 0n, AR.TLeaf{None{}}, Pair.fst({Nat.is_le(DA.clamp_limit(k, Nat.is_lt(k, 31n)), 31n) == True{} : Bool}, {DA.clamp_limit(k, Nat.is_lt(k, 31n)) == Nat.min(k, 31n) : Nat}, TR.clamp_case(k, Nat.is_lt(k, 31n), {==})), N.zero_le(DA.clamp_limit(k, Nat.is_lt(k, 31n))), {==}, {==}) 46 47 def with_limit_inv(-T: Data, +k: Nat) -> ST.Inv(T, DA.with_limit(T, k)): 48 (TR.limited(T, k), ({==}, limit_good(T, k))) 49 50 def with_limit_abs(-T: Data, +k: Nat) -> {ST.abs(T, DA.with_limit(T, k)) == S.with_limit(T, k) : S.Model}: 51 %Equal.sym(Nat, DA.clamp_limit(k, Nat.is_lt(k, 31n)), Nat.min(k, 31n), Pair.snd({Nat.is_le(DA.clamp_limit(k, Nat.is_lt(k, 31n)), 31n) == True{} : Bool}, {DA.clamp_limit(k, Nat.is_lt(k, 31n)) == Nat.min(k, 31n) : Nat}, TR.clamp_case(k, Nat.is_lt(k, 31n), {==}))) : {S.M{_, 0n, Nil{}} == S.M{Nat.min(k, 31n), 0n, Nil{}} : S.Model} 52 {==} 53 54 # ---- every operation (errors included), on every reachable representation ---- 55 56 def step_refines(-T: Data, +sh: ST.Shadow, +op: E.Op, +g: {ST.good(T, sh) == True{} : Bool}) -> {view1(T, DA.step(T, ST.real(T, sh), op)) == S.step(T, ST.abs(T, ST.real(T, sh)), op) : S.Model & E.Obs}: 57 +sh2 = TR.so_sh(T, sh, op, SP.step_ok(T, sh, op, g)) 58 +o = TR.so_obs(T, sh, op, SP.step_ok(T, sh, op, g)) 59 %Equal.sym(DA.DynArray<&2, T> & E.Obs, DA.step(T, ST.real(T, sh), op), (ST.real(T, sh2), o), TR.so_step(T, sh, op, SP.step_ok(T, sh, op, g))) : {view1(T, _) == S.step(T, ST.abs(T, ST.real(T, sh)), op) : S.Model & E.Obs} 60 %Equal.sym(S.Model, ST.abs(T, ST.real(T, sh2)), ST.model(T, sh2), ST.abs_real(T, sh2)) : {(_, o) == S.step(T, ST.abs(T, ST.real(T, sh)), op) : S.Model & E.Obs} 61 %Equal.sym(S.Model, ST.abs(T, ST.real(T, sh)), ST.model(T, sh), ST.abs_real(T, sh)) : {(ST.model(T, sh2), o) == S.step(T, _, op) : S.Model & E.Obs} 62 TR.so_spec(T, sh, op, SP.step_ok(T, sh, op, g)) 63 64 def step_preserves(-T: Data, +sh: ST.Shadow, +op: E.Op, +g: {ST.good(T, sh) == True{} : Bool}) -> ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, E.Obs, DA.step(T, ST.real(T, sh), op))): 65 +sh2 = TR.so_sh(T, sh, op, SP.step_ok(T, sh, op, g)) 66 (sh2, (Equal.cong(DA.DynArray<&2, T> & E.Obs, DA.DynArray<&2, T>, r => Pair.fst(DA.DynArray<&2, T>, E.Obs, r), DA.step(T, ST.real(T, sh), op), (ST.real(T, sh2), TR.so_obs(T, sh, op, SP.step_ok(T, sh, op, g))), TR.so_step(T, sh, op, SP.step_ok(T, sh, op, g))), TR.so_good(T, sh, op, SP.step_ok(T, sh, op, g)))) 67 68 # ---- arbitrary finite traces from a constructor ---- 69 70 def run_from(-T: Data, +ops: List<&2, E.Op>, +sh0: ST.Shadow, +g0: {ST.good(T, sh0) == True{} : Bool}) -> {DA.run(T, ops, ST.real(T, sh0)) == (ST.real(T, TR.ro_sh(T, ops, sh0, Nil{}, TR.run_ok(T, ops, sh0, Nil{}, g0))), TR.srun_obs(T, ops, ST.model(T, sh0))) : DA.DynArray<&2, T> & List<&2, E.Obs>}: 71 +sh2 = TR.ro_sh(T, ops, sh0, Nil{}, TR.run_ok(T, ops, sh0, Nil{}, g0)) 72 +os = TR.srun_obs(T, ops, ST.model(T, sh0)) 73 %Equal.sym(DA.DynArray<&2, T> & List<&2, E.Obs>, DA.run_acc(T, ops, (ST.real(T, sh0), Nil{})), (ST.real(T, sh2), List.reverse.go(&2, E.Obs, os, Nil{})), TR.ro_run(T, ops, sh0, Nil{}, TR.run_ok(T, ops, sh0, Nil{}, g0))) : {DA.finish(T, _) == (ST.real(T, sh2), os) : DA.DynArray<&2, T> & List<&2, E.Obs>} 74 %Equal.sym(List<&2, E.Obs>, List.reverse(&2, E.Obs, List.reverse.go(&2, E.Obs, os, Nil{})), os, LL.rev_rev(E.Obs, os)) : {(ST.real(T, sh2), _) == (ST.real(T, sh2), os) : DA.DynArray<&2, T> & List<&2, E.Obs>} 75 {==} 76 77 def trace_from(-T: Data, +ops: List<&2, E.Op>, +sh0: ST.Shadow, +g0: {ST.good(T, sh0) == True{} : Bool}) -> {view(T, DA.run(T, ops, ST.real(T, sh0))) == S.run(T, ops, ST.model(T, sh0)) : S.Model & List<&2, E.Obs>}: 78 +sh2 = TR.ro_sh(T, ops, sh0, Nil{}, TR.run_ok(T, ops, sh0, Nil{}, g0)) 79 +os = TR.srun_obs(T, ops, ST.model(T, sh0)) 80 %Equal.sym(DA.DynArray<&2, T> & List<&2, E.Obs>, DA.run(T, ops, ST.real(T, sh0)), (ST.real(T, sh2), os), run_from(T, ops, sh0, g0)) : {view(T, _) == S.run(T, ops, ST.model(T, sh0)) : S.Model & List<&2, E.Obs>} 81 %Equal.sym(S.Model, ST.abs(T, ST.real(T, sh2)), ST.model(T, sh2), ST.abs_real(T, sh2)) : {(_, os) == S.run(T, ops, ST.model(T, sh0)) : S.Model & List<&2, E.Obs>} 82 %Equal.sym(S.Model, ST.model(T, sh2), TR.srun_state(T, ops, ST.model(T, sh0)), TR.ro_model(T, ops, sh0, Nil{}, TR.run_ok(T, ops, sh0, Nil{}, g0))) : {(_, os) == S.run(T, ops, ST.model(T, sh0)) : S.Model & List<&2, E.Obs>} 83 Equal.sym(S.Model & List<&2, E.Obs>, S.run(T, ops, ST.model(T, sh0)), (TR.srun_state(T, ops, ST.model(T, sh0)), os), L.pair_eta(S.Model, List<&2, E.Obs>, S.run(T, ops, ST.model(T, sh0)))) 84 85 def inv_from(-T: Data, +ops: List<&2, E.Op>, +sh0: ST.Shadow, +g0: {ST.good(T, sh0) == True{} : Bool}) -> ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs>, DA.run(T, ops, ST.real(T, sh0)))): 86 +sh2 = TR.ro_sh(T, ops, sh0, Nil{}, TR.run_ok(T, ops, sh0, Nil{}, g0)) 87 (sh2, (Equal.cong(DA.DynArray<&2, T> & List<&2, E.Obs>, DA.DynArray<&2, T>, r => Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs>, r), DA.run(T, ops, ST.real(T, sh0)), (ST.real(T, sh2), TR.srun_obs(T, ops, ST.model(T, sh0))), run_from(T, ops, sh0, g0)), TR.ro_good(T, ops, sh0, Nil{}, TR.run_ok(T, ops, sh0, Nil{}, g0)))) 88 89 # Public trace laws: every finite op list run from DA.new / DA.with_limit 90 # through the actual DA.run equals the specification run, and the final 91 # array satisfies the invariant. 92 def trace_new(-T: Data, +ops: List<&2, E.Op>) -> {view(T, DA.run(T, ops, DA.new(T))) == S.run(T, ops, S.new(T)) : S.Model & List<&2, E.Obs>}: 93 trace_from(T, ops, TR.initial(T), TR.new_good(T)) 94 95 def trace_new_inv(-T: Data, +ops: List<&2, E.Op>) -> ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs>, DA.run(T, ops, DA.new(T)))): 96 inv_from(T, ops, TR.initial(T), TR.new_good(T)) 97 98 def trace_with_limit(-T: Data, +k: Nat, +ops: List<&2, E.Op>) -> {view(T, DA.run(T, ops, DA.with_limit(T, k))) == S.run(T, ops, S.with_limit(T, k)) : S.Model & List<&2, E.Obs>}: 99 %with_limit_abs(T, k) : {view(T, DA.run(T, ops, DA.with_limit(T, k))) == S.run(T, ops, _) : S.Model & List<&2, E.Obs>} 100 trace_from(T, ops, TR.limited(T, k), limit_good(T, k)) 101 102 def trace_with_limit_inv(-T: Data, +k: Nat, +ops: List<&2, E.Op>) -> ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs>, DA.run(T, ops, DA.with_limit(T, k)))): 103 inv_from(T, ops, TR.limited(T, k), limit_good(T, k)) 104 105 # ---- the executable specializations (closed element type) ---- 106 # 107 # DA.*_at is what tests and benchmarks run (see src/dynamic_array.bend for 108 # why a closed element type is required by the native backend). CL.*_eq 109 # proves each specialization equal to the parametric definition, so every 110 # law above holds verbatim of the executed code. 111 112 def new_at_abs(~T: Data) -> {ST.abs(T, DA.new_at(~T)) == S.new(T) : S.Model}: 113 %Equal.sym(DA.DynArray<&2, T>, DA.new_at(~T), DA.new(T), CL.new_eq(~T)) : {ST.abs(T, _) == S.new(T) : S.Model} 114 new_abs(T) 115 116 def new_at_inv(~T: Data) -> ST.Inv(T, DA.new_at(~T)): 117 %Equal.sym(DA.DynArray<&2, T>, DA.new_at(~T), DA.new(T), CL.new_eq(~T)) : ST.Inv(T, _) 118 new_inv(T) 119 120 def with_limit_at_abs(~T: Data, +k: Nat) -> {ST.abs(T, DA.with_limit_at(~T, k)) == S.with_limit(T, k) : S.Model}: 121 %Equal.sym(DA.DynArray<&2, T>, DA.with_limit_at(~T, k), DA.with_limit(T, k), CL.with_limit_eq(~T, k)) : {ST.abs(T, _) == S.with_limit(T, k) : S.Model} 122 with_limit_abs(T, k) 123 124 def step_at_refines(~T: Data, +sh: ST.Shadow, +op: E.Op, +g: {ST.good(T, sh) == True{} : Bool}) -> {view1(T, DA.step_at(~T, ST.real(T, sh), op)) == S.step(T, ST.abs(T, ST.real(T, sh)), op) : S.Model & E.Obs}: 125 %Equal.sym(DA.DynArray<&2, T> & E.Obs, DA.step_at(~T, ST.real(T, sh), op), DA.step(T, ST.real(T, sh), op), CL.step_eq(~T, sh, op, g)) : {view1(T, _) == S.step(T, ST.abs(T, ST.real(T, sh)), op) : S.Model & E.Obs} 126 step_refines(T, sh, op, g) 127 128 def step_at_preserves(~T: Data, +sh: ST.Shadow, +op: E.Op, +g: {ST.good(T, sh) == True{} : Bool}) -> ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, E.Obs, DA.step_at(~T, ST.real(T, sh), op))): 129 %Equal.sym(DA.DynArray<&2, T> & E.Obs, DA.step_at(~T, ST.real(T, sh), op), DA.step(T, ST.real(T, sh), op), CL.step_eq(~T, sh, op, g)) : ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, E.Obs, _)) 130 step_preserves(T, sh, op, g) 131 132 def trace_new_at(~T: Data, +ops: List<&2, E.Op>) -> {view(T, DA.run_at(~T, ops, DA.new_at(~T))) == S.run(T, ops, S.new(T)) : S.Model & List<&2, E.Obs>}: 133 %Equal.sym(DA.DynArray<&2, T>, DA.new_at(~T), DA.new(T), CL.new_eq(~T)) : {view(T, DA.run_at(~T, ops, _)) == S.run(T, ops, S.new(T)) : S.Model & List<&2, E.Obs>} 134 %Equal.sym(DA.DynArray<&2, T> & List<&2, E.Obs>, DA.run_at(~T, ops, ST.real(T, TR.initial(T))), DA.run(T, ops, ST.real(T, TR.initial(T))), CL.run_eq(~T, ops, TR.initial(T), TR.new_good(T))) : {view(T, _) == S.run(T, ops, S.new(T)) : S.Model & List<&2, E.Obs>} 135 trace_new(T, ops) 136 137 def trace_new_at_inv(~T: Data, +ops: List<&2, E.Op>) -> ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs>, DA.run_at(~T, ops, DA.new_at(~T)))): 138 %Equal.sym(DA.DynArray<&2, T>, DA.new_at(~T), DA.new(T), CL.new_eq(~T)) : ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs>, DA.run_at(~T, ops, _))) 139 %Equal.sym(DA.DynArray<&2, T> & List<&2, E.Obs>, DA.run_at(~T, ops, ST.real(T, TR.initial(T))), DA.run(T, ops, ST.real(T, TR.initial(T))), CL.run_eq(~T, ops, TR.initial(T), TR.new_good(T))) : ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs>, _)) 140 trace_new_inv(T, ops) 141 142 def trace_with_limit_at(~T: Data, +k: Nat, +ops: List<&2, E.Op>) -> {view(T, DA.run_at(~T, ops, DA.with_limit_at(~T, k))) == S.run(T, ops, S.with_limit(T, k)) : S.Model & List<&2, E.Obs>}: 143 %Equal.sym(DA.DynArray<&2, T>, DA.with_limit_at(~T, k), DA.with_limit(T, k), CL.with_limit_eq(~T, k)) : {view(T, DA.run_at(~T, ops, _)) == S.run(T, ops, S.with_limit(T, k)) : S.Model & List<&2, E.Obs>} 144 %Equal.sym(DA.DynArray<&2, T> & List<&2, E.Obs>, DA.run_at(~T, ops, ST.real(T, TR.limited(T, k))), DA.run(T, ops, ST.real(T, TR.limited(T, k))), CL.run_eq(~T, ops, TR.limited(T, k), limit_good(T, k))) : {view(T, _) == S.run(T, ops, S.with_limit(T, k)) : S.Model & List<&2, E.Obs>} 145 trace_with_limit(T, k, ops) 146 147 def trace_with_limit_at_inv(~T: Data, +k: Nat, +ops: List<&2, E.Op>) -> ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs>, DA.run_at(~T, ops, DA.with_limit_at(~T, k)))): 148 %Equal.sym(DA.DynArray<&2, T>, DA.with_limit_at(~T, k), DA.with_limit(T, k), CL.with_limit_eq(~T, k)) : ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs>, DA.run_at(~T, ops, _))) 149 %Equal.sym(DA.DynArray<&2, T> & List<&2, E.Obs>, DA.run_at(~T, ops, ST.real(T, TR.limited(T, k))), DA.run(T, ops, ST.real(T, TR.limited(T, k))), CL.run_eq(~T, ops, TR.limited(T, k), limit_good(T, k))) : ST.Inv(T, Pair.fst(DA.DynArray<&2, T>, List<&2, E.Obs>, _)) 150 trace_with_limit_inv(T, k, ops) 151 152 # ==== the contract of dynamic_array (stated in spec/containers/dynamic_array.bend) ==================== 153 154 # ---- the implementation ---- 155 # every Post below is a property of S.step; it holds of DA.step read back 156 # through the abstraction (view1), on every good array 157 def impl(-T: Data, +sh: ST.Shadow, +op: E.Op, +g: {ST.good(T, sh) == True{} : Bool}, -Post: (S.Model & E.Obs) -> Type, pf: Post(S.step(T, ST.abs(T, ST.real(T, sh)), op))) -> Post(view1(T, DA.step(T, ST.real(T, sh), op))): 158 L.subst(S.Model & E.Obs, Post, S.step(T, ST.abs(T, ST.real(T, sh)), op), view1(T, DA.step(T, ST.real(T, sh), op)), Equal.sym(S.Model & E.Obs, view1(T, DA.step(T, ST.real(T, sh), op)), S.step(T, ST.abs(T, ST.real(T, sh)), op), step_refines(T, sh, op, g)), pf) 159 160 # ---- Length, Capacity, iteration: the value, and nothing changes ---- 161 def length_result(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Length.length_result(T, l, d, xs): 162 {==} 163 164 def length_frame(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Length.length_frame(T, l, d, xs): 165 {==} 166 167 def capacity_result(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Capacity.capacity_result(T, l, d, xs): 168 {==} 169 170 def capacity_frame(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Capacity.capacity_frame(T, l, d, xs): 171 {==} 172 173 def to_list_model(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Iteration.to_list_model(T, l, d, xs): 174 {==} 175 176 def to_list_frame(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Iteration.to_list_frame(T, l, d, xs): 177 {==} 178 179 # ---- Empty_Vector: Length 0 (the default capacity is 2^0) ---- 180 def new_empty(-T: Data) -> S.Empty_Vector.new_empty(T): 181 {==} 182 183 def new_capacity(-T: Data) -> S.Empty_Vector.new_capacity(T): 184 {==} 185 186 def new_impl(-T: Data) -> {ST.abs(T, DA.new(T)) == S.new(T) : S.Model}: 187 new_abs(T) 188 189 def with_limit_empty(-T: Data, +k: Nat) -> S.Empty_Vector.with_limit_empty(T, k): 190 {==} 191 192 def with_limit_impl(-T: Data, +k: Nat) -> {ST.abs(T, DA.with_limit(T, k)) == S.with_limit(T, k) : S.Model}: 193 with_limit_abs(T, k) 194 195 # ---- Reserve_Capacity: M.Equal (Model, Model'Old) ---- 196 def re_c(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +n: Nat, +c1: Bool, +h1: {Nat.is_le(n, SC.pow2(d)) == c1 : Bool}, +c2: Bool, +h2: {Nat.is_le(n, SC.pow2(l)) == c2 : Bool}) -> {S.items(T, S.nx(T, S.M{l, d, xs}, E.Reserve{n})) == xs : List<&2, T>}: 197 match c1 c2: 198 case True{} _: 199 %Equal.sym(Bool, Nat.is_le(n, SC.pow2(d)), True{}, h1) : {S.items(T, Pair.fst(S.Model, E.Obs, Bool.pick(S.Model & E.Obs, _, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model & E.Obs, Nat.is_le(n, SC.pow2(l)), (S.M{l, S.fit(n, d, n), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == xs : List<&2, T>} 200 {==} 201 case False{} True{}: 202 %Equal.sym(Bool, Nat.is_le(n, SC.pow2(d)), False{}, h1) : {S.items(T, Pair.fst(S.Model, E.Obs, Bool.pick(S.Model & E.Obs, _, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model & E.Obs, Nat.is_le(n, SC.pow2(l)), (S.M{l, S.fit(n, d, n), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == xs : List<&2, T>} 203 %Equal.sym(Bool, Nat.is_le(n, SC.pow2(l)), True{}, h2) : {S.items(T, Pair.fst(S.Model, E.Obs, Bool.pick(S.Model & E.Obs, False{}, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model & E.Obs, _, (S.M{l, S.fit(n, d, n), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == xs : List<&2, T>} 204 {==} 205 case False{} False{}: 206 %Equal.sym(Bool, Nat.is_le(n, SC.pow2(d)), False{}, h1) : {S.items(T, Pair.fst(S.Model, E.Obs, Bool.pick(S.Model & E.Obs, _, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model & E.Obs, Nat.is_le(n, SC.pow2(l)), (S.M{l, S.fit(n, d, n), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == xs : List<&2, T>} 207 %Equal.sym(Bool, Nat.is_le(n, SC.pow2(l)), False{}, h2) : {S.items(T, Pair.fst(S.Model, E.Obs, Bool.pick(S.Model & E.Obs, False{}, (S.M{l, d, xs}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model & E.Obs, _, (S.M{l, S.fit(n, d, n), xs}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == xs : List<&2, T>} 208 {==} 209 210 def reserve_equal(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +n: Nat) -> S.Reserve_Capacity.reserve_equal(T, l, d, xs, n): 211 re_c(T, l, d, xs, n, Nat.is_le(n, SC.pow2(d)), {==}, Nat.is_le(n, SC.pow2(l)), {==}) 212 213 # ---- Clear: Length 0 (the capacity is kept) ---- 214 def clear_length(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Clear.clear_length(T, l, d, xs): 215 {==} 216 217 def clear_capacity(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Clear.clear_capacity(T, l, d, xs): 218 {==} 219 220 # ---- Element / First_Element / Last_Element ---- 221 def get_element(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {SC.nth(T, xs, i) == Some{v} : Maybe<&2, T>}) -> S.Element.get_element(T, l, d, xs, i, v, h): 222 %Equal.sym(Maybe<&2, T>, SC.nth(T, xs, i), Some{v}, h) : {E.OItem{S.item_result(T, _)} == E.OItem{Done{v}} : E.Obs} 223 {==} 224 225 def get_frame(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat) -> S.Element.get_frame(T, l, d, xs, i): 226 {==} 227 228 def get_outside(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +h: {Nat.is_le(SC.length(T, xs), i) == True{} : Bool}) -> S.Element.get_outside(T, l, d, xs, i, h): 229 %Equal.sym(Maybe<&2, T>, SC.nth(T, xs, i), None{}, LL.nth_none(T, xs, i, h)) : {E.OItem{S.item_result(T, _)} == E.OItem{Fail{E.IndexOutOfRange{}}} : E.Obs} 230 {==} 231 232 def first_element(-T: Data, +l: Nat, +d: Nat, +h: T, +t: List<&2, T>) -> S.First_Element.first_element(T, l, d, h, t): 233 {==} 234 235 def last_element(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>) -> S.Last_Element.last_element(T, l, d, xs): 236 {==} 237 238 # ---- Replace_Element: Length kept, Element (Index) = New_Item, Equal_Except elsewhere ---- 239 def set_step(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> {S.step(T, S.M{l, d, xs}, E.Set{i, v}) == (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{Done{Unit{}}}) : S.Model & E.Obs}: 240 %Equal.sym(Bool, Nat.is_lt(i, SC.length(T, xs)), True{}, h) : {Bool.pick(S.Model & E.Obs, _, (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}})) == (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{Done{Unit{}}}) : S.Model & E.Obs} 241 {==} 242 243 def set_items(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> {S.items(T, S.nx(T, S.M{l, d, xs}, E.Set{i, v})) == SC.update(T, xs, i, v) : List<&2, T>}: 244 %Equal.sym(S.Model & E.Obs, S.step(T, S.M{l, d, xs}, E.Set{i, v}), (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{Done{Unit{}}}), set_step(T, l, d, xs, i, v, h)) : {S.items(T, Pair.fst(S.Model, E.Obs, _)) == SC.update(T, xs, i, v) : List<&2, T>} 245 {==} 246 247 def set_length(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> S.Replace_Element.set_length(T, l, d, xs, i, v, h): 248 %Equal.sym(List<&2, T>, S.items(T, S.nx(T, S.M{l, d, xs}, E.Set{i, v})), SC.update(T, xs, i, v), set_items(T, l, d, xs, i, v, h)) : {SC.length(T, _) == SC.length(T, xs) : Nat} 249 VL.update_length(T, xs, i, v) 250 251 def set_element(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> S.Replace_Element.set_element(T, l, d, xs, i, v, h): 252 %Equal.sym(List<&2, T>, S.items(T, S.nx(T, S.M{l, d, xs}, E.Set{i, v})), SC.update(T, xs, i, v), set_items(T, l, d, xs, i, v, h)) : {SC.nth(T, _, i) == Some{v} : Maybe<&2, T>} 253 VL.update_at(T, xs, i, v, h) 254 255 def set_except(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == True{} : Bool}) -> S.Replace_Element.set_except(T, l, d, xs, i, v, h): 256 L.subst(List<&2, T>, z => V.EqualExcept(T, xs, z, i), SC.update(T, xs, i, v), S.items(T, S.nx(T, S.M{l, d, xs}, E.Set{i, v})), Equal.sym(List<&2, T>, S.items(T, S.nx(T, S.M{l, d, xs}, E.Set{i, v})), SC.update(T, xs, i, v), set_items(T, l, d, xs, i, v, h)), VL.update_except(T, xs, i, v)) 257 258 def set_outside(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +i: Nat, +v: T, +h: {Nat.is_lt(i, SC.length(T, xs)) == False{} : Bool}) -> S.Replace_Element.set_outside(T, l, d, xs, i, v, h): 259 %Equal.sym(Bool, Nat.is_lt(i, SC.length(T, xs)), False{}, h) : {Bool.pick(S.Model & E.Obs, _, (S.M{l, d, SC.update(T, xs, i, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}})) == (S.M{l, d, xs}, E.OUnit{Fail{E.IndexOutOfRange{}}}) : S.Model & E.Obs} 260 {==} 261 262 def pi_c(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +c1: Bool, +h1: {Nat.is_lt(SC.length(T, xs), SC.pow2(d)) == c1 : Bool}, +c2: Bool, +h2: {Nat.is_lt(d, l) == c2 : Bool}, +hr: {Bool.or(c1, c2) == True{} : Bool}) -> {S.items(T, S.nx(T, S.M{l, d, xs}, E.Push{v})) == SC.snoc(T, xs, v) : List<&2, T>}: 263 match c1 c2: 264 case True{} _: 265 %Equal.sym(Bool, Nat.is_lt(SC.length(T, xs), SC.pow2(d)), True{}, h1) : {S.items(T, Pair.fst(S.Model, E.Obs, Bool.pick(S.Model & E.Obs, _, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model & E.Obs, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == SC.snoc(T, xs, v) : List<&2, T>} 266 {==} 267 case False{} True{}: 268 %Equal.sym(Bool, Nat.is_lt(SC.length(T, xs), SC.pow2(d)), False{}, h1) : {S.items(T, Pair.fst(S.Model, E.Obs, Bool.pick(S.Model & E.Obs, _, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model & E.Obs, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == SC.snoc(T, xs, v) : List<&2, T>} 269 %Equal.sym(Bool, Nat.is_lt(d, l), True{}, h2) : {S.items(T, Pair.fst(S.Model, E.Obs, Bool.pick(S.Model & E.Obs, False{}, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model & E.Obs, _, (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))))) == SC.snoc(T, xs, v) : List<&2, T>} 270 {==} 271 case False{} False{}: 272 Empty.absurd({S.items(T, S.nx(T, S.M{l, d, xs}, E.Push{v})) == SC.snoc(T, xs, v) : List<&2, T>}, L.false_true(hr)) 273 274 def push_items(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +hr: {S.room(T, l, d, xs) == True{} : Bool}) -> {S.items(T, S.nx(T, S.M{l, d, xs}, E.Push{v})) == SC.snoc(T, xs, v) : List<&2, T>}: 275 pi_c(T, l, d, xs, v, Nat.is_lt(SC.length(T, xs), SC.pow2(d)), {==}, Nat.is_lt(d, l), {==}, hr) 276 277 def push_length(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +hr: {S.room(T, l, d, xs) == True{} : Bool}) -> S.Append.push_length(T, l, d, xs, v, hr): 278 %Equal.sym(List<&2, T>, S.items(T, S.nx(T, S.M{l, d, xs}, E.Push{v})), SC.snoc(T, xs, v), push_items(T, l, d, xs, v, hr)) : {SC.length(T, _) == 1n+SC.length(T, xs) : Nat} 279 VL.snoc_length(T, xs, v) 280 281 def push_prefix(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +hr: {S.room(T, l, d, xs) == True{} : Bool}) -> S.Append.push_prefix(T, l, d, xs, v, hr): 282 L.subst(List<&2, T>, z => V.EqualPrefix(T, xs, z), SC.snoc(T, xs, v), S.items(T, S.nx(T, S.M{l, d, xs}, E.Push{v})), Equal.sym(List<&2, T>, S.items(T, S.nx(T, S.M{l, d, xs}, E.Push{v})), SC.snoc(T, xs, v), push_items(T, l, d, xs, v, hr)), VL.snoc_prefix(T, xs, v)) 283 284 def push_element(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +hr: {S.room(T, l, d, xs) == True{} : Bool}) -> S.Append.push_element(T, l, d, xs, v, hr): 285 %Equal.sym(List<&2, T>, S.items(T, S.nx(T, S.M{l, d, xs}, E.Push{v})), SC.snoc(T, xs, v), push_items(T, l, d, xs, v, hr)) : {SC.nth(T, _, SC.length(T, xs)) == Some{v} : Maybe<&2, T>} 286 VL.snoc_last(T, xs, v) 287 288 def push_full(-T: Data, +l: Nat, +d: Nat, +xs: List<&2, T>, +v: T, +h1: {Nat.is_lt(SC.length(T, xs), SC.pow2(d)) == False{} : Bool}, +h2: {Nat.is_lt(d, l) == False{} : Bool}) -> S.Append.push_full(T, l, d, xs, v, h1, h2): 289 %Equal.sym(Bool, Nat.is_lt(SC.length(T, xs), SC.pow2(d)), False{}, h1) : {Bool.pick(S.Model & E.Obs, _, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model & E.Obs, Nat.is_lt(d, l), (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) == (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) : S.Model & E.Obs} 290 %Equal.sym(Bool, Nat.is_lt(d, l), False{}, h2) : {Bool.pick(S.Model & E.Obs, False{}, (S.M{l, d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), Bool.pick(S.Model & E.Obs, _, (S.M{l, 1n+d, SC.snoc(T, xs, v)}, E.OUnit{S.ok_unit()}), (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}))) == (S.M{l, d, xs}, E.OUnit{Fail{E.CapacityExceeded{}}}) : S.Model & E.Obs} 291 {==} 292 293 # ---- Delete_Last: Length - 1, Equal_Prefix (Model, Model'Old); pop returns Last_Element'Old ---- 294 def pop_length(-T: Data, +l: Nat, +d: Nat, +h: T, +t: List<&2, T>) -> S.Delete_Last.pop_length(T, l, d, h, t): 295 VL.init_length(T, t, h) 296 297 def pop_prefix(-T: Data, +l: Nat, +d: Nat, +h: T, +t: List<&2, T>) -> S.Delete_Last.pop_prefix(T, l, d, h, t): 298 VL.init_prefix(T, t, h) 299 300 def pop_result(-T: Data, +l: Nat, +d: Nat, +h: T, +t: List<&2, T>) -> S.Delete_Last.pop_result(T, l, d, h, t): 301 %Equal.sym(Maybe<&2, T>, SC.last(T, Con{h, t}), V.last_elem(T, Con{h, t}), VL.last_is_elem(T, t, h)) : {E.OItem{S.item_result(T, _)} == E.OItem{S.item_result(T, V.last_elem(T, Con{h, t}))} : E.Obs} 302 {==} 303 304 def pop_empty(-T: Data, +l: Nat, +d: Nat) -> S.Delete_Last.pop_empty(T, l, d): 305 {==}