-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathsmc_rtt_unmap.v
112 lines (93 loc) · 5.7 KB
/
smc_rtt_unmap.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
Require Import CodeProofDeps.
Require Import Ident.
Require Import Constants.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import CommonLib.
Require Import TableAux.Spec.
Require Import AbsAccessor.Spec.
Require Import TableDataOpsIntro.Spec.
Require Import TableDataOpsRef3.Spec.
Require Import TableDataOpsRef3.Layer.
Require Import TableDataSMC.Code.smc_rtt_unmap.
Require Import TableDataSMC.LowSpecs.smc_rtt_unmap.
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) :=
_validate_table_commands ↦ gensem validate_table_commands_spec
⊕ _find_lock_granule ↦ gensem find_lock_granule_spec
⊕ _is_null ↦ gensem is_null_spec
⊕ _table_unmap ↦ gensem table_unmap_spec
⊕ _table_unmap3 ↦ gensem table_unmap3_spec
⊕ _granule_unlock ↦ gensem granule_unlock_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_validate_table_commands: block.
Hypothesis h_validate_table_commands_s : Genv.find_symbol ge _validate_table_commands = Some b_validate_table_commands.
Hypothesis h_validate_table_commands_p : Genv.find_funct_ptr ge b_validate_table_commands
= Some (External (EF_external _validate_table_commands
(signature_of_type (Tcons tulong (Tcons tulong (Tcons tulong (Tcons tulong (Tcons tulong Tnil))))) tuint cc_default))
(Tcons tulong (Tcons tulong (Tcons tulong (Tcons tulong (Tcons tulong Tnil))))) tuint cc_default).
Local Opaque validate_table_commands_spec.
Variable b_find_lock_granule: block.
Hypothesis h_find_lock_granule_s : Genv.find_symbol ge _find_lock_granule = Some b_find_lock_granule.
Hypothesis h_find_lock_granule_p : Genv.find_funct_ptr ge b_find_lock_granule
= Some (External (EF_external _find_lock_granule
(signature_of_type (Tcons tulong (Tcons tulong Tnil)) Tptr cc_default))
(Tcons tulong (Tcons tulong Tnil)) Tptr cc_default).
Local Opaque find_lock_granule_spec.
Variable b_is_null: block.
Hypothesis h_is_null_s : Genv.find_symbol ge _is_null = Some b_is_null.
Hypothesis h_is_null_p : Genv.find_funct_ptr ge b_is_null
= Some (External (EF_external _is_null
(signature_of_type (Tcons Tptr Tnil) tuint cc_default))
(Tcons Tptr Tnil) tuint cc_default).
Local Opaque is_null_spec.
Variable b_table_unmap: block.
Hypothesis h_table_unmap_s : Genv.find_symbol ge _table_unmap = Some b_table_unmap.
Hypothesis h_table_unmap_p : Genv.find_funct_ptr ge b_table_unmap
= Some (External (EF_external _table_unmap
(signature_of_type (Tcons Tptr (Tcons tulong (Tcons tulong Tnil))) tulong cc_default))
(Tcons Tptr (Tcons tulong (Tcons tulong Tnil))) tulong cc_default).
Local Opaque table_unmap_spec.
Variable b_table_unmap3: block.
Hypothesis h_table_unmap3_s : Genv.find_symbol ge _table_unmap3 = Some b_table_unmap3.
Hypothesis h_table_unmap3_p : Genv.find_funct_ptr ge b_table_unmap3
= Some (External (EF_external _table_unmap3
(signature_of_type (Tcons Tptr (Tcons tulong (Tcons tulong Tnil))) tulong cc_default))
(Tcons Tptr (Tcons tulong (Tcons tulong Tnil))) tulong cc_default).
Local Opaque table_unmap3_spec.
Variable b_granule_unlock: block.
Hypothesis h_granule_unlock_s : Genv.find_symbol ge _granule_unlock = Some b_granule_unlock.
Hypothesis h_granule_unlock_p : Genv.find_funct_ptr ge b_granule_unlock
= Some (External (EF_external _granule_unlock
(signature_of_type (Tcons Tptr Tnil) tvoid cc_default))
(Tcons Tptr Tnil) tvoid cc_default).
Local Opaque granule_unlock_spec.
Lemma smc_rtt_unmap_body_correct:
forall m d d' env le rd_addr map_addr level res
(Henv: env = PTree.empty _)
(Hinv: high_level_invariant d)
(HPTrd_addr: PTree.get _rd_addr le = Some (Vlong rd_addr))
(HPTmap_addr: PTree.get _map_addr le = Some (Vlong map_addr))
(HPTlevel: PTree.get _level le = Some (Vlong level))
(Hspec: smc_rtt_unmap_spec0 (VZ64 (Int64.unsigned rd_addr)) (VZ64 (Int64.unsigned map_addr)) (VZ64 (Int64.unsigned level)) d = Some (d', VZ64 (Int64.unsigned res))),
exists le', (exec_stmt ge env le ((m, d): mem) smc_rtt_unmap_body E0 le' (m, d') (Out_return (Some (Vlong res, tulong)))).
Proof.
solve_code_proof Hspec smc_rtt_unmap_body; eexists; solve_proof_low.
Qed.
End BodyProof.
End CodeProof.