generated_proof_free.v 1.48 KB
Newer Older
1
From refinedc.typing Require Import typing.
2
3
From refinedc.examples.paper_example_2_2 Require Import generated_code.
From refinedc.examples.paper_example_2_2 Require Import generated_spec.
4
5
6
From refinedc.examples.spinlock Require Import spinlock_def.
Set Default Proof Using "Type".

7
(* Generated from [examples/paper_example_2_2.c]. *)
8
9
10
11
12
13
14
15
Section proof_free.
  Context `{!typeG Σ} `{!globalG Σ}.
  Context `{!lockG Σ}.

  (* Typing proof for [free]. *)
  Lemma type_free :
     typed_function impl_free type_of_free.
  Proof.
16
    Open Scope printing_sugar.
17
    start_function "free" ([[s p] n]) => arg_list arg_data arg_sz local_cur local_entry.
18
19
20
    split_blocks ((
      <[ "#1" :=
         cp : loc,
21
         cs : gmultiset nat,
22
23
        arg_data ◁ₗ (&own (uninit (n))) 
        arg_sz ◁ₗ (n @ (int (size_t))) 
24
        local_entry ◁ₗ uninit void* 
25
        local_cur ◁ₗ (cp @ (&own (cs @ (chunks_t)))) 
26
        arg_list ◁ₗ (p @ (&own (wand (cp ◁ₗ ({[n]}  cs) @ chunks_t) (({[n]}  s) @ (chunks_t)))))
27
28
    ]> $
      
29
    )%I : gmap label (iProp Σ)) ((
30
      
31
    )%I : gmap label (iProp Σ)).
32
33
34
35
    - repeat liRStep; liShow.
      all: print_typesystem_goal "free" "#0".
    - repeat liRStep; liShow.
      all: print_typesystem_goal "free" "#1".
Michael Sammler's avatar
Michael Sammler committed
36
    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
37
38
39
40
    all: multiset_solver.
    all: print_sidecondition_goal "free".
  Qed.
End proof_free.