-
Notifications
You must be signed in to change notification settings - Fork 88
Expand file tree
/
Copy pathinplace_list_reversal.coma
More file actions
146 lines (117 loc) · 5.63 KB
/
Copy pathinplace_list_reversal.coma
File metadata and controls
146 lines (117 loc) · 5.63 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
module M_rev
use creusot.prelude.MutBorrow
use creusot.prelude.Any
type t_T
type tup2_T_List_T = { f0: t_T; f1: t_List_T }
with t_List_T = Nil | Cons tup2_T_List_T
predicate inv_T (_1: t_T)
predicate inv_List_T (_1: t_List_T)
predicate inv_tup2_T_List_T [@inline:trivial] (_1: tup2_T_List_T) = inv_T _1.f0 /\ inv_List_T _1.f1
meta "rewrite_def" predicate inv_tup2_T_List_T
predicate invariant_Box_tup2_T_List_T_Global (self: tup2_T_List_T) = inv_tup2_T_List_T self
predicate inv_Box_tup2_T_List_T_Global [@inline:trivial] (_1: tup2_T_List_T) = invariant_Box_tup2_T_List_T_Global _1
meta "rewrite_def" predicate inv_Box_tup2_T_List_T_Global
axiom inv_axiom [@rewrite]: forall x: t_List_T [inv_List_T x]. inv_List_T x
= match x with
| Nil -> true
| Cons f0'0 -> inv_Box_tup2_T_List_T_Global f0'0
end
predicate invariant_refmut_List_T [@inline:trivial] (self: MutBorrow.t t_List_T) =
inv_List_T self.current /\ inv_List_T self.final
meta "rewrite_def" predicate invariant_refmut_List_T
predicate inv_refmut_List_T [@inline:trivial] (_1: MutBorrow.t t_List_T) = invariant_refmut_List_T _1
meta "rewrite_def" predicate inv_refmut_List_T
let replace_List_T (dest: MutBorrow.t t_List_T) (src: t_List_T) (return (x: t_List_T)) =
{[@stop_split] [@expl:replace_List_T requires] ([@stop_split] [@expl:replace 'dest' type invariant] inv_refmut_List_T dest)
/\ ([@stop_split] [@expl:replace 'src' type invariant] inv_List_T src)}
any
[ return (result: t_List_T) ->
{[@stop_split] [@expl:replace_List_T ensures] ([@stop_split] [@expl:replace result type invariant] inv_List_T result)
/\ ([@stop_split] [@expl:replace ensures #0] dest.final = src)
/\ ([@stop_split] [@expl:replace ensures #1] result = dest.current)}
(! return {result}) ]
function rev_append_T (n: t_List_T) (o: t_List_T) : t_List_T = match n with
| Nil -> o
| Cons {f0 = hd; f1 = tl} -> rev_append_T tl (Cons { f0 = hd; f1 = o })
end
let elim_Cons (_x: t_List_T) (return (f0'0: tup2_T_List_T)) = any
[ _k (f0'0: tup2_T_List_T) -> {Cons f0'0 = _x} (! return {f0'0})
| _chk -> (! {[@expl:elim Cons] match _x with
| Cons _ -> true
| _ -> false
end}
any) ]
predicate resolve_T (_1: t_T)
predicate resolve_List_T (_1: t_List_T)
predicate resolve_tup2_T_List_T [@inline:trivial] (_1: tup2_T_List_T) = resolve_T _1.f0 /\ resolve_List_T _1.f1
meta "rewrite_def" predicate resolve_tup2_T_List_T
predicate resolve_Box_tup2_T_List_T_Global [@inline:trivial] (_1: tup2_T_List_T) = resolve_tup2_T_List_T _1
meta "rewrite_def" predicate resolve_Box_tup2_T_List_T_Global
axiom resolve_axiom [@rewrite]: forall x: t_List_T [resolve_List_T x]. resolve_List_T x
= match x with
| Nil -> true
| Cons x0 -> resolve_Box_tup2_T_List_T_Global x0
end
predicate resolve_refmut_List_T [@inline:trivial] (_1: MutBorrow.t t_List_T) = _1.final = _1.current
meta "rewrite_def" predicate resolve_refmut_List_T
meta "compute_max_steps" 1000000
meta "select_lsinst" "all"
let rev_T (l: MutBorrow.t t_List_T) (return (x: ())) =
{[@stop_split] [@expl:rev 'l' type invariant] inv_refmut_List_T l}
(! bb0
[ bb0 = s0
[ s0 = [ &old_l <- l ] s1
| s1 = [ &prev <- Nil ] s2
| s2 = [ &_10 <- Nil ] s3
| s3 = MutBorrow.borrow_mut <t_List_T> {l.current}
(fun (_bor: MutBorrow.t t_List_T) ->
[ &_9 <- _bor ] -{inv_List_T _bor.final}-
[ &l <- { l with current = _bor.final } ] s4)
[ _ck -> (! {[@expl:type invariant] inv_List_T l.current} any) ]
| s4 = replace_List_T {_9} {_10} (fun (_x: t_List_T) -> [ &head <- _x ] s5)
| s5 = bb3 ]
| bb3 = bb3
[ bb3 = {[@expl:inferred invariant: type invariant] inv_List_T prev}
{[@expl:inferred invariant: type invariant] inv_List_T head}
{[@expl:loop invariant] rev_append_T head prev = rev_append_T old_l.current (Nil)}
(! s0)
[ s0 = any [ br0 -> {head = Nil} (! bb18) | br1 (x0: tup2_T_List_T) -> {head = Cons x0} (! bb6) ] ]
[ bb6 = s0
[ s0 = elim_Cons {head} (fun (r0: tup2_T_List_T) -> [ &curr <- r0 ] s1)
| s1 = [ &next <- curr.f1 ] s2
| s2 = [ &curr <- { curr with f1 = prev } ] s3
| s3 = [ &_22 <- Cons curr ] s4
| s4 = [ &prev <- _22 ] s5
| s5 = [ &head <- next ] s6
| s6 = bb3 ] ] ]
| bb18 = s0
[ s0 = s1
[ _ck -> (! {[@expl:type invariant] match head with
| Cons x -> inv_Box_tup2_T_List_T_Global x
| _ -> true
end}
any) ]
| s1 = -{match head with
| Cons x -> resolve_Box_tup2_T_List_T_Global x
| _ -> true
end}-
s2
| s2 = s3 [ _ck -> (! {[@expl:type invariant] inv_List_T l.current} any) ]
| s3 = -{resolve_List_T l.current}- s4
| s4 = [ &l <- { l with current = prev } ] s5
| s5 = s6 [ _ck -> (! {[@expl:type invariant] inv_refmut_List_T l} any) ]
| s6 = -{resolve_refmut_List_T l}- s7
| s7 = return {_ret} ] ]
[ & _ret: () = Any.any_l ()
| & l: MutBorrow.t t_List_T = l
| & old_l: MutBorrow.t t_List_T = Any.any_l ()
| & prev: t_List_T = Any.any_l ()
| & head: t_List_T = Any.any_l ()
| & _9: MutBorrow.t t_List_T = Any.any_l ()
| & _10: t_List_T = Any.any_l ()
| & curr: tup2_T_List_T = Any.any_l ()
| & next: t_List_T = Any.any_l ()
| & _22: t_List_T = Any.any_l () ])
[ return (result: ()) -> {[@stop_split] [@expl:rev ensures] l.final = rev_append_T l.current (Nil)}
(! return {result}) ]
end