From 3b18f763733453e6bdeec56f41f5ffb233086943 Mon Sep 17 00:00:00 2001 From: Xupeng Li Date: Wed, 31 Aug 2022 19:02:52 +0000 Subject: [PATCH] update code_proof --- Makefile | 1 - _CoqProject | 1 - proof/CommonLib.v | 18 + .../CodeProof/restore_ns_state_sysreg_state.v | 353 +++++++++++++ .../CodeProof/restore_sysreg_state.v | 475 ++++++++++++++++++ proof/PSCIAux2/RefProof/system_off_reboot.v | 5 +- proof/RefTactics.v | 4 - proof/TableAux2/CodeProof/table_fold.v | 36 ++ .../TableAux3/CodeProof/.#table_create_aux.v | 1 + proof/TableAux3/CodeProof/table_create_aux.v | 51 ++ .../TableDataOpsIntro/CodeProof/data_create.v | 68 +++ .../CodeProof/table_destroy.v | 50 ++ proof/TableDataOpsIntro/CodeProof/table_map.v | 85 ++++ .../TableDataOpsIntro/CodeProof/table_unmap.v | 85 ++++ 14 files changed, 1226 insertions(+), 7 deletions(-) create mode 120000 proof/TableAux3/CodeProof/.#table_create_aux.v diff --git a/Makefile b/Makefile index 435aec0..3377054 100644 --- a/Makefile +++ b/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\ diff --git a/_CoqProject b/_CoqProject index 80e3448..0b8d32f 100644 --- a/_CoqProject +++ b/_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 diff --git a/proof/CommonLib.v b/proof/CommonLib.v index d13864e..46fea3c 100644 --- a/proof/CommonLib.v +++ b/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 diff --git a/proof/CtxtSwitchAux/CodeProof/restore_ns_state_sysreg_state.v b/proof/CtxtSwitchAux/CodeProof/restore_ns_state_sysreg_state.v index fd69c81..b696b17 100644 --- a/proof/CtxtSwitchAux/CodeProof/restore_ns_state_sysreg_state.v +++ b/proof/CtxtSwitchAux/CodeProof/restore_ns_state_sysreg_state.v @@ -55,6 +55,359 @@ Section CodeProof. (Tcons tuint (Tcons tulong Tnil)) tvoid cc_default). Local Opaque sysreg_write_spec. + Lemma restore_ns_state_sysreg_state_body_correct: + forall m d d' env le + (Henv: env = PTree.empty _) + (Hinv: high_level_invariant d) + (Hspec: restore_ns_state_sysreg_state_spec0 d = Some d'), + exists le', (exec_stmt ge env le ((m, d): mem) restore_ns_state_sysreg_state_body E0 le' (m, d') Out_normal). + Proof. + solve_code_proof Hspec restore_ns_state_sysreg_state_body. + eexists. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z0. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z2. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z4. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z6. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z8. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z10. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z12. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z14. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z16. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z18. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z20. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z22. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z24. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z26. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z28. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z30. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z32. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z34. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z36. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z38. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z40. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z42. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z44. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z46. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z48. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z50. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z52. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z54. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z56. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z58. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z60. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z62. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z64. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z66. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z68. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z70. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. + solve_func64 z72. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. big_vcgen. + solve_func64 z74. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + Qed. + End BodyProof. End CodeProof. diff --git a/proof/CtxtSwitchAux/CodeProof/restore_sysreg_state.v b/proof/CtxtSwitchAux/CodeProof/restore_sysreg_state.v index 39daaba..2a1e035 100644 --- a/proof/CtxtSwitchAux/CodeProof/restore_sysreg_state.v +++ b/proof/CtxtSwitchAux/CodeProof/restore_sysreg_state.v @@ -55,6 +55,481 @@ Section CodeProof. (Tcons tuint (Tcons tulong Tnil)) tvoid cc_default). Local Opaque sysreg_write_spec. + Lemma restore_sysreg_state_body_correct: + forall m d d' env le rec_base rec_offset + (Henv: env = PTree.empty _) + (Hinv: high_level_invariant d) + (HPTrec: PTree.get _rec le = Some (Vptr rec_base (Int.repr rec_offset))) + (Hspec: restore_sysreg_state_spec0 (rec_base, rec_offset) d = Some d'), + exists le', (exec_stmt ge env le ((m, d): mem) restore_sysreg_state_body E0 le' (m, d') Out_normal). + Proof. + solve_code_proof Hspec restore_sysreg_state_body. + eexists. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z0. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. big_vcgen. solve_func64 z2. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. big_vcgen. solve_func64 z4. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z6. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. big_vcgen. solve_func64 z8. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. big_vcgen. solve_func64 z10. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z12. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z14. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. + big_vcgen. solve_func64 z16. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z18. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z20. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z22. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. + big_vcgen. solve_func64 z24. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z26. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z28. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z30. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. + big_vcgen. solve_func64 z32. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z34. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z36. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z38. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. + big_vcgen. solve_func64 z40. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z42. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z44. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z46. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. + big_vcgen. solve_func64 z48. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z50. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z52. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z54. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. + big_vcgen. solve_func64 z56. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z58. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z60. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z62. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. + big_vcgen. solve_func64 z64. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. + big_vcgen. solve_func64 z66. reflexivity. + symmetry. sstep. assumption. somega. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. vcgen. + vcgen. vcgen. vcgen. vcgen. vcgen. solve_proof_low. + Qed. + End BodyProof. End CodeProof. diff --git a/proof/PSCIAux2/RefProof/system_off_reboot.v b/proof/PSCIAux2/RefProof/system_off_reboot.v index 6e96e44..bb1f49a 100644 --- a/proof/PSCIAux2/RefProof/system_off_reboot.v +++ b/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. diff --git a/proof/RefTactics.v b/proof/RefTactics.v index 8d7a8a5..d006b80 100644 --- a/proof/RefTactics.v +++ b/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 * diff --git a/proof/TableAux2/CodeProof/table_fold.v b/proof/TableAux2/CodeProof/table_fold.v index c6ea773..5e221bb 100644 --- a/proof/TableAux2/CodeProof/table_fold.v +++ b/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. diff --git a/proof/TableAux3/CodeProof/.#table_create_aux.v b/proof/TableAux3/CodeProof/.#table_create_aux.v new file mode 120000 index 0000000..95f8715 --- /dev/null +++ b/proof/TableAux3/CodeProof/.#table_create_aux.v @@ -0,0 +1 @@ +ubuntu@ip-172-31-21-86.2439:1661966326 \ No newline at end of file diff --git a/proof/TableAux3/CodeProof/table_create_aux.v b/proof/TableAux3/CodeProof/table_create_aux.v index cd8ff9e..87aee73 100644 --- a/proof/TableAux3/CodeProof/table_create_aux.v +++ b/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. diff --git a/proof/TableDataOpsIntro/CodeProof/data_create.v b/proof/TableDataOpsIntro/CodeProof/data_create.v index 5dc2966..42aaf00 100644 --- a/proof/TableDataOpsIntro/CodeProof/data_create.v +++ b/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. diff --git a/proof/TableDataOpsIntro/CodeProof/table_destroy.v b/proof/TableDataOpsIntro/CodeProof/table_destroy.v index 2a964ac..9815fb2 100644 --- a/proof/TableDataOpsIntro/CodeProof/table_destroy.v +++ b/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. diff --git a/proof/TableDataOpsIntro/CodeProof/table_map.v b/proof/TableDataOpsIntro/CodeProof/table_map.v index d7c1fbb..cbb0aa1 100644 --- a/proof/TableDataOpsIntro/CodeProof/table_map.v +++ b/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. diff --git a/proof/TableDataOpsIntro/CodeProof/table_unmap.v b/proof/TableDataOpsIntro/CodeProof/table_unmap.v index 361fad0..1d3c7ea 100644 --- a/proof/TableDataOpsIntro/CodeProof/table_unmap.v +++ b/proof/TableDataOpsIntro/CodeProof/table_unmap.v @@ -147,6 +147,91 @@ Section CodeProof. (Tcons Tptr Tnil) tvoid cc_default). Local Opaque granule_unlock_spec. + Lemma table_unmap_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_unmap_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_unmap_body E0 le' (m, d') (Out_return (Some (Vlong res, tulong)))). + Proof. + solve_code_proof Hspec table_unmap_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 C26. assumption. + 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. + 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. reflexivity. solve_proof_low. + unfold cast_int_long. solve_proof_low. + Grab Existential Variables. + assumption. + Qed. + End BodyProof. End CodeProof.