-
Notifications
You must be signed in to change notification settings - Fork 1
/
psci_cpu_on_target.v
139 lines (117 loc) · 7.98 KB
/
psci_cpu_on_target.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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
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 PSCIAux.Spec.
Require Import PSCIAux.Layer.
Require Import PSCIAux2.Code.psci_cpu_on_target.
Require Import PSCIAux2.LowSpecs.psci_cpu_on_target.
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) :=
_get_rec_runnable ↦ gensem get_rec_runnable_spec
⊕ _buffer_unmap ↦ gensem buffer_unmap_spec
⊕ _granule_unlock ↦ gensem granule_unlock_spec
⊕ _set_psci_result_x0 ↦ gensem set_psci_result_x0_spec
⊕ _psci_reset_rec ↦ gensem psci_reset_rec_spec
⊕ _set_rec_pc ↦ gensem set_rec_pc_spec
⊕ _set_rec_runnable ↦ gensem set_rec_runnable_spec
⊕ _set_psci_result_forward_psci_call ↦ gensem set_psci_result_forward_psci_call_spec
⊕ _set_psci_result_forward_x1 ↦ gensem set_psci_result_forward_x1_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_get_rec_runnable: block.
Hypothesis h_get_rec_runnable_s : Genv.find_symbol ge _get_rec_runnable = Some b_get_rec_runnable.
Hypothesis h_get_rec_runnable_p : Genv.find_funct_ptr ge b_get_rec_runnable
= Some (External (EF_external _get_rec_runnable
(signature_of_type (Tcons Tptr Tnil) tuint cc_default))
(Tcons Tptr Tnil) tuint cc_default).
Local Opaque get_rec_runnable_spec.
Variable b_buffer_unmap: block.
Hypothesis h_buffer_unmap_s : Genv.find_symbol ge _buffer_unmap = Some b_buffer_unmap.
Hypothesis h_buffer_unmap_p : Genv.find_funct_ptr ge b_buffer_unmap
= Some (External (EF_external _buffer_unmap
(signature_of_type (Tcons Tptr Tnil) tvoid cc_default))
(Tcons Tptr Tnil) tvoid cc_default).
Local Opaque buffer_unmap_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.
Variable b_set_psci_result_x0: block.
Hypothesis h_set_psci_result_x0_s : Genv.find_symbol ge _set_psci_result_x0 = Some b_set_psci_result_x0.
Hypothesis h_set_psci_result_x0_p : Genv.find_funct_ptr ge b_set_psci_result_x0
= Some (External (EF_external _set_psci_result_x0
(signature_of_type (Tcons tulong Tnil) tvoid cc_default))
(Tcons tulong Tnil) tvoid cc_default).
Local Opaque set_psci_result_x0_spec.
Variable b_psci_reset_rec: block.
Hypothesis h_psci_reset_rec_s : Genv.find_symbol ge _psci_reset_rec = Some b_psci_reset_rec.
Hypothesis h_psci_reset_rec_p : Genv.find_funct_ptr ge b_psci_reset_rec
= Some (External (EF_external _psci_reset_rec
(signature_of_type (Tcons Tptr (Tcons Tptr Tnil)) tvoid cc_default))
(Tcons Tptr (Tcons Tptr Tnil)) tvoid cc_default).
Local Opaque psci_reset_rec_spec.
Variable b_set_rec_pc: block.
Hypothesis h_set_rec_pc_s : Genv.find_symbol ge _set_rec_pc = Some b_set_rec_pc.
Hypothesis h_set_rec_pc_p : Genv.find_funct_ptr ge b_set_rec_pc
= Some (External (EF_external _set_rec_pc
(signature_of_type (Tcons Tptr (Tcons tulong Tnil)) tvoid cc_default))
(Tcons Tptr (Tcons tulong Tnil)) tvoid cc_default).
Local Opaque set_rec_pc_spec.
Variable b_set_rec_runnable: block.
Hypothesis h_set_rec_runnable_s : Genv.find_symbol ge _set_rec_runnable = Some b_set_rec_runnable.
Hypothesis h_set_rec_runnable_p : Genv.find_funct_ptr ge b_set_rec_runnable
= Some (External (EF_external _set_rec_runnable
(signature_of_type (Tcons Tptr (Tcons tuint Tnil)) tvoid cc_default))
(Tcons Tptr (Tcons tuint Tnil)) tvoid cc_default).
Local Opaque set_rec_runnable_spec.
Variable b_set_psci_result_forward_psci_call: block.
Hypothesis h_set_psci_result_forward_psci_call_s : Genv.find_symbol ge _set_psci_result_forward_psci_call = Some b_set_psci_result_forward_psci_call.
Hypothesis h_set_psci_result_forward_psci_call_p : Genv.find_funct_ptr ge b_set_psci_result_forward_psci_call
= Some (External (EF_external _set_psci_result_forward_psci_call
(signature_of_type (Tcons tuint Tnil) tvoid cc_default))
(Tcons tuint Tnil) tvoid cc_default).
Local Opaque set_psci_result_forward_psci_call_spec.
Variable b_set_psci_result_forward_x1: block.
Hypothesis h_set_psci_result_forward_x1_s : Genv.find_symbol ge _set_psci_result_forward_x1 = Some b_set_psci_result_forward_x1.
Hypothesis h_set_psci_result_forward_x1_p : Genv.find_funct_ptr ge b_set_psci_result_forward_x1
= Some (External (EF_external _set_psci_result_forward_x1
(signature_of_type (Tcons tulong Tnil) tvoid cc_default))
(Tcons tulong Tnil) tvoid cc_default).
Local Opaque set_psci_result_forward_x1_spec.
Lemma psci_cpu_on_target_body_correct:
forall m d d' env le g_target_rec_base g_target_rec_offset target_rec_base target_rec_offset rec_base rec_offset entry_point_address target_cpu
(Henv: env = PTree.empty _)
(Hinv: high_level_invariant d)
(HPTg_target_rec: PTree.get _g_target_rec le = Some (Vptr g_target_rec_base (Int.repr g_target_rec_offset)))
(HPTtarget_rec: PTree.get _target_rec le = Some (Vptr target_rec_base (Int.repr target_rec_offset)))
(HPTrec: PTree.get _rec le = Some (Vptr rec_base (Int.repr rec_offset)))
(HPTentry_point_address: PTree.get _entry_point_address le = Some (Vlong entry_point_address))
(HPTtarget_cpu: PTree.get _target_cpu le = Some (Vlong target_cpu))
(Hspec: psci_cpu_on_target_spec0 (g_target_rec_base, g_target_rec_offset) (target_rec_base, target_rec_offset) (rec_base, rec_offset) (VZ64 (Int64.unsigned entry_point_address)) (VZ64 (Int64.unsigned target_cpu)) d = Some d'),
exists le', (exec_stmt ge env le ((m, d): mem) psci_cpu_on_target_body E0 le' (m, d') Out_normal).
Proof.
solve_code_proof Hspec psci_cpu_on_target_body; eexists; solve_proof_low.
Qed.
End BodyProof.
End CodeProof.