generated_spec.v 6.55 KB
Newer Older
Michael Sammler's avatar
Michael Sammler committed
1
From refinedc.typing Require Import typing.
2
From refinedc.examples.queue Require Import generated_code.
Michael Sammler's avatar
Michael Sammler committed
3
4
Set Default Proof Using "Type".

5
(* Generated from [examples/queue.c]. *)
Michael Sammler's avatar
Michael Sammler committed
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
Section spec.
  Context `{!typeG Σ} `{!globalG Σ}.

  (* Inlined code. *)

  Definition alloc_initialized := initialized "allocator_state" ().

  (* Definition of type [queue_elem]. *)
  Definition queue_elem_rec : (type * type -d> typeO)  (type * type -d> typeO) := (λ self patt__,
    let ty := patt__.1 in
    let cont := patt__.2 in
    (&own (
      struct struct_queue_elem [@{type}
        (&own (ty)) ;
        (cont)
      ]
    ))
  )%I.
  Typeclasses Opaque queue_elem_rec.

  Global Instance queue_elem_rec_ne : Contractive queue_elem_rec.
  Proof. solve_type_proper. Qed.

  Definition queue_elem (cont : type) : rtype := {|
    rty_type := type;
    rty r__ := fixp queue_elem_rec (r__, cont)
  |}.

  Lemma queue_elem_unfold (cont : type) (ty : type) :
    (ty @ queue_elem cont)%I @{type} (
      (&own (
        struct struct_queue_elem [@{type}
          (&own (ty)) ;
          (cont)
        ]
      ))
    )%I.
  Proof. by rewrite {1}/with_refinement/=fixp_unfold. Qed.


  Global Program Instance queue_elem_rmovable (cont : type) : RMovable (queue_elem cont) :=
    {| rmovable 'ty := movable_eq _ _ (queue_elem_unfold cont ty) |}.
  Next Obligation. solve_ty_layout_eq. Qed.

  Global Instance queue_elem_simplify_hyp_place_inst l_ β_ (cont : type) (ty : type) :
    SimplifyHypPlace l_ β_ (ty @ queue_elem cont)%I (Some 100%N) :=
    λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (queue_elem_unfold _ _)).
  Global Instance queue_elem_simplify_goal_place_inst l_ β_ (cont : type) (ty : type) :
    SimplifyGoalPlace l_ β_ (ty @ queue_elem cont)%I (Some 100%N) :=
    λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (queue_elem_unfold _ _)).

  Global Program Instance queue_elem_simplify_hyp_val_inst v_ (cont : type) (ty : type) :
    SimplifyHypVal v_ (ty @ queue_elem cont)%I (Some 100%N) :=
    λ T, i2p (simplify_hyp_val_eq v_ _ _ (queue_elem_unfold _ _) T _).
  Next Obligation. done. Qed.
  Global Program Instance queue_elem_simplify_goal_val_inst v_ (cont : type) (ty : type) :
    SimplifyGoalVal v_ (ty @ queue_elem cont)%I (Some 100%N) :=
    λ T, i2p (simplify_goal_val_eq v_ _ _ (queue_elem_unfold _ _) T _).
  Next Obligation. done. Qed.

  (* Definition of type [queue]. *)
  Definition queue_rec : ((list type) -d> typeO)  ((list type) -d> typeO) := (λ self tys,
    (&own (
      tyexists (λ p : loc,
      struct struct_queue [@{type}
        (tyfold ((λ ty x, ty @ queue_elem x) <$> tys) (singleton_place (p))) ;
        (p @ (&own (null)))
      ])
    ))
  )%I.
  Typeclasses Opaque queue_rec.

  Global Instance queue_rec_ne : Contractive queue_rec.
  Proof. solve_type_proper. Qed.

  Definition queue : rtype := {|
    rty_type := (list type);
    rty r__ := fixp queue_rec r__
  |}.

  Lemma queue_unfold (tys : list type) :
    (tys @ queue)%I @{type} (
      (&own (
        tyexists (λ p : loc,
        struct struct_queue [@{type}
          (tyfold ((λ ty x, ty @ queue_elem x) <$> tys) (singleton_place (p))) ;
          (p @ (&own (null)))
        ])
      ))
    )%I.
  Proof. by rewrite {1}/with_refinement/=fixp_unfold. Qed.


  Global Program Instance queue_rmovable : RMovable queue :=
    {| rmovable 'tys := movable_eq _ _ (queue_unfold tys) |}.
  Next Obligation. solve_ty_layout_eq. Qed.

  Global Instance queue_simplify_hyp_place_inst l_ β_ (tys : list type) :
    SimplifyHypPlace l_ β_ (tys @ queue)%I (Some 100%N) :=
    λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (queue_unfold _)).
  Global Instance queue_simplify_goal_place_inst l_ β_ (tys : list type) :
    SimplifyGoalPlace l_ β_ (tys @ queue)%I (Some 100%N) :=
    λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (queue_unfold _)).

  Global Program Instance queue_simplify_hyp_val_inst v_ (tys : list type) :
    SimplifyHypVal v_ (tys @ queue)%I (Some 100%N) :=
    λ T, i2p (simplify_hyp_val_eq v_ _ _ (queue_unfold _) T _).
  Next Obligation. done. Qed.
  Global Program Instance queue_simplify_goal_val_inst v_ (tys : list type) :
    SimplifyGoalVal v_ (tys @ queue)%I (Some 100%N) :=
    λ T, i2p (simplify_goal_val_eq v_ _ _ (queue_unfold _) T _).
  Next Obligation. done. Qed.

  (* Type definitions. *)

  (* Specifications for function [alloc]. *)
  Definition type_of_alloc :=
123
124
    fn( size : nat; (size @ (int (size_t))); size + 16  max_int size_t  (8 | size)  (alloc_initialized))
        () : (), (&own (uninit (Layout size 3))); True.
Michael Sammler's avatar
Michael Sammler committed
125
126
127

  (* Specifications for function [free]. *)
  Definition type_of_free :=
128
    fn( size : nat; (size @ (int (size_t))), (&own (uninit (Layout size 3))); (alloc_initialized)  (8 | size))
Michael Sammler's avatar
Michael Sammler committed
129
130
131
132
        () : (), (void); True.

  (* Specifications for function [alloc_array]. *)
  Definition type_of_alloc_array :=
133
134
    fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))); size * n + 16  max_int size_t  (8 | size)  (alloc_initialized))
        () : (), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); True.
Michael Sammler's avatar
Michael Sammler committed
135
136
137

  (* Specifications for function [free_array]. *)
  Definition type_of_free_array :=
138
    fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); size * n  max_int size_t  (8 | size)  (alloc_initialized))
Michael Sammler's avatar
Michael Sammler committed
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
        () : (), (void); True.

  (* Specifications for function [init_queue]. *)
  Definition type_of_init_queue :=
    fn( () : (); (alloc_initialized))
        () : (), (([]) @ (queue)); True.

  (* Specifications for function [is_empty]. *)
  Definition type_of_is_empty :=
    fn( (p, tys) : loc * (list type); (p @ (&own ((tys) @ (queue)))); True)
        () : (), ((bool_decide (tys  [])) @ (boolean (bool_it))); (p ◁ₗ ((tys) @ (queue))).

  (* Specifications for function [enqueue]. *)
  Definition type_of_enqueue :=
    fn( (p, tys, ty) : loc * (list type) * type; (p @ (&own ((tys) @ (queue)))), (&own (ty)); (alloc_initialized))
        () : (), (void); (p ◁ₗ ((tys ++ [ty]) @ (queue))).

  (* Specifications for function [dequeue]. *)
  Definition type_of_dequeue :=
    fn( (p, tys) : loc * (list type); (p @ (&own ((tys) @ (queue)))); (alloc_initialized))
        () : (), ((maybe2 cons tys) @ (optionalO (λ patt__,
        let ty := patt__.1 in
        let _ := patt__.2 in
        &own (ty) ) null)); (p ◁ₗ ((tail tys) @ (queue))).
End spec.

Typeclasses Opaque queue_elem_rec.
Typeclasses Opaque queue_rec.