-
Notifications
You must be signed in to change notification settings - Fork 1
/
psci_rsi.v
49 lines (43 loc) · 1.5 KB
/
psci_rsi.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
Require Import RefProofDeps.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import Constants.
Require Import CommonLib.
Require Import RefTactics.
Require Import PSCI.Spec.
Require Import AbsAccessor.Spec.
Require Import PSCIHandler.Specs.psci_rsi.
Require Import PSCIHandler.LowSpecs.psci_rsi.
Require Import PSCIHandler.RefProof.RefRel.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Local Opaque Z.add Z.mul Z.div Z.shiftl Z.shiftr Z.land Z.lor.
Section Refine.
Hint Unfold
set_psci_result_x0_spec
set_psci_result_forward_psci_call_spec
.
Lemma psci_rsi_spec_exists:
forall habd habd' labd rec function_id arg0 arg1 arg2
(Hspec: psci_rsi_spec rec function_id arg0 arg1 arg2 habd = Some habd')
(Hrel: relate_RData habd labd),
exists labd', psci_rsi_spec0 rec function_id arg0 arg1 arg2 labd = Some labd' /\ relate_RData habd' labd'.
Proof.
Local Opaque
psci_version_spec
psci_cpu_suspend_spec
psci_cpu_off_spec
psci_cpu_on_spec
psci_affinity_info_spec
psci_system_off_spec
psci_system_reset_spec
psci_features_spec.
intros. inv Hrel. destruct rec.
unfold psci_rsi_spec, psci_rsi_spec0 in *.
autounfold in *.
hsimpl_hyp Hspec; inv Hspec; repeat destruct_con; repeat destruct_dis; grewrite; simpl;
repeat (extract_if; [bool_rel;omega|grewrite]);
try solve[eexists; split; [reflexivity|constructor;reflexivity]].
Qed.
End Refine.