proofs/containers/dynamic_array/owned_instances.bend
bend-collections-laws-containers@1.0.0.0 · 113 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as A
3import bend-collections-laws-containers@1.0.0.0/src/containers/types/dynamic_array.bend as E
4import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/owned.bend as P
5
6# Explicit checked instances: template declarations alone are not proof checks.
7def array_new_length() -> {A.length_owned(~Array<U32>, A.new_owned(~Array<U32>)) == (A.new_owned(~Array<U32>), 0n) : A.DynArray<Array<U32>> & Nat}:
8 P.new_length(~Array<U32>)
9
10def array_new_capacity() -> {A.capacity_owned(~Array<U32>, A.new_owned(~Array<U32>)) == (A.new_owned(~Array<U32>), 1n) : A.DynArray<Array<U32>> & Nat}:
11 P.new_capacity(~Array<U32>)
12
13def array_empty_pop(l: Nat, d: Nat, c: Nat, a: Array<Maybe<Array<U32>>>) -> {A.pop_owned(~Array<U32>, A.DA{l, d, c, 0n, a}) == (A.DA{l, d, c, 0n, a}, Fail{E.EmptyArray{}}) : A.DynArray<Array<U32>> & Result<&2, &1, E.Error, Array<U32>>}:
14 P.empty_pop(~Array<U32>, l, d, c, a)
15
16def array_swap_rejected(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<Array<U32>>>, i: Nat, v: Array<U32>) -> {A.swap_checked_owned(~Array<U32>, l, d, c, n, a, i, v, False{}) == (A.DA{l, d, c, n, a}, Fail{E.Rejected{E.IndexOutOfRange{}, v}}) : A.DynArray<Array<U32>> & Result<&1, &1, E.Rejected<Array<U32>>, Maybe<Array<U32>>>}:
17 P.swap_rejected(~Array<U32>, l, d, c, n, a, i, v)
18
19def array_push_rejected(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<Array<U32>>>, v: Array<U32>) -> {A.push_room_owned(~Array<U32>, l, d, c, n, a, v, False{}, False{}) == (A.DA{l, d, c, n, a}, Fail{E.Rejected{E.CapacityExceeded{}, v}}) : A.DynArray<Array<U32>> & Result<&1, &2, E.Rejected<Array<U32>>, Unit>}:
20 P.push_rejected(~Array<U32>, l, d, c, n, a, v)
21
22def array_update_rejected(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<Array<U32>>>, i: Nat, f: Array<U32> -> Array<U32> & Array<U32>) -> {A.update_checked_owned(~Array<U32>, ~Array<U32>, l, d, c, n, a, i, f, False{}) == (A.DA{l, d, c, n, a}, Fail{E.IndexOutOfRange{}}) : A.DynArray<Array<U32>> & Result<&2, &1, E.Error, Array<U32>>}:
23 P.update_rejected(~Array<U32>, ~Array<U32>, l, d, c, n, a, i, f)
24
25def array_first_push_pop(x: Array<U32>) -> {A.pop_owned(~Array<U32>, Pair.fst(A.DynArray<Array<U32>>, Result<&1, &2, E.Rejected<Array<U32>>, Unit>, A.push_owned(~Array<U32>, A.new_owned(~Array<U32>), x))) == (A.new_owned(~Array<U32>), Done{x}) : A.DynArray<Array<U32>> & Result<&2, &1, E.Error, Array<U32>>}:
26 P.first_push_pop(~Array<U32>, x)
27
28def array_first_swap(x: Array<U32>, y: Array<U32>) -> {A.swap_owned(~Array<U32>, A.DA{31n, 0n, 1n, 1n, ALeaf{Some{x}}}, 0n, y) == (A.DA{31n, 0n, 1n, 1n, ALeaf{Some{y}}}, Done{Some{x}}) : A.DynArray<Array<U32>> & Result<&1, &1, E.Rejected<Array<U32>>, Maybe<Array<U32>>>}:
29 P.first_swap(~Array<U32>, x, y)
30
31def array_first_update(x: Array<U32>, f: Array<U32> -> Array<U32> & Array<U32>) -> {A.update_owned(~Array<U32>, ~Array<U32>, A.DA{31n, 0n, 1n, 1n, ALeaf{Some{x}}}, 0n, f) == A.update_put_owned(~Array<U32>, ~Array<U32>, 31n, 0n, 1n, 1n, ALeaf{None{}}, 0n, f(x)) : A.DynArray<Array<U32>> & Result<&2, &1, E.Error, Array<U32>>}:
32 P.first_update(~Array<U32>, ~Array<U32>, x, f)
33
34def array_clear_length(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<Array<U32>>>) -> {A.length_owned(~Array<U32>, A.clear_owned(~Array<U32>, A.DA{l, d, c, n, a})) == (A.DA{l, d, c, 0n, A.empty_owned(~Array<U32>, d)}, 0n) : A.DynArray<Array<U32>> & Nat}:
35 P.clear_length(~Array<U32>, l, d, c, n, a)
36
37def array_clear_capacity(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<Array<U32>>>) -> {A.capacity_owned(~Array<U32>, A.clear_owned(~Array<U32>, A.DA{l, d, c, n, a})) == (A.DA{l, d, c, 0n, A.empty_owned(~Array<U32>, d)}, c) : A.DynArray<Array<U32>> & Nat}:
38 P.clear_capacity(~Array<U32>, l, d, c, n, a)
39
40def array_first_drain(x: Array<U32>) -> {A.into_list_owned(~Array<U32>, A.DA{31n, 0n, 1n, 1n, ALeaf{Some{x}}}) == Con{x, Nil{}} : List<Array<U32>>}:
41 P.first_drain(~Array<U32>, x)
42
43def nested_new_length() -> {A.length_owned(~A.DynArray<&2, U32>, A.new_owned(~A.DynArray<&2, U32>)) == (A.new_owned(~A.DynArray<&2, U32>), 0n) : A.DynArray<A.DynArray<&2, U32>> & Nat}:
44 P.new_length(~A.DynArray<&2, U32>)
45
46def nested_new_capacity() -> {A.capacity_owned(~A.DynArray<&2, U32>, A.new_owned(~A.DynArray<&2, U32>)) == (A.new_owned(~A.DynArray<&2, U32>), 1n) : A.DynArray<A.DynArray<&2, U32>> & Nat}:
47 P.new_capacity(~A.DynArray<&2, U32>)
48
49def nested_empty_pop(l: Nat, d: Nat, c: Nat, a: Array<Maybe<A.DynArray<&2, U32>>>) -> {A.pop_owned(~A.DynArray<&2, U32>, A.DA{l, d, c, 0n, a}) == (A.DA{l, d, c, 0n, a}, Fail{E.EmptyArray{}}) : A.DynArray<A.DynArray<&2, U32>> & Result<&2, &1, E.Error, A.DynArray<&2, U32>>}:
50 P.empty_pop(~A.DynArray<&2, U32>, l, d, c, a)
51
52def nested_swap_rejected(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<A.DynArray<&2, U32>>>, i: Nat, v: A.DynArray<&2, U32>) -> {A.swap_checked_owned(~A.DynArray<&2, U32>, l, d, c, n, a, i, v, False{}) == (A.DA{l, d, c, n, a}, Fail{E.Rejected{E.IndexOutOfRange{}, v}}) : A.DynArray<A.DynArray<&2, U32>> & Result<&1, &1, E.Rejected<A.DynArray<&2, U32>>, Maybe<A.DynArray<&2, U32>>>}:
53 P.swap_rejected(~A.DynArray<&2, U32>, l, d, c, n, a, i, v)
54
55def nested_push_rejected(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<A.DynArray<&2, U32>>>, v: A.DynArray<&2, U32>) -> {A.push_room_owned(~A.DynArray<&2, U32>, l, d, c, n, a, v, False{}, False{}) == (A.DA{l, d, c, n, a}, Fail{E.Rejected{E.CapacityExceeded{}, v}}) : A.DynArray<A.DynArray<&2, U32>> & Result<&1, &2, E.Rejected<A.DynArray<&2, U32>>, Unit>}:
56 P.push_rejected(~A.DynArray<&2, U32>, l, d, c, n, a, v)
57
58def nested_update_rejected(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<A.DynArray<&2, U32>>>, i: Nat, f: A.DynArray<&2, U32> -> A.DynArray<&2, U32> & Array<U32>) -> {A.update_checked_owned(~A.DynArray<&2, U32>, ~Array<U32>, l, d, c, n, a, i, f, False{}) == (A.DA{l, d, c, n, a}, Fail{E.IndexOutOfRange{}}) : A.DynArray<A.DynArray<&2, U32>> & Result<&2, &1, E.Error, Array<U32>>}:
59 P.update_rejected(~A.DynArray<&2, U32>, ~Array<U32>, l, d, c, n, a, i, f)
60
61def nested_first_push_pop(x: A.DynArray<&2, U32>) -> {A.pop_owned(~A.DynArray<&2, U32>, Pair.fst(A.DynArray<A.DynArray<&2, U32>>, Result<&1, &2, E.Rejected<A.DynArray<&2, U32>>, Unit>, A.push_owned(~A.DynArray<&2, U32>, A.new_owned(~A.DynArray<&2, U32>), x))) == (A.new_owned(~A.DynArray<&2, U32>), Done{x}) : A.DynArray<A.DynArray<&2, U32>> & Result<&2, &1, E.Error, A.DynArray<&2, U32>>}:
62 P.first_push_pop(~A.DynArray<&2, U32>, x)
63
64def nested_first_swap(x: A.DynArray<&2, U32>, y: A.DynArray<&2, U32>) -> {A.swap_owned(~A.DynArray<&2, U32>, A.DA{31n, 0n, 1n, 1n, ALeaf{Some{x}}}, 0n, y) == (A.DA{31n, 0n, 1n, 1n, ALeaf{Some{y}}}, Done{Some{x}}) : A.DynArray<A.DynArray<&2, U32>> & Result<&1, &1, E.Rejected<A.DynArray<&2, U32>>, Maybe<A.DynArray<&2, U32>>>}:
65 P.first_swap(~A.DynArray<&2, U32>, x, y)
66
67def nested_first_update(x: A.DynArray<&2, U32>, f: A.DynArray<&2, U32> -> A.DynArray<&2, U32> & Array<U32>) -> {A.update_owned(~A.DynArray<&2, U32>, ~Array<U32>, A.DA{31n, 0n, 1n, 1n, ALeaf{Some{x}}}, 0n, f) == A.update_put_owned(~A.DynArray<&2, U32>, ~Array<U32>, 31n, 0n, 1n, 1n, ALeaf{None{}}, 0n, f(x)) : A.DynArray<A.DynArray<&2, U32>> & Result<&2, &1, E.Error, Array<U32>>}:
68 P.first_update(~A.DynArray<&2, U32>, ~Array<U32>, x, f)
69
70def nested_clear_length(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<A.DynArray<&2, U32>>>) -> {A.length_owned(~A.DynArray<&2, U32>, A.clear_owned(~A.DynArray<&2, U32>, A.DA{l, d, c, n, a})) == (A.DA{l, d, c, 0n, A.empty_owned(~A.DynArray<&2, U32>, d)}, 0n) : A.DynArray<A.DynArray<&2, U32>> & Nat}:
71 P.clear_length(~A.DynArray<&2, U32>, l, d, c, n, a)
72
73def nested_clear_capacity(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<A.DynArray<&2, U32>>>) -> {A.capacity_owned(~A.DynArray<&2, U32>, A.clear_owned(~A.DynArray<&2, U32>, A.DA{l, d, c, n, a})) == (A.DA{l, d, c, 0n, A.empty_owned(~A.DynArray<&2, U32>, d)}, c) : A.DynArray<A.DynArray<&2, U32>> & Nat}:
74 P.clear_capacity(~A.DynArray<&2, U32>, l, d, c, n, a)
75
76def nested_first_drain(x: A.DynArray<&2, U32>) -> {A.into_list_owned(~A.DynArray<&2, U32>, A.DA{31n, 0n, 1n, 1n, ALeaf{Some{x}}}) == Con{x, Nil{}} : List<A.DynArray<&2, U32>>}:
77 P.first_drain(~A.DynArray<&2, U32>, x)
78
79def closure_new_length() -> {A.length_owned(~(U32 -> U32), A.new_owned(~(U32 -> U32))) == (A.new_owned(~(U32 -> U32)), 0n) : A.DynArray<(U32 -> U32)> & Nat}:
80 P.new_length(~(U32 -> U32))
81
82def closure_new_capacity() -> {A.capacity_owned(~(U32 -> U32), A.new_owned(~(U32 -> U32))) == (A.new_owned(~(U32 -> U32)), 1n) : A.DynArray<(U32 -> U32)> & Nat}:
83 P.new_capacity(~(U32 -> U32))
84
85def closure_empty_pop(l: Nat, d: Nat, c: Nat, a: Array<Maybe<(U32 -> U32)>>) -> {A.pop_owned(~(U32 -> U32), A.DA{l, d, c, 0n, a}) == (A.DA{l, d, c, 0n, a}, Fail{E.EmptyArray{}}) : A.DynArray<(U32 -> U32)> & Result<&2, &1, E.Error, (U32 -> U32)>}:
86 P.empty_pop(~(U32 -> U32), l, d, c, a)
87
88def closure_swap_rejected(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<(U32 -> U32)>>, i: Nat, v: (U32 -> U32)) -> {A.swap_checked_owned(~(U32 -> U32), l, d, c, n, a, i, v, False{}) == (A.DA{l, d, c, n, a}, Fail{E.Rejected{E.IndexOutOfRange{}, v}}) : A.DynArray<(U32 -> U32)> & Result<&1, &1, E.Rejected<(U32 -> U32)>, Maybe<(U32 -> U32)>>}:
89 P.swap_rejected(~(U32 -> U32), l, d, c, n, a, i, v)
90
91def closure_push_rejected(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<(U32 -> U32)>>, v: (U32 -> U32)) -> {A.push_room_owned(~(U32 -> U32), l, d, c, n, a, v, False{}, False{}) == (A.DA{l, d, c, n, a}, Fail{E.Rejected{E.CapacityExceeded{}, v}}) : A.DynArray<(U32 -> U32)> & Result<&1, &2, E.Rejected<(U32 -> U32)>, Unit>}:
92 P.push_rejected(~(U32 -> U32), l, d, c, n, a, v)
93
94def closure_update_rejected(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<(U32 -> U32)>>, i: Nat, f: (U32 -> U32) -> (U32 -> U32) & Array<U32>) -> {A.update_checked_owned(~(U32 -> U32), ~Array<U32>, l, d, c, n, a, i, f, False{}) == (A.DA{l, d, c, n, a}, Fail{E.IndexOutOfRange{}}) : A.DynArray<(U32 -> U32)> & Result<&2, &1, E.Error, Array<U32>>}:
95 P.update_rejected(~(U32 -> U32), ~Array<U32>, l, d, c, n, a, i, f)
96
97def closure_first_push_pop(x: (U32 -> U32)) -> {A.pop_owned(~(U32 -> U32), Pair.fst(A.DynArray<(U32 -> U32)>, Result<&1, &2, E.Rejected<(U32 -> U32)>, Unit>, A.push_owned(~(U32 -> U32), A.new_owned(~(U32 -> U32)), x))) == (A.new_owned(~(U32 -> U32)), Done{x}) : A.DynArray<(U32 -> U32)> & Result<&2, &1, E.Error, (U32 -> U32)>}:
98 P.first_push_pop(~(U32 -> U32), x)
99
100def closure_first_swap(x: (U32 -> U32), y: (U32 -> U32)) -> {A.swap_owned(~(U32 -> U32), A.DA{31n, 0n, 1n, 1n, ALeaf{Some{x}}}, 0n, y) == (A.DA{31n, 0n, 1n, 1n, ALeaf{Some{y}}}, Done{Some{x}}) : A.DynArray<(U32 -> U32)> & Result<&1, &1, E.Rejected<(U32 -> U32)>, Maybe<(U32 -> U32)>>}:
101 P.first_swap(~(U32 -> U32), x, y)
102
103def closure_first_update(x: (U32 -> U32), f: (U32 -> U32) -> (U32 -> U32) & Array<U32>) -> {A.update_owned(~(U32 -> U32), ~Array<U32>, A.DA{31n, 0n, 1n, 1n, ALeaf{Some{x}}}, 0n, f) == A.update_put_owned(~(U32 -> U32), ~Array<U32>, 31n, 0n, 1n, 1n, ALeaf{None{}}, 0n, f(x)) : A.DynArray<(U32 -> U32)> & Result<&2, &1, E.Error, Array<U32>>}:
104 P.first_update(~(U32 -> U32), ~Array<U32>, x, f)
105
106def closure_clear_length(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<(U32 -> U32)>>) -> {A.length_owned(~(U32 -> U32), A.clear_owned(~(U32 -> U32), A.DA{l, d, c, n, a})) == (A.DA{l, d, c, 0n, A.empty_owned(~(U32 -> U32), d)}, 0n) : A.DynArray<(U32 -> U32)> & Nat}:
107 P.clear_length(~(U32 -> U32), l, d, c, n, a)
108
109def closure_clear_capacity(l: Nat, d: Nat, c: Nat, n: Nat, a: Array<Maybe<(U32 -> U32)>>) -> {A.capacity_owned(~(U32 -> U32), A.clear_owned(~(U32 -> U32), A.DA{l, d, c, n, a})) == (A.DA{l, d, c, 0n, A.empty_owned(~(U32 -> U32), d)}, c) : A.DynArray<(U32 -> U32)> & Nat}:
110 P.clear_capacity(~(U32 -> U32), l, d, c, n, a)
111
112def closure_first_drain(x: (U32 -> U32)) -> {A.into_list_owned(~(U32 -> U32), A.DA{31n, 0n, 1n, 1n, ALeaf{Some{x}}}) == Con{x, Nil{}} : List<(U32 -> U32)>}:
113 P.first_drain(~(U32 -> U32), x)