update code_proof

Makefile

@@ -492,7 +492,6 @@ VFILES:=proof/RelaxedMemory/weakenedWDRF/PageTable.v\
   proof/RealmSyncHandler/Specs/handle_sysreg_access_trap.v\
   proof/RealmSyncHandler/LowSpecs/handle_sysreg_access_trap.v\
   proof/RealmSyncHandler/Code/handle_sysreg_access_trap.v\
-  proof/RealmSyncHandler/RefProof/handle_realm_rsi.v\
   proof/RealmSyncHandler/CodeProof/handle_realm_rsi.v\
   proof/RealmSyncHandler/Specs/handle_realm_rsi.v\
   proof/RealmSyncHandler/LowSpecs/handle_realm_rsi.v\

_CoqProject

@@ -485,7 +485,6 @@ proof/RealmSyncHandler/Code/handle_realm_rsi.v
 proof/RealmSyncHandler/LowSpecs/handle_realm_rsi.v
 proof/RealmSyncHandler/Specs/handle_realm_rsi.v
 proof/RealmSyncHandler/CodeProof/handle_realm_rsi.v
-proof/RealmSyncHandler/RefProof/handle_realm_rsi.v
 proof/RealmSyncHandler/Code/handle_sysreg_access_trap.v
 proof/RealmSyncHandler/LowSpecs/handle_sysreg_access_trap.v
 proof/RealmSyncHandler/Specs/handle_sysreg_access_trap.v

proof/CommonLib.v

@@ -600,6 +600,10 @@ Qed.
 Hypothesis lor_leN_if:
   forall a b N (Hpa: 0 <= a) (Hpb: 0 <= b)  (Hab: a + b <= N), Z.lor a b <= N.
 
+Hypothesis or_le_64:
+  forall a b (Ha: 0 <= a) (Ha': a <= 18446744073709551615) (Hb: 0 <= b) (Hb': b <= 18446744073709551615),
+    Z.lor a b <= 18446744073709551615.
+
 (* Add 0 <= a *)
 Hypothesis shiftl_leN_if:
   forall a b N (Hpa: 0 <= a) (Ha: a * 281474976710656 <= N) (Hb1: 0 <= b) (Hb2: b <= 48), Z.shiftl a b <= N.
@@ -909,6 +913,20 @@ Ltac simpl_hyp H :=
 Ltac hsimpl_hyp H :=
   repeat (simpl_hyp H; contra).
 
+Ltac solve_func64 val :=
+  try unfold Monad.bind; try unfold ret; simpl;
+  match goal with
+  | [|- match ?v with | Some _ => _ | None => None end = _] =>
+      replace v with (Some (VZ64 (Int64.unsigned (Int64.repr val))))
+  end.
+
+Ltac solve_func val :=
+  try unfold Monad.bind; try unfold ret; simpl;
+  match goal with
+  | [|- match ?v with | Some _ => _ | None => None end = _] =>
+      replace v with (Some (Int.unsigned (Int.repr val)))
+  end.
+
 Ltac despec exp :=
   simpl in *; srewrite; contra;
   let Hcond := fresh "cond" in

proof/PSCIAux2/RefProof/system_off_reboot.v

@@ -70,7 +70,10 @@ Section Refine.
     }
     exploit H; try eapply C13. simpl. omega.
     intros (d'' & Hd'' & Hi & Hdeq); rewrite Hd''. grewrite. simpl.
-    eexists; split. reflexivity. constructor. reflexivity.
+    replace ((0 <=? g_rec_idx (gro (gs (share labd)) @ z0)) &&
+         (g_rec_idx (gro (gs (share labd)) @ z0) <=? 18446744073709551615)) with true.
+    eexists; split. reflexivity. constructor.
+    admit. admit.
   Qed.
 
 End Refine.

proof/RefTactics.v

@@ -317,10 +317,6 @@ Ltac simpl_hgoals :=
 Ltac construct_relate :=
   constructor; simpl; autounfold with Replay; simpl; grewrite; try assumption; try reflexivity; simpl_hgoals.
 
-Hypothesis or_le_64:
-  forall a b (Ha: 0 <= a) (Ha': a <= 18446744073709551615) (Hb: 0 <= b) (Hb': b <= 18446744073709551615),
-    Z.lor a b <= 18446744073709551615.
-
 Ltac simpl_query_oracle :=
   repeat match goal with
           | H:query_oracle ?d = Some ?d' |- _ => try unfold query_oracle; unfold query_oracle in H; autounfold in H; repeat simpl_hyp H; inv H; simpl in *

proof/TableAux2/CodeProof/table_fold.v

@@ -83,6 +83,42 @@ Section CodeProof.
                                                  (Tcons Tptr (Tcons tulong Tnil)) tvoid cc_default).
     Local Opaque granule_refcount_dec_spec.
 
+   Lemma table_fold_body_correct:
+      forall m d d' env le table_base table_offset level g_tbl_base g_tbl_offset res
+             (Henv: env = PTree.empty _)
+             (Hinv: high_level_invariant d)
+             (HPTtable: PTree.get _table le = Some (Vptr table_base (Int.repr table_offset)))
+             (HPTlevel: PTree.get _level le = Some (Vlong level))
+             (HPTg_tbl: PTree.get _g_tbl le = Some (Vptr g_tbl_base (Int.repr g_tbl_offset)))
+             (Hspec: table_fold_spec0 (table_base, table_offset) (VZ64 (Int64.unsigned level)) (g_tbl_base, g_tbl_offset) d = Some (d', VZ64 (Int64.unsigned res))),
+           exists le', (exec_stmt ge env le ((m, d): mem) table_fold_body E0 le' (m, d') (Out_return (Some (Vlong res, tulong)))).
+    Proof.
+      solve_code_proof Hspec table_fold_body.
+      - eexists; solve_proof_low.
+      - eexists; solve_proof_low.
+        rewrite C8. solve_func64 z2. reflexivity.
+        symmetry. sstep. assumption. somega.
+        rewrite C10. sstep. reflexivity. somega.
+      - eexists; solve_proof_low.
+        rewrite C8. solve_func64 z2. reflexivity.
+        symmetry. sstep. assumption. somega.
+        solve_func z3. reflexivity.
+        symmetry. sstep. assumption. somega.
+        solve_proof_low. simpl.
+        solve_proof_low.
+        apply or_le_64. somega. somega. somega. somega.
+        simpl. repeat big_vcgen. rewrite C15. rewrite H1. solve_proof_low.
+      - eexists; solve_proof_low.
+        rewrite C8. solve_func64 z2. reflexivity.
+        symmetry. sstep. assumption. somega.
+        solve_func z3. reflexivity.
+        symmetry. sstep. assumption. somega.
+        solve_proof_low. simpl.
+        solve_proof_low.
+        simpl. repeat big_vcgen.
+        simpl. rewrite H1. solve_proof_low.
+    Qed.
+
   End BodyProof.
 
 End CodeProof.

proof/TableAux3/CodeProof/.#table_create_aux.v

@@ -0,0 +1 @@
+ubuntu@ip-172-31-21-86.2439:1661966326

proof/TableAux3/CodeProof/table_create_aux.v

@@ -137,6 +137,57 @@ Section CodeProof.
                                        (Tcons Tptr (Tcons Tptr (Tcons tulong (Tcons tulong Tnil)))) tvoid cc_default).
     Local Opaque link_table_spec.
 
+    Lemma table_create_aux_body_correct:
+      forall m d d' env le g_rd_base g_rd_offset g_llt_base g_llt_offset g_rtt_base g_rtt_offset llt_pte ll_table_base ll_table_offset level index map_addr rtt_addr
+             (Henv: env = PTree.empty _)
+             (Hinv: high_level_invariant d)
+             (HPTg_rd: PTree.get _g_rd le = Some (Vptr g_rd_base (Int.repr g_rd_offset)))
+             (HPTg_llt: PTree.get _g_llt le = Some (Vptr g_llt_base (Int.repr g_llt_offset)))
+             (HPTg_rtt: PTree.get _g_rtt le = Some (Vptr g_rtt_base (Int.repr g_rtt_offset)))
+             (HPTllt_pte: PTree.get _llt_pte le = Some (Vlong llt_pte))
+             (HPTll_table: PTree.get _ll_table le = Some (Vptr ll_table_base (Int.repr ll_table_offset)))
+             (HPTlevel: PTree.get _level le = Some (Vlong level))
+             (HPTindex: PTree.get _index le = Some (Vlong index))
+             (HPTmap_addr: PTree.get _map_addr le = Some (Vlong map_addr))
+             (HPTrtt_addr: PTree.get _rtt_addr le = Some (Vlong rtt_addr))
+             (Hspec: table_create_aux_spec0 (g_rd_base, g_rd_offset) (g_llt_base, g_llt_offset) (g_rtt_base, g_rtt_offset) (VZ64 (Int64.unsigned llt_pte)) (ll_table_base, ll_table_offset) (VZ64 (Int64.unsigned level)) (VZ64 (Int64.unsigned index)) (VZ64 (Int64.unsigned map_addr)) (VZ64 (Int64.unsigned rtt_addr)) d = Some d'),
+           exists le', (exec_stmt ge env le ((m, d): mem) table_create_aux_body E0 le' (m, d') Out_normal).
+    Proof.
+      solve_code_proof Hspec table_create_aux_body.
+      - eexists; solve_proof_low.
+        rewrite C6. assumption.
+      - eexists; solve_proof_low.
+        rewrite C7. assumption.
+      - eexists. vcgen. vcgen. vcgen. solve_proof_low.
+        vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low.
+        solve_proof_low. solve_proof_low. solve_proof_low.
+        solve_proof_low. solve_proof_low.
+        vcgen. vcgen. vcgen. solve_proof_low. solve_proof_low. solve_proof_low.
+        solve_proof_low. solve_proof_low. solve_proof_low.
+        vcgen. vcgen. vcgen. solve_proof_low.
+        rewrite C8. destruct zeq; try omega. solve_proof_low.
+        reflexivity. solve_proof_low. solve_proof_low.
+      - eexists. vcgen. vcgen. vcgen. solve_proof_low.
+        vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low.
+        solve_proof_low. solve_proof_low. solve_proof_low.
+        solve_proof_low. solve_proof_low.
+        vcgen. vcgen. vcgen. solve_proof_low. solve_proof_low. solve_proof_low.
+        solve_proof_low. solve_proof_low. solve_proof_low.
+        vcgen. vcgen. vcgen. solve_proof_low.
+        rewrite C9. destruct zeq; try omega. solve_proof_low.
+        reflexivity. solve_proof_low. solve_proof_low.
+      - eexists. vcgen. vcgen. vcgen. solve_proof_low.
+        vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low.
+        solve_proof_low. solve_proof_low. solve_proof_low.
+        solve_proof_low. solve_proof_low.
+        vcgen. vcgen. vcgen. solve_proof_low. solve_proof_low. solve_proof_low.
+        solve_proof_low. solve_proof_low. solve_proof_low.
+        vcgen. vcgen. vcgen. solve_proof_low.
+        solve_proof_low.
+        Grab Existential Variables.
+        assumption.
+    Qed.
+
   End BodyProof.
 
 End CodeProof.

proof/TableDataOpsIntro/CodeProof/data_create.v

@@ -182,6 +182,74 @@ Section CodeProof.
                                            (Tcons Tptr Tnil) tvoid cc_default).
     Local Opaque granule_unlock_spec.
 
+
+    Lemma data_create_body_correct:
+      forall m d d' env le g_rd_base g_rd_offset data_addr map_addr g_data_base g_data_offset g_src_base g_src_offset res
+             (Henv: env = PTree.empty _)
+             (Hinv: high_level_invariant d)
+             (HPTg_rd: PTree.get _g_rd le = Some (Vptr g_rd_base (Int.repr g_rd_offset)))
+             (HPTdata_addr: PTree.get _data_addr le = Some (Vlong data_addr))
+             (HPTmap_addr: PTree.get _map_addr le = Some (Vlong map_addr))
+             (HPTg_data: PTree.get _g_data le = Some (Vptr g_data_base (Int.repr g_data_offset)))
+             (HPTg_src: PTree.get _g_src le = Some (Vptr g_src_base (Int.repr g_src_offset)))
+             (Hspec: data_create_spec0 (g_rd_base, g_rd_offset) (VZ64 (Int64.unsigned data_addr)) (VZ64 (Int64.unsigned map_addr)) (g_data_base, g_data_offset) (g_src_base, g_src_offset) d = Some (d', VZ64 (Int64.unsigned res))),
+           exists le', (exec_stmt ge env le ((m, d): mem) data_create_body E0 le' (m, d') (Out_return (Some (Vlong res, tulong)))).
+    Proof.
+      solve_code_proof Hspec data_create_body.
+      -  eexists. solve_proof_low.
+         rewrite <- H1. simpl. somega.
+      - eexists. solve_proof_low.
+        rewrite <- H1. simpl. somega.
+      - eexists. repeat big_vcgen.
+        rewrite <- H1. simpl. somega.
+        rewrite <- H1. simpl. somega. somega.
+        solve_func64 z1. reflexivity. symmetry. solve_proof_low.
+        solve_func z2.  reflexivity. symmetry. sstep. assumption. somega.
+        rewrite <- H1. solve_proof_low. somega. somega. somega.
+        simpl.
+        repeat big_vcgen.
+        solve_func64 z5. reflexivity. symmetry. solve_proof_low.
+        solve_proof_low. somega. somega. somega. somega. somega.
+        simpl. repeat big_vcgen.
+        somega.
+        assert(ns_buffer_read_data_spec 0 (p6, z6) r2 = Some (r3, Int.unsigned (Int.repr 0))).
+        sstep. assumption. somega. eassumption.
+        solve_proof_low.
+        simpl.
+        repeat big_vcgen.
+        simpl. repeat vcgen.
+        reflexivity.
+        simpl. big_vcgen. repeat vcgen.
+        discriminate.
+        reflexivity.
+        simpl. repeat vcgen.
+        simpl. repeat vcgen.
+        simpl. repeat vcgen.
+      - eexists. repeat big_vcgen.
+        somega.
+        solve_func64 z1. reflexivity. symmetry. solve_proof_low.
+        solve_func z2.  reflexivity. symmetry. sstep. assumption. somega.
+        solve_proof_low.
+        simpl. repeat big_vcgen.
+        solve_func64 z5. reflexivity. symmetry. solve_proof_low.
+        solve_proof_low. somega. somega. somega. somega. somega. somega. somega.
+        somega.
+        simpl. repeat big_vcgen.
+        simpl. somega.
+        assert(ns_buffer_read_data_spec (Int64.unsigned res) (p6, z6) r2 = Some (r3, Int.unsigned (Int.repr z7))).
+        sstep. assumption. somega. eassumption. somega. somega.
+        solve_proof_low. somega. somega. somega.
+        simpl. repeat big_vcgen.
+        unfold Int64.or. repeat sstep. simpl in C34. assumption.
+        somega. apply or_le_64. omega. omega. somega. somega. somega. somega.
+        simpl. repeat vcgen.
+        somega. reflexivity.
+        simpl. repeat vcgen. somega. reflexivity.
+        simpl. repeat vcgen.
+        simpl. repeat vcgen. somega. reflexivity.
+        simpl. repeat vcgen. somega.
+    Qed.
+
   End BodyProof.
 
 End CodeProof.

proof/TableDataOpsIntro/CodeProof/table_destroy.v

@@ -147,6 +147,56 @@ Section CodeProof.
                                          (Tcons Tptr Tnil) tvoid cc_default).
     Local Opaque buffer_unmap_spec.
 
+    Lemma table_destroy_body_correct:
+      forall m d d' env le g_rd_base g_rd_offset map_addr rtt_addr level res
+             (Henv: env = PTree.empty _)
+             (Hinv: high_level_invariant d)
+             (HPTg_rd: PTree.get _g_rd le = Some (Vptr g_rd_base (Int.repr g_rd_offset)))
+             (HPTmap_addr: PTree.get _map_addr le = Some (Vlong map_addr))
+             (HPTrtt_addr: PTree.get _rtt_addr le = Some (Vlong rtt_addr))
+             (HPTlevel: PTree.get _level le = Some (Vlong level))
+             (Hspec: table_destroy_spec0 (g_rd_base, g_rd_offset) (VZ64 (Int64.unsigned map_addr)) (VZ64 (Int64.unsigned rtt_addr)) (VZ64 (Int64.unsigned level)) d = Some (d', VZ64 (Int64.unsigned res))),
+           exists le', (exec_stmt ge env le ((m, d): mem) table_destroy_body E0 le' (m, d') (Out_return (Some (Vlong res, tulong)))).
+    Proof.
+      solve_code_proof Hspec table_destroy_body.
+      - eexists; solve_proof_low.
+      - eexists; solve_proof_low.
+        unfold cast_int_long. rewrite <- H1.
+        solve_proof_low.
+      - eexists; solve_proof_low.
+        unfold cast_int_long. rewrite <- H1.
+        solve_proof_low.
+      - rewrite <- H1 in *.
+        simpl_func C31.
+      - eexists; repeat big_vcgen.
+        solve_func64 z1. reflexivity.
+        symmetry. solve_proof_low.
+        solve_func z2. reflexivity.
+        symmetry. sstep. assumption. somega.
+        solve_proof_low. simpl.
+        repeat big_vcgen.
+        idtac. solve_func64 z5. reflexivity.
+        symmetry. sstep. assumption. somega.
+        solve_func z6. reflexivity.
+        symmetry. sstep. sstep. assumption. somega. somega.
+        simpl. solve_proof_low. simpl.
+        repeat big_vcgen. somega.
+        rewrite C22. rewrite C24. reflexivity.
+        simpl. somega. somega.
+        solve_func z8. reflexivity.
+        symmetry. sstep. assumption. somega.
+        solve_proof_low.
+        simpl. solve_proof_low.
+        simpl. repeat big_vcgen.
+        reflexivity.
+        simpl. repeat big_vcgen.
+        reflexivity.
+        simpl. repeat big_vcgen.
+        reflexivity.
+        somega.
+        simpl. repeat big_vcgen.
+    Qed.
+
   End BodyProof.
 
 End CodeProof.

proof/TableDataOpsIntro/CodeProof/table_map.v

@@ -128,6 +128,91 @@ Section CodeProof.
                                            (Tcons Tptr Tnil) tvoid cc_default).
     Local Opaque granule_unlock_spec.
 
+  Lemma table_map_body_correct:
+      forall m d d' env le g_rd_base g_rd_offset map_addr level res
+             (Henv: env = PTree.empty _)
+             (Hinv: high_level_invariant d)
+             (HPTg_rd: PTree.get _g_rd le = Some (Vptr g_rd_base (Int.repr g_rd_offset)))
+             (HPTmap_addr: PTree.get _map_addr le = Some (Vlong map_addr))
+             (HPTlevel: PTree.get _level le = Some (Vlong level))
+             (Hspec: table_map_spec0 (g_rd_base, g_rd_offset) (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) table_map_body E0 le' (m, d') (Out_return (Some (Vlong res, tulong)))).
+    Proof.
+      solve_code_proof Hspec table_map_body.
+      - eexists; solve_proof_low.
+      - eexists; solve_proof_low.
+        unfold cast_int_long. rewrite <- H1.
+        solve_proof_low.
+      - eexists; solve_proof_low.
+      - eexists; solve_proof_low.
+        unfold cast_int_long. rewrite <- H1.
+        solve_proof_low.
+      - eexists; solve_proof_low.
+        unfold cast_int_long. rewrite <- H1.
+        solve_proof_low.
+      - eexists. repeat big_vcgen.
+        rewrite C25. eassumption.
+        solve_func64 z1. reflexivity.
+        symmetry. sstep. assumption. somega.
+        solve_func z2. reflexivity.
+        symmetry. sstep. assumption. somega.
+        solve_proof_low. simpl.
+        repeat big_vcgen.
+        solve_func64 z5. reflexivity.
+        symmetry. sstep. assumption. somega.
+        rewrite <- H1.
+        replace (negb (Int.eq (Int.repr 0) Int.zero)) with false by reflexivity.
+        repeat big_vcgen.
+        solve_proof_low.
+        simpl. repeat big_vcgen.
+        simpl. repeat big_vcgen.
+        reflexivity.
+        simpl. repeat big_vcgen.
+        reflexivity.
+        simpl. repeat big_vcgen.
+        rewrite H1. solve_proof_low.
+      - eexists. repeat big_vcgen.
+        solve_func64 z1. reflexivity.
+        symmetry. sstep. assumption. somega.
+        solve_func z2. reflexivity.
+        symmetry. sstep. assumption. somega.
+        solve_proof_low. simpl.
+        repeat big_vcgen.
+        solve_func64 z5. reflexivity.
+        symmetry. sstep. assumption. somega.
+        rewrite <- H1.
+        replace (negb (Int.eq (Int.repr 0) Int.zero)) with false by reflexivity.
+        repeat big_vcgen.
+        solve_proof_low.
+        simpl. repeat big_vcgen.
+        simpl. repeat big_vcgen.
+        reflexivity.
+        simpl. repeat big_vcgen.
+        reflexivity.
+        simpl. repeat big_vcgen.
+        rewrite H1. solve_proof_low.
+      - eexists. repeat big_vcgen. somega.
+        solve_func64 z1. reflexivity.
+        symmetry. sstep. assumption. somega.
+        solve_func z2. reflexivity.
+        symmetry. sstep. assumption. somega.
+        solve_proof_low. simpl. somega. somega. somega.
+        simpl. repeat big_vcgen.
+        solve_func64 z5. reflexivity.
+        symmetry. sstep. assumption. somega.
+        solve_proof_low. simpl. solve_proof_low.
+        simpl. repeat big_vcgen. reflexivity.
+        simpl.
+        replace (negb (Int.eq (Int.repr 0) Int.zero)) with false by reflexivity.
+        repeat big_vcgen. solve_proof_low. somega.
+        simpl. solve_proof_low.
+        somega. somega. solve_proof_low. reflexivity.
+        solve_proof_low. simpl. reflexivity. solve_proof_low.
+        simpl. unfold cast_int_long. solve_proof_low.
+        Grab Existential Variables.
+        assumption.
+    Qed.
+
   End BodyProof.
 
 End CodeProof.