generated_proof_fsm_realloc_if_necessary.v 3.25 KB
Newer Older
Michael Sammler's avatar
Michael Sammler committed
1
From refinedc.typing Require Import typing.
2
3
From refinedc.examples.mutable_map Require Import generated_code.
From refinedc.examples.mutable_map Require Import generated_spec.
Michael Sammler's avatar
Michael Sammler committed
4
5
6
From refinedc.examples.mutable_map Require Import mutable_map_extra.
Set Default Proof Using "Type".

7
(* Generated from [examples/mutable_map.c]. *)
Michael Sammler's avatar
Michael Sammler committed
8
9
10
11
Section proof_fsm_realloc_if_necessary.
  Context `{!typeG Σ} `{!globalG Σ}.

  (* Typing proof for [fsm_realloc_if_necessary]. *)
12
13
  Lemma type_fsm_realloc_if_necessary (compute_min_count free_array fsm_init fsm_insert : loc) :
    compute_min_count ◁ᵥ compute_min_count @ function_ptr type_of_compute_min_count -
Michael Sammler's avatar
Michael Sammler committed
14
15
16
    free_array ◁ᵥ free_array @ function_ptr type_of_free_array -
    fsm_init ◁ᵥ fsm_init @ function_ptr type_of_fsm_init -
    fsm_insert ◁ᵥ fsm_insert @ function_ptr type_of_fsm_insert -
17
    typed_function (impl_fsm_realloc_if_necessary compute_min_count free_array fsm_init fsm_insert) type_of_fsm_realloc_if_necessary.
Michael Sammler's avatar
Michael Sammler committed
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
  Proof.
    start_function "fsm_realloc_if_necessary" ([[[m items] count] mp]) => arg_m local_i local_m2 local_new_len.
    split_blocks ((
      <[ "#3" :=
         i : nat,
         items2 : list item_ref,
         count2 : nat,
        local_new_len ◁ₗ uninit (it_layout size_t) 
        local_i ◁ₗ (i @ (int (size_t))) 
        arg_m ◁ₗ (m @ (&own (struct (struct_fixed_size_map) [@{type} &own (array (struct_item) (replicate i (uninit struct_item) ++ (drop i items `at_type` item))) ; int (size_t) ; (length items) @ (int (size_t)) ]))) 
        local_m2 ◁ₗ ((fsm_copy_entries items i, items2, count2) @ (fixed_size_map)) 
        count + length items - i < count2 
        i <= length items 
        0 < count 
        length items * 2 <= length items2 
        fsm_invariant mp items 
34
        struct_item.(ly_size) * length items  max_int size_t
Michael Sammler's avatar
Michael Sammler committed
35
36
37
38
39
40
41
42
    ]> $
      <[ "#11" :=
        arg_m ◁ₗ (m @ (&own ((mp, items, count) @ (fixed_size_map)))) 
        local_i ◁ₗ uninit (it_layout size_t) 
        local_m2 ◁ₗ uninit (layout_of struct_fixed_size_map) 
        local_new_len ◁ₗ uninit (it_layout size_t)
    ]> $
      
43
    )%I : gmap label (iProp Σ)) ((
Michael Sammler's avatar
Michael Sammler committed
44
      
45
    )%I : gmap label (iProp Σ)).
Michael Sammler's avatar
Michael Sammler committed
46
47
48
49
50
51
52
53
54
55
56
57
    - repeat liRStep; liShow.
      all: print_typesystem_goal "fsm_realloc_if_necessary" "#0".
    - repeat liRStep; liShow.
      all: print_typesystem_goal "fsm_realloc_if_necessary" "#3".
    - repeat liRStep; liShow.
      all: print_typesystem_goal "fsm_realloc_if_necessary" "#11".
    Unshelve. all: prepare_sideconditions; normalize_and_simpl_goal; try solve_goal.
    all: try by eexists (length items); rewrite /shelve_hint; split_and?; rewrite ?drop_ge; solve_goal.
    all: try match goal with | H : fsm_invariant ?mp2 ?items2 |- fsm_invariant ?mp1 ?items1 => have ->: mp1 = mp2; [|done] end.
    all: try by apply: fsm_copy_entries_not_add; solve_goal.
    all: try by apply: fsm_copy_entries_add; solve_goal.
    all: try by apply: fsm_copy_entries_id; solve_goal.
Michael Sammler's avatar
Michael Sammler committed
58
    all: try by apply list_subequiv_split; [solve_goal|]; normalize_and_simpl_goal; try solve_goal; f_equal; solve_goal.
Michael Sammler's avatar
Michael Sammler committed
59
60
61
    all: print_sidecondition_goal "fsm_realloc_if_necessary".
  Qed.
End proof_fsm_realloc_if_necessary.