-
Notifications
You must be signed in to change notification settings - Fork 1
/
validate_realm_params.v
52 lines (48 loc) · 1.35 KB
/
validate_realm_params.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
Require Import SpecDeps.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import Constants.
Require Import CommonLib.
Require Import AbsAccessor.Spec.
Local Open Scope Z_scope.
Section SpecLow.
Definition validate_realm_params_spec0 (adt: RData) : option Z64 :=
when' _base == get_realm_params_par_base_spec adt;
rely is_int64 _base;
when' _size == get_realm_params_par_size_spec adt;
rely is_int64 _size;
rely is_int64 (_base mod 4096);
if ((_base mod 4096) =? 0) then
rely is_int64 (_size mod 4096);
let _t'3 := ((_size mod 4096) =? 0) in
if _t'3 then
rely is_int64 (_base + _size);
let _t'4 := ((_base + _size) >? _base) in
if _t'4 then
when' _t'6 == max_ipa_size_spec adt;
rely is_int64 _t'6;
let _t'5 := ((_base + _size) <? _t'6) in
if _t'5 then
let _ret := 0 in
Some (VZ64 _ret)
else
let _ret := 1 in
Some (VZ64 _ret)
else
let _t'5 := 0 in
let _ret := 1 in
Some (VZ64 _ret)
else
let _t'4 := 0 in
let _t'5 := 0 in
let _ret := 1 in
Some (VZ64 _ret)
else
let _t'3 := 0 in
let _t'4 := 0 in
let _t'5 := 0 in
let _ret := 1 in
Some (VZ64 _ret)
.
End SpecLow.