-
Notifications
You must be signed in to change notification settings - Fork 2
/
table_fold.v
124 lines (106 loc) · 5.86 KB
/
table_fold.v
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
Require Import CodeProofDeps.
Require Import Ident.
Require Import Constants.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import CommonLib.
Require Import AbsAccessor.Spec.
Require Import TableAux.Spec.
Require Import TableAux.Layer.
Require Import TableAux2.Code.table_fold.
Require Import TableAux2.LowSpecs.table_fold.
Local Open Scope Z_scope.
Section CodeProof.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Let L : compatlayer (cdata RData) :=
_pgte_read ↦ gensem pgte_read_spec
⊕ _entry_to_phys ↦ gensem entry_to_phys_spec
⊕ _assert_cond ↦ gensem assert_cond_spec
⊕ _table_maps_block ↦ gensem table_maps_block_spec
⊕ _granule_refcount_dec ↦ gensem granule_refcount_dec_spec
.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section BodyProof.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv) (STENCIL_MATCHES: stencil_matches sc ge).
Variable b_pgte_read: block.
Hypothesis h_pgte_read_s : Genv.find_symbol ge _pgte_read = Some b_pgte_read.
Hypothesis h_pgte_read_p : Genv.find_funct_ptr ge b_pgte_read
= Some (External (EF_external _pgte_read
(signature_of_type (Tcons Tptr (Tcons tulong Tnil)) tulong cc_default))
(Tcons Tptr (Tcons tulong Tnil)) tulong cc_default).
Local Opaque pgte_read_spec.
Variable b_entry_to_phys: block.
Hypothesis h_entry_to_phys_s : Genv.find_symbol ge _entry_to_phys = Some b_entry_to_phys.
Hypothesis h_entry_to_phys_p : Genv.find_funct_ptr ge b_entry_to_phys
= Some (External (EF_external _entry_to_phys
(signature_of_type (Tcons tulong (Tcons tulong Tnil)) tulong cc_default))
(Tcons tulong (Tcons tulong Tnil)) tulong cc_default).
Local Opaque entry_to_phys_spec.
Variable b_assert_cond: block.
Hypothesis h_assert_cond_s : Genv.find_symbol ge _assert_cond = Some b_assert_cond.
Hypothesis h_assert_cond_p : Genv.find_funct_ptr ge b_assert_cond
= Some (External (EF_external _assert_cond
(signature_of_type (Tcons tuint Tnil) tvoid cc_default))
(Tcons tuint Tnil) tvoid cc_default).
Local Opaque assert_cond_spec.
Variable b_table_maps_block: block.
Hypothesis h_table_maps_block_s : Genv.find_symbol ge _table_maps_block = Some b_table_maps_block.
Hypothesis h_table_maps_block_p : Genv.find_funct_ptr ge b_table_maps_block
= Some (External (EF_external _table_maps_block
(signature_of_type (Tcons Tptr (Tcons tulong (Tcons tulong Tnil))) tuint cc_default))
(Tcons Tptr (Tcons tulong (Tcons tulong Tnil))) tuint cc_default).
Local Opaque table_maps_block_spec.
Variable b_granule_refcount_dec: block.
Hypothesis h_granule_refcount_dec_s : Genv.find_symbol ge _granule_refcount_dec = Some b_granule_refcount_dec.
Hypothesis h_granule_refcount_dec_p : Genv.find_funct_ptr ge b_granule_refcount_dec
= Some (External (EF_external _granule_refcount_dec
(signature_of_type (Tcons Tptr (Tcons tulong Tnil)) tvoid cc_default))
(Tcons Tptr (Tcons tulong Tnil)) tvoid cc_default).
Local Opaque granule_refcount_dec_spec.
Lemma table_fold_body_correct:
forall m d d' env le table_base table_offset level g_tbl_base g_tbl_offset res
(Henv: env = PTree.empty _)
(Hinv: high_level_invariant d)
(HPTtable: PTree.get _table le = Some (Vptr table_base (Int.repr table_offset)))
(HPTlevel: PTree.get _level le = Some (Vlong level))
(HPTg_tbl: PTree.get _g_tbl le = Some (Vptr g_tbl_base (Int.repr g_tbl_offset)))
(Hspec: table_fold_spec0 (table_base, table_offset) (VZ64 (Int64.unsigned level)) (g_tbl_base, g_tbl_offset) d = Some (d', VZ64 (Int64.unsigned res))),
exists le', (exec_stmt ge env le ((m, d): mem) table_fold_body E0 le' (m, d') (Out_return (Some (Vlong res, tulong)))).
Proof.
solve_code_proof Hspec table_fold_body.
- eexists; solve_proof_low.
- eexists; solve_proof_low.
rewrite C8. solve_func64 z2. reflexivity.
symmetry. sstep. assumption. somega.
rewrite C10. sstep. reflexivity. somega.
- eexists; solve_proof_low.
rewrite C8. solve_func64 z2. reflexivity.
symmetry. sstep. assumption. somega.
solve_func z3. reflexivity.
symmetry. sstep. assumption. somega.
solve_proof_low. simpl.
solve_proof_low.
apply or_le_64. somega. somega. somega. somega.
simpl. repeat big_vcgen. rewrite C15. rewrite H1. solve_proof_low.
- eexists; solve_proof_low.
rewrite C8. solve_func64 z2. reflexivity.
symmetry. sstep. assumption. somega.
solve_func z3. reflexivity.
symmetry. sstep. assumption. somega.
solve_proof_low. simpl.
solve_proof_low.
simpl. repeat big_vcgen.
simpl. rewrite H1. solve_proof_low.
Qed.
End BodyProof.
End CodeProof.