proofs/containers/dynamic_array/state.bend
bend-collections-laws-containers@1.0.0.0 · 108 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
7import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
8import bend-collections-laws-containers@1.0.0.0/spec/containers/dynamic_array.bend as S
9import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as DA
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/layout.bend as LY
11import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as E
12
13# Shadow (Data) description of a reachable dynamic array: limit, depth,
14# length and the mirror tree t of its Base.Array (the array is thaw(t)).
15
16type Shadow<-T: Data> is Data:
17 Sh{limit: Nat, depth: Nat, len: Nat, tree: AR.Tree<Maybe<&2, T>>}
18
19def real(-T: Data, sh: Shadow<T>) -> DA.DynArray<&2, T>:
20 match sh:
21 case Sh{l, +d, n, t}:
22 DA.DA{l, d, SC.pow2(d), n, AR.thaw(Maybe<&2, T>, t)}
23
24# Representation invariant.
25def good(-T: Data, sh: Shadow<T>) -> Bool:
26 match sh:
27 case Sh{+l, +d, +n, +t}:
28 Bool.and(Nat.is_le(l, 31n), Bool.and(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n))))
29
30def model(-T: Data, sh: Shadow<T>) -> S.Model<T>:
31 match sh:
32 case Sh{l, d, n, t}:
33 S.M{l, d, LY.somes(T, AR.slots(Maybe<&2, T>, t))}
34
35# Abstraction of an actual dynamic array (proof-level; reads the Base.Array
36# tree through AR.freeze).
37def abs(-T: Data, da: DA.DynArray<&2, T>) -> S.Model<T>:
38 match da:
39 case DA.DA{l, d, c, n, arr}:
40 S.M{l, d, LY.somes(T, AR.slots(Maybe<&2, T>, AR.freeze(Maybe<&2, T>, arr)))}
41
42def abs_real(-T: Data, +sh: Shadow<T>) -> {abs(T, real(T, sh)) == model(T, sh) : S.Model<T>}:
43 match sh:
44 case Sh{+l, +d, +n, +t}:
45 %Equal.sym(AR.Tree<Maybe<&2, T>>, AR.freeze(Maybe<&2, T>, AR.thaw(Maybe<&2, T>, t)), t, AR.freeze_thaw(Maybe<&2, T>, t)) : {S.M{l, d, LY.somes(T, AR.slots(Maybe<&2, T>, _))} == S.M{l, d, LY.somes(T, AR.slots(Maybe<&2, T>, t))} : S.Model<T>}
46 {==}
47
48# Invariant of an actual array: it is the realization of a good shadow.
49def Inv(-T: Data, da: DA.DynArray<&2, T>) -> Type:
50 Sigma<&1, &1, Shadow<T>, sh => {da == real(T, sh) : DA.DynArray<&2, T>} & {good(T, sh) == True{} : Bool}>
51
52# ---- projections of good ----
53
54def g_limit(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {good(T, Sh{l, d, n, t}) == True{} : Bool}) -> {Nat.is_le(l, 31n) == True{} : Bool}:
55 L.and_left(Nat.is_le(l, 31n), Bool.and(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n))), g)
56
57def g_rest1(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {good(T, Sh{l, d, n, t}) == True{} : Bool}) -> {Bool.and(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n))) == True{} : Bool}:
58 L.and_right(Nat.is_le(l, 31n), Bool.and(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n))), g)
59
60def g_depth(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {good(T, Sh{l, d, n, t}) == True{} : Bool}) -> {Nat.is_le(d, l) == True{} : Bool}:
61 L.and_left(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n)), g_rest1(T, l, d, n, t, g))
62
63def g_rest2(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {good(T, Sh{l, d, n, t}) == True{} : Bool}) -> {Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n)) == True{} : Bool}:
64 L.and_right(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n)), g_rest1(T, l, d, n, t, g))
65
66def g_perfect(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {good(T, Sh{l, d, n, t}) == True{} : Bool}) -> {AR.perfect(Maybe<&2, T>, d, t) == True{} : Bool}:
67 L.and_left(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n), g_rest2(T, l, d, n, t, g))
68
69def g_lay(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +g: {good(T, Sh{l, d, n, t}) == True{} : Bool}) -> {LY.lay(T, AR.slots(Maybe<&2, T>, t), n) == True{} : Bool}:
70 L.and_right(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n), g_rest2(T, l, d, n, t, g))
71
72def good_intro(-T: Data, +l: Nat, +d: Nat, +n: Nat, +t: AR.Tree<Maybe<&2, T>>, +a: {Nat.is_le(l, 31n) == True{} : Bool}, +b: {Nat.is_le(d, l) == True{} : Bool}, +c: {AR.perfect(Maybe<&2, T>, d, t) == True{} : Bool}, +e: {LY.lay(T, AR.slots(Maybe<&2, T>, t), n) == True{} : Bool}) -> {good(T, Sh{l, d, n, t}) == True{} : Bool}:
73 L.and_intro(Nat.is_le(l, 31n), Bool.and(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n))), a,
74 L.and_intro(Nat.is_le(d, l), Bool.and(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n)), b,
75 L.and_intro(AR.perfect(Maybe<&2, T>, d, t), LY.lay(T, AR.slots(Maybe<&2, T>, t), n), c, e)))
76
77# ---- derived facts ----
78
79def lt32(+d: Nat, +l: Nat, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hl: {Nat.is_le(l, 31n) == True{} : Bool}) -> {Nat.is_lt(d, 32n) == True{} : Bool}:
80 N.le_lt_succ(d, 31n, N.le_trans(d, l, 31n, hd, hl))
81
82def le32(+d: Nat, +l: Nat, +hd: {Nat.is_le(d, l) == True{} : Bool}, +hl: {Nat.is_le(l, 31n) == True{} : Bool}) -> {Nat.is_le(d, 32n) == True{} : Bool}:
83 N.lt_le(d, 32n, lt32(d, l, hd, hl))
84
85def pow2_src(+d: Nat) -> {DA.pow2(d) == SC.pow2(d) : Nat}:
86 match d:
87 case 0n:
88 {==}
89 case 1n+p:
90 Equal.cong(Nat, Nat, Nat.double, DA.pow2(p), SC.pow2(p), pow2_src(p))
91
92def slot_item(-T: Data, +m: Maybe<&2, T>) -> {DA.slot_result(T, m) == S.item_result(T, m) : Result<&2, &2, E.Error, T>}:
93 match m:
94 case None{}:
95 {==}
96 case Some{x}:
97 {==}
98
99def empty_eq(-T: Data, +d: Nat) -> {DA.empty_slots(T, d) == AR.thaw(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})) : Array<Maybe<&2, T>>}:
100 AR.new(Maybe<&2, T>, d, None{})
101
102def grown_eq(-T: Data, +d: Nat, +t: AR.Tree<Maybe<&2, T>>) -> {DA.grown(T, d, AR.thaw(Maybe<&2, T>, t)) == AR.thaw(Maybe<&2, T>, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}) : Array<Maybe<&2, T>>}:
103 %Equal.sym(Array<Maybe<&2, T>>, DA.empty_slots(T, d), AR.thaw(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), empty_eq(T, d)) : {ANode{AR.thaw(Maybe<&2, T>, t), _} == ANode{AR.thaw(Maybe<&2, T>, t), AR.thaw(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{}))} : Array<Maybe<&2, T>>}
104 {==}
105
106def slots_grown(-T: Data, +d: Nat, +t: AR.Tree<Maybe<&2, T>>) -> {AR.slots(Maybe<&2, T>, AR.TNode{t, AR.trep(Maybe<&2, T>, d, None{})}) == SC.append(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{})) : List<&2, Maybe<&2, T>>}:
107 %Equal.sym(List<&2, Maybe<&2, T>>, AR.slots(Maybe<&2, T>, AR.trep(Maybe<&2, T>, d, None{})), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{}), AR.trep_slots(Maybe<&2, T>, d, None{})) : {SC.append(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), _) == SC.append(Maybe<&2, T>, AR.slots(Maybe<&2, T>, t), SC.replicate(Maybe<&2, T>, SC.pow2(d), None{})) : List<&2, Maybe<&2, T>>}
108 {==}