VIA/proof/PendingCheck/RefProof/check_pending_ptimers.v at main · columbia/VIA · GitHub

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
Require Import RefProofDeps.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import Constants.
Require Import CommonLib.
Require Import RefTactics.
Require Import AbsAccessor.Spec.
Require Import PendingCheckAux.Spec.
Require Import RVIC4.Spec.
Require Import PendingCheck.Specs.check_pending_ptimers.
Require Import PendingCheck.LowSpecs.check_pending_ptimers.
Require Import PendingCheck.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
       get_rec_g_rec_spec
       sysreg_read_spec
       check_timer_became_asserted_spec
       get_rec_ptimer_spec
       granule_lock_spec
       sysreg_write_spec
       get_rec_sysregs_spec
       set_rec_sysregs_spec
       set_rec_ptimer_asserted_spec
       rvic_set_pending_spec
       get_rec_rvic_spec
       granule_unlock_spec
    .

  Lemma check_pending_ptimers_spec_exists:
    forall habd habd'  labd rec
           (Hspec: check_pending_ptimers_spec rec habd = Some habd')
            (Hrel: relate_RData habd labd),
    exists labd', check_pending_ptimers_spec0 rec labd = Some labd' /\ relate_RData habd' labd'.
  Proof.
    Local Opaque ptr_eq.
    intros. destruct Hrel. inv id_rdata. destruct rec.
    unfold check_pending_ptimers_spec, check_pending_ptimers_spec0 in *.
    repeat autounfold in *. simpl in *.
    hsimpl_hyp Hspec; inv Hspec; simpl_query_oracle; extract_prop_dec;
      repeat destruct_con; bool_rel; simpl in *; srewrite; repeat simpl_update_reg;
        repeat (simpl_htarget; grewrite; simpl in * );
        try solve[repeat (solve_bool_range; grewrite); eexists; split; [reflexivity|constructor; reflexivity]].
    solve_bool_range; grewrite. solve_bool_range; grewrite.
    extract_if. apply andb_true_iff; split; bool_rel. somega. apply or_le_64; somega. grewrite.
    unfold ref_accessible in *. simpl. srewrite.
    simpl_hyp C15; contra. grewrite.
    assert(0 <= 30 / 64 < 512) by (replace (30 / 64) with 0 by reflexivity; omega).
    repeat (grewrite; simpl_htarget; repeat simpl_update_reg; repeat simpl_field; simpl).
    repeat (solve_bool_range; grewrite).
    repeat (grewrite; simpl_htarget; repeat simpl_update_reg; repeat simpl_field; simpl).
    eexists; split; [reflexivity|constructor; try reflexivity].
    repeat swap_fields; repeat simpl_field. rewrite <- C14, <- Prop0; repeat simpl_field.
    reflexivity.
  Qed.

End Refine.