diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..ca16bab --- /dev/null +++ b/.gitignore @@ -0,0 +1,49 @@ +.*.aux +.*.d +*.a +*.cma +*.cmi +*.cmo +*.cmx +*.cmxa +*.cmxs +*.glob +*.ml.d +*.ml4.d +*.mlg.d +*.mli.d +*.mllib.d +*.mlpack.d +*.native +*.o +*.v.d +*.vio +*.vo +*.vok +*.vos +.coq-native +.csdp.cache +.lia.cache +.nia.cache +.nlia.cache +.nra.cache +csdp.cache +lia.cache +nia.cache +nlia.cache +nra.cache +native_compute_profile_*.data + +# generated timing files +*.timing.diff +*.v.after-timing +*.v.before-timing +*.v.timing +time-of-build-after.log +time-of-build-before.log +time-of-build-both.log +time-of-build-pretty.log +!lib/* +!lib/*/* +!lib/*/*/* +!lib/*/*/*/* diff --git a/proof/PSCIAux2/CodeProof/system_off_reboot.v b/proof/PSCIAux2/CodeProof/system_off_reboot.v index d1da624..1566c0f 100644 --- a/proof/PSCIAux2/CodeProof/system_off_reboot.v +++ b/proof/PSCIAux2/CodeProof/system_off_reboot.v @@ -137,7 +137,8 @@ Section CodeProof. (Tcons Tptr Tnil) tvoid cc_default). Local Opaque buffer_unmap_spec. - (* Lemma system_off_reboot_body_correct: + + Lemma system_off_reboot_body_correct: forall m d d' env le rec_base rec_offset (Henv: env = PTree.empty _) (Hinv: high_level_invariant d) @@ -145,8 +146,108 @@ Section CodeProof. (Hspec: system_off_reboot_spec0 (rec_base, rec_offset) d = Some d'), exists le', (exec_stmt ge env le ((m, d): mem) system_off_reboot_body E0 le' (m, d') Out_normal). Proof. - solve_code_proof Hspec system_off_reboot_body; eexists; solve_proof_low. - Qed. *) + solve_code_proof Hspec system_off_reboot_body. + destruct p, p0, p1, p3. + add_int64 C1 z0; try somega. + remember (Int64.repr z0) as ZZ. + + get_loop_body. clear_hyp. + set (Hloop := C10). simpl; solve_proof_low. + remember + (PTree.set _i (Vlong (Int64.repr 0)) + (PTree.set _rec_list (Vptr p2 (Int.repr z4)) + (PTree.set _t'5 (Vptr p2 (Int.repr z4)) + (PTree.set _g (Vptr p1 (Int.repr z3)) + (PTree.set _t'4 (Vptr p1 (Int.repr z3)) + (PTree.set _idx (Vlong ZZ) + (PTree.set _t'3 (Vlong ZZ) + (PTree.set _g_rd (Vptr p0 (Int.repr z2)) + (PTree.set _t'2 (Vptr p0 (Int.repr z2)) + (PTree.set _g_rec (Vptr p (Int.repr z)) + (PTree.set _t'1 (Vptr p (Int.repr z)) le))))))))))) as le_loop. + remember 512 as num. + set (P := fun le0 m0 => m0 = (m, r2) /\ le0 = le_loop). + set (Q := fun (le0: temp_env) m0 => m0 = (m, r3) /\ le0 ! _rec_list = Some (Vptr p2 (Int.repr z4))). + set (Inv := fun le0 m0 n => exists i' adt', + system_off_reboot_loop0 (Z.to_nat (num - n)) 0 z0 (p0, z2) (p2, z4) r2 = + Some (adt', Int64.unsigned i') /\ Int64.unsigned i' = num - n /\ + m0 = (m, adt') /\ 0 <= n /\ n <= num /\ le0 ! _i = Some (Vlong i') /\ + le0 ! _g_rd = Some (Vptr p0 (Int.repr z2)) /\ + le0 ! _rec_list = Some (Vptr p2 (Int.repr z4)) /\ + le0 ! _idx = Some (Vlong (Int64.repr z0))). + assert(loop_succ: forall N, Z.of_nat N <= num -> exists i' adt', + system_off_reboot_loop0 (Z.to_nat (num - Z.of_nat N)) 0 z0 (p0, z2) (p2, z4) r2 = + Some (adt', Int64.unsigned i')). + { add_int64 Hloop z1; try somega. + induction N. rewrite Z.sub_0_r. rewrite Hloop. intros. repeat eexists; reflexivity. + intros. erewrite loop_ind_sub1 in IHN; try omega. + rewrite Nat2Z.inj_succ, succ_plus_1 in H. + assert(Hcc: Z.of_nat N <= num) by omega. + apply IHN in Hcc. destruct Hcc as (? & ? & Hnext). + Local Opaque Z.of_nat. simpl in Hnext. clear Heqle_loop. + simpl_func Hnext; try add_int64' z5; try somega; repeat eexists. } + assert (T: LoopProofSimpleWhile.t (external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops L) cond body ge (PTree.empty _) P Q). + { apply LoopProofSimpleWhile.make with (W:=Z) (lt:=fun z1 z2 => (0 <= z2 /\ z1 < z2)) (I:=Inv). + - apply Zwf_well_founded. + - unfold P, Inv. intros ? ? CC. destruct CC as [CC1 CC2]. + rewrite CC2 in *. exists num. + replace (num - num) with 0 by omega. simpl. + exists (Int64.repr 0). exists r2. + rewrite Heqnum. rewrite Heqle_loop. rewrite HeqZZ. + repeat eexists; first [reflexivity|assumption|solve_proof_low]. + - intros ? ? ? I. unfold Inv in I. destruct I as (? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ?). + set (Hnow := H). + rewrite Heqbody, Heqcond in *. + destruct (n >? 0) eqn:Hn; bool_rel. + + eexists. eexists. split_and. + * solve_proof_low. + * solve_proof_low. + * intro CC. inversion CC. + * assert(Hlx: Z.of_nat (Z.to_nat (n-1)) <= num) by (rewrite Z2Nat.id; omega). + apply loop_succ in Hlx. rewrite Z2Nat.id in Hlx; try omega. + intro. destruct Hlx as (? & ? & Hnext). duplicate Hnext. + rewrite loop_nat_sub1 in Hnext; try somega. + simpl in Hnext. rewrite Hnow in Hnext. + autounfold in Hnext; repeat simpl_hyp Hnext; + repeat destruct_con; bool_rel; contra; inversion Hnext. + rewrite H11, H12 in *; eexists; eexists; split. + solve_proof_low. + exists (n-1); split. split; solve_proof_low. + solve_proof_low; unfold Inv; repeat eexists; first[eassumption|solve_proof_low]. + + destruct p4, p6. + rewrite H11, H12 in *; eexists; eexists; split. + solve_proof_low. + exists (n-1); split. split; solve_proof_low. + solve_proof_low; unfold Inv; repeat eexists; first[eassumption|solve_proof_low]. + + destruct p4. + rewrite H11, H12 in *; eexists; eexists; split. + solve_proof_low. + exists (n-1); split. split; solve_proof_low. + solve_proof_low; unfold Inv; repeat eexists; first[eassumption|solve_proof_low]. + + eexists. eexists. split_and. + * solve_proof_low. + * solve_proof_low. + * intro. unfold Q. + assert (n=0) by omega. clear Heqle_loop. subst. + sstep. rewrite Hloop in Hnow. inv Hnow. + split_and; first[reflexivity|solve_proof_low]. + somega. + * intro CC. inversion CC. } + assert (Pre: P le_loop (m, r2)) by (split; reflexivity). + pose proof (LoopProofSimpleWhile.termination _ _ _ _ _ _ T _ (m, r2) Pre) as LoopProof. + destruct LoopProof as (le' & m' & (exec & Post)). + unfold exec_stmt in exec. rewrite Heqle_loop in exec. + unfold Q in Post. destruct Post as (Post & Hle'). rewrite Post in exec. + eexists; solve_proof_low. + + match goal with + | [|- match ?v with Some _ => _ | None => None end = _] => + replace v with (Some (VZ64 (Int64.unsigned ZZ))) + end. + reflexivity. + Qed. End BodyProof. diff --git a/proof/PSCIAux2/LowSpecs/system_off_reboot.v b/proof/PSCIAux2/LowSpecs/system_off_reboot.v index bf93f02..6107ecd 100644 --- a/proof/PSCIAux2/LowSpecs/system_off_reboot.v +++ b/proof/PSCIAux2/LowSpecs/system_off_reboot.v @@ -39,6 +39,7 @@ Section SpecLow. when g_rec == get_rec_g_rec_spec rec adt; when g_rd == get_rec_g_rd_spec rec adt; when' idx == get_rec_rec_idx_spec rec adt; + rely is_int64 idx; when g == get_rec_g_rec_list_spec rec adt; when adt == granule_lock_spec g_rec adt; when adt == set_rec_runnable_spec rec 0 adt; @@ -47,9 +48,8 @@ Section SpecLow. match system_off_reboot_loop0 (Z.to_nat MAX_NUM_RECS) 0 idx g_rd rec_list adt with | Some (adt, i) => rely is_int64 i; - Some adt + buffer_unmap_spec rec_list adt | _ => None end. - End SpecLow. diff --git a/proof/RealmExitHandlerAux/CodeProof/handle_exception_sync.v b/proof/RealmExitHandlerAux/CodeProof/handle_exception_sync.v index 16b135e..f6df9fa 100644 --- a/proof/RealmExitHandlerAux/CodeProof/handle_exception_sync.v +++ b/proof/RealmExitHandlerAux/CodeProof/handle_exception_sync.v @@ -146,6 +146,92 @@ Section CodeProof. (Tcons Tptr (Tcons tulong Tnil)) tvoid cc_default). Local Opaque handle_data_abort_spec. + + Lemma handle_exception_sync_body_correct: + forall m d d' env le rec_base rec_offset res + (Henv: env = PTree.empty _) + (Hinv: high_level_invariant d) + (HPTrec: PTree.get _rec le = Some (Vptr rec_base (Int.repr rec_offset))) + (Hspec: handle_exception_sync_spec0 (rec_base, rec_offset) d = Some (d',Int.unsigned res)), + exists le', (exec_stmt ge env le ((m, d): mem) handle_exception_sync_body E0 le' (m, d') (Out_return (Some (Vint res, tuint)))). + Proof. + solve_code_proof Hspec handle_exception_sync_body. + - eexists; solve_proof_low. + - get_loop_body. clear_hyp. + set (Hloop := C9). simpl. solve_proof_low. + remember + (PTree.set _info (Vlong (Int64.repr (Z.land z0 (Z.lor 4227858432 65535)))) + (PTree.set _i (Vint res) + (PTree.set _ec (Vlong (Int64.repr (Z.land z0 4227858432))) + (PTree.set _esr (Vlong (Int64.repr z0)) (PTree.set _t'1 (Vlong (Int64.repr z0)) le))))) + as le_loop. + remember 7 as num. + set (P := fun le0 m0 => m0 = (m, r0) /\ le0 = le_loop). + set (Q := fun (le0: temp_env) m0 => m0 = (m, d')). + set (Inv := fun le0 m0 n => exists i' adt', + handle_exception_sync_loop0 (Z.to_nat (num - n)) + (Int.unsigned res) rec_base rec_offset r0 = + Some (Int.unsigned i', adt') /\ Int.unsigned i' = num - n /\ + m0 = (m, adt') /\ 0 <= n /\ n <= num /\ le0 ! _i = Some (Vint i') /\ + le0 ! _rec = Some (Vptr rec_base (Int.repr rec_offset))). + assert(loop_succ: forall N, Z.of_nat N <= num -> exists i' adt', + handle_exception_sync_loop0 (Z.to_nat (num - Z.of_nat N)) (Int.unsigned res) rec_base rec_offset r0 + = Some (Int.unsigned i', adt')). + { add_int Hloop z1; try somega. + induction N. rewrite Z.sub_0_r. rewrite Hloop. intros. repeat eexists; reflexivity. + intros. erewrite loop_ind_sub1 in IHN; try omega. + rewrite Nat2Z.inj_succ, succ_plus_1 in H. + assert(Hcc: Z.of_nat N <= num) by omega. + apply IHN in Hcc. destruct Hcc as (? & ? & Hnext). + Local Opaque Z.of_nat. simpl in Hnext. clear Heqle_loop. + simpl_func Hnext; try add_int' z; repeat eexists; try somega. } + assert (T: LoopProofSimpleWhile.t (external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops L) cond body ge (PTree.empty _) P Q). + { apply LoopProofSimpleWhile.make with (W:=Z) (lt:=fun z1 z2 => (0 <= z2 /\ z1 < z2)) (I:=Inv). + - apply Zwf_well_founded. + - unfold P, Inv. intros ? ? CC. destruct CC as [CC1 CC2]. + rewrite CC2 in *. exists num. + replace (num - num) with 0 by omega. simpl. add_int' 0; try somega. + rewrite Heqnum. rewrite Heqle_loop. + repeat eexists; first [reflexivity|assumption|solve_proof_low]. + - intros ? ? ? I. unfold Inv in I. destruct I as (? & ? & ? & ? & ? & ? & ? & ? & ?). + set (Hnow := H). + rewrite Heqbody, Heqcond in *. + destruct (n >? 0) eqn:Hn; bool_rel. + + eexists. eexists. split_and. + * solve_proof_low. + * solve_proof_low. + * intro CC. inversion CC. + * assert(Hlx: Z.of_nat (Z.to_nat (n-1)) <= num) by (rewrite Z2Nat.id; omega). + apply loop_succ in Hlx. rewrite Z2Nat.id in Hlx; try omega. + intro. destruct Hlx as (? & ? & Hnext). duplicate Hnext. + rewrite loop_nat_sub1 in Hnext; try somega. + simpl in Hnext. rewrite Hnow in Hnext. + autounfold in Hnext; repeat simpl_hyp Hnext; + repeat destruct_con; bool_rel; contra; inversion Hnext. + rewrite H9, H10 in *; eexists; eexists; split. solve_proof_low. + exists (n-1); split. split; solve_proof_low. + solve_proof_low; unfold Inv; repeat eexists; first[eassumption|solve_proof_low]. + + eexists. eexists. split_and. + * solve_proof_low. + * solve_proof_low. + * intro. unfold Q. + assert (n=0) by omega. clear Heqle_loop. subst. + sstep. rewrite Hloop in Hnow. inv Hnow. + split_and; first[reflexivity|solve_proof_low]. + * intro CC. inversion CC. } + assert (Pre: P le_loop (m, r0)) by (split; reflexivity). + pose proof (LoopProofSimpleWhile.termination _ _ _ _ _ _ T _ (m, r0) Pre) as LoopProof. + destruct LoopProof as (le' & m' & (exec & Post)). + unfold exec_stmt in exec. rewrite Heqle_loop in exec. + unfold Q in Post. rewrite Post in exec. + eexists; solve_proof_low. + - eexists; solve_proof_low. + - eexists; solve_proof_low. + - eexists; solve_proof_low. + - eexists; solve_proof_low. + - eexists; solve_proof_low. + Qed. + End BodyProof. End CodeProof. diff --git a/proof/RealmSyncHandler/CodeProof/handle_realm_rsi.v b/proof/RealmSyncHandler/CodeProof/handle_realm_rsi.v index 759432d..ecc7f7b 100644 --- a/proof/RealmSyncHandler/CodeProof/handle_realm_rsi.v +++ b/proof/RealmSyncHandler/CodeProof/handle_realm_rsi.v @@ -155,6 +155,20 @@ Section CodeProof. Tnil tulong cc_default). Local Opaque get_psci_result_forward_x3_spec. + 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. + Lemma handle_realm_rsi_body_correct: forall m d d' env le rec_base rec_offset res (Henv: env = PTree.empty _) @@ -163,7 +177,259 @@ Section CodeProof. (Hspec: handle_realm_rsi_spec0 (rec_base, rec_offset) d = Some (d',Int.unsigned res)), exists le', (exec_stmt ge env le ((m, d): mem) handle_realm_rsi_body E0 le' (m, d') (Out_return (Some (Vint res, tuint)))). Proof. - solve_code_proof Hspec handle_realm_rsi_body; eexists; solve_proof_low. + solve_code_proof Hspec handle_realm_rsi_body. + - eexists. repeat big_vcgen. + solve_func64 3355443200. reflexivity. + solve_func64 z2. reflexivity. + symmetry. sstep. assumption. somega. + solve_func64 z4. reflexivity. + symmetry. sstep. assumption. somega. + solve_func64 z6. reflexivity. + symmetry. sstep. assumption. somega. + solve_proof_low. somega. somega. simpl. + solve_proof_low. + - destruct_dis; bool_rel_all. omega. + + eexists. repeat big_vcgen. + solve_func64 z0. reflexivity. + symmetry. sstep. assumption. somega. + solve_func64 z2. reflexivity. + symmetry. sstep. assumption. somega. + solve_func64 z4. reflexivity. + symmetry. sstep. assumption. somega. + solve_func64 z6. reflexivity. + symmetry. sstep. assumption. somega. + solve_proof_low. somega. somega. simpl. + repeat big_vcgen. + solve_proof_low. simpl. + solve_proof_low. solve_proof_low. + solve_proof_low. simpl. solve_proof_low. + solve_proof_low. solve_proof_low. + simpl. + repeat big_vcgen. + somega. + solve_func64 z8. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. + solve_func64 z10. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. + solve_func64 z12. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. + solve_func64 z14. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. + solve_func 1. reflexivity. + solve_proof_low. simpl. + repeat big_vcgen. + solve_func64 z17. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. + solve_func64 z19. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. + solve_func64 z21. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. + unfold Swhile. + replace E0 with (E0 ** E0 ** E0) by reflexivity. + eapply exec_Sloop_loop. + solve_proof_low. econstructor. + eapply exec_Sskip. + replace E0 with (E0 ** E0 ** E0) by reflexivity. + eapply exec_Sloop_loop. + solve_proof_low. econstructor. + eapply exec_Sskip. + replace E0 with (E0 ** E0 ** E0) by reflexivity. + eapply exec_Sloop_loop. + solve_proof_low. econstructor. + eapply exec_Sskip. simpl. + eapply exec_Sloop_stop1. + eapply exec_Sseq_2. + solve_proof_low. red; intro T; inv T. + econstructor. + + eexists. repeat big_vcgen. + solve_func64 z0. reflexivity. + symmetry. sstep. assumption. somega. + solve_func64 z2. reflexivity. + symmetry. sstep. assumption. somega. + solve_func64 z4. reflexivity. + symmetry. sstep. assumption. somega. + solve_func64 z6. reflexivity. + symmetry. sstep. assumption. somega. + solve_proof_low. somega. somega. simpl. + repeat big_vcgen. + solve_proof_low. simpl. + solve_proof_low. destruct zlt. solve_proof_low. omega. + solve_proof_low. solve_proof_low. simpl. solve_proof_low. + solve_proof_low. solve_proof_low. + rewrite C32. destruct (zeq 1 0); [omega|]. + destruct zeq. inv e. + replace (Int.eq Int.one Int.zero) with false by reflexivity. + simpl. + repeat big_vcgen. + somega. + solve_func64 z8. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. + solve_func64 z10. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. + solve_func64 z12. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. + solve_func64 z14. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. + solve_func 1. reflexivity. + solve_proof_low. simpl. + repeat big_vcgen. + solve_func64 z17. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. + solve_func64 z19. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. + solve_func64 z21. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. + unfold Swhile. + replace E0 with (E0 ** E0 ** E0) by reflexivity. + eapply exec_Sloop_loop. + solve_proof_low. econstructor. + eapply exec_Sskip. + replace E0 with (E0 ** E0 ** E0) by reflexivity. + eapply exec_Sloop_loop. + solve_proof_low. econstructor. + eapply exec_Sskip. + replace E0 with (E0 ** E0 ** E0) by reflexivity. + eapply exec_Sloop_loop. + solve_proof_low. econstructor. + eapply exec_Sskip. simpl. + eapply exec_Sloop_stop1. + eapply exec_Sseq_2. + solve_proof_low. red; intro T; inv T. + econstructor. + - destruct_dis; bool_rel_all. omega. + + eexists. repeat big_vcgen. + solve_func64 z0. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_func64 z2. reflexivity. + symmetry. sstep. assumption. somega. + solve_func64 z4. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_func64 z6. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_proof_low. somega. somega. simpl. + repeat big_vcgen. + solve_proof_low. simpl. + solve_proof_low. solve_proof_low. + solve_proof_low. simpl. solve_proof_low. + solve_proof_low. solve_proof_low. + rewrite <- (Int.repr_unsigned res), <- H1. + replace (Int.eq (Int.repr 1) Int.zero) with false by reflexivity. + simpl. + repeat big_vcgen. + somega. + solve_func64 z8. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. somega. + solve_func64 z10. reflexivity. + symmetry. sstep. assumption. somega. + sstep. rewrite H1. eassumption. somega. somega. + solve_func64 z12. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. somega. + solve_func64 z14. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. somega. + solve_func z15. reflexivity. + symmetry. sstep. assumption. somega. + solve_proof_low. simpl. + solve_proof_low. + + eexists. repeat big_vcgen. + solve_func64 z0. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_func64 z2. reflexivity. + symmetry. sstep. assumption. somega. + solve_func64 z4. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_func64 z6. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_proof_low. somega. somega. simpl. + repeat big_vcgen. + solve_proof_low. simpl. + solve_proof_low. destruct zlt. solve_proof_low. omega. + solve_proof_low. solve_proof_low. simpl. solve_proof_low. + solve_proof_low. solve_proof_low. + destruct (zeq 1 0); [omega|]. + repeat big_vcgen. + somega. + solve_func64 z8. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. somega. + solve_func64 z10. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. somega. + solve_func64 z12. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. somega. + solve_func64 z14. reflexivity. + symmetry. sstep. assumption. somega. + sstep. eassumption. somega. somega. + solve_func z15. reflexivity. + symmetry. sstep. assumption. somega. + solve_proof_low. simpl. + solve_proof_low. + - repeat destruct_dis; bool_rel; try omega. + eexists. repeat big_vcgen. + solve_func64 z0. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_func64 z2. reflexivity. + symmetry. sstep. assumption. somega. + solve_func64 z4. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_func64 z6. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_proof_low. somega. somega. simpl. + repeat big_vcgen. + solve_proof_low. simpl. + solve_proof_low. solve_proof_low. + solve_proof_low. simpl. solve_proof_low. + solve_proof_low. solve_proof_low. simpl. + solve_proof_low. + eexists. repeat big_vcgen. + solve_func64 z0. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_func64 z2. reflexivity. + symmetry. sstep. assumption. somega. + solve_func64 z4. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_func64 z6. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_proof_low. somega. somega. simpl. + repeat big_vcgen. + solve_proof_low. simpl. + solve_proof_low. solve_proof_low. + solve_proof_low. simpl. solve_proof_low. + solve_proof_low. solve_proof_low. simpl. + solve_proof_low. + eexists. repeat big_vcgen. + solve_func64 z0. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_func64 z2. reflexivity. + symmetry. sstep. assumption. somega. + solve_func64 z4. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_func64 z6. reflexivity. + symmetry. sstep. assumption. somega. somega. + solve_proof_low. somega. somega. simpl. + repeat big_vcgen. + solve_proof_low. simpl. + solve_proof_low. solve_proof_low. + solve_proof_low. simpl. solve_proof_low. + solve_proof_low. solve_proof_low. simpl. + solve_proof_low. Qed. End BodyProof. diff --git a/proof/RealmSyncHandler/LowSpecs/handle_realm_rsi.v b/proof/RealmSyncHandler/LowSpecs/handle_realm_rsi.v index 5f70b84..5b5adbd 100644 --- a/proof/RealmSyncHandler/LowSpecs/handle_realm_rsi.v +++ b/proof/RealmSyncHandler/LowSpecs/handle_realm_rsi.v @@ -12,6 +12,54 @@ Local Open Scope Z_scope. Section SpecLow. Definition handle_realm_rsi_spec0 (rec: Pointer) (adt: RData) : option (RData * Z) := - None. + when' function_id == get_rec_regs_spec rec 0 adt; + when' arg1 == get_rec_regs_spec rec 1 adt; + when' arg2 == get_rec_regs_spec rec 2 adt; + when' arg3 == get_rec_regs_spec rec 3 adt; + rely is_int64 function_id; rely is_int64 arg1; rely is_int64 arg2; rely is_int64 arg3; + if function_id =? SMC_RSI_ABI_VERSION then + when adt == set_rec_regs_spec rec 1 (VZ64 RSI_ABI_VERSION) adt; + when adt == set_rec_regs_spec rec 0 (VZ64 STATUS_SUCCESS) adt; + Some (adt, 1) + else + if ((function_id >=? SMC32_PSCI_BASE) && (function_id <=? SMC32_PSCI_MAX)) || + ((function_id >=? SMC64_PSCI_BASE) && (function_id <=? SMC64_PSCI_MAX)) + then + when adt == psci_rsi_spec rec function_id (VZ64 arg1) (VZ64 arg2) (VZ64 arg3) adt; + when' x0 == get_psci_result_x0_spec adt; + rely is_int64 x0; + when adt == set_rec_regs_spec rec 0 (VZ64 x0) adt; + when' x1 == get_psci_result_x1_spec adt; + rely is_int64 x1; + when adt == set_rec_regs_spec rec 1 (VZ64 x1) adt; + when' x2 == get_psci_result_x2_spec adt; + rely is_int64 x2; + when adt == set_rec_regs_spec rec 2 (VZ64 x2) adt; + when' x3 == get_psci_result_x3_spec adt; + rely is_int64 x3; + when adt == set_rec_regs_spec rec 3 (VZ64 x3) adt; + when forward == get_psci_result_forward_psci_call_spec adt; + rely is_int forward; + if forward =? 1 then + when adt == set_rec_run_exit_reason_spec (VZ64 EXIT_REASON_PSCI) adt; + when adt == set_rec_run_gprs_spec 0 (VZ64 function_id) adt; + when' x1 == get_psci_result_forward_x1_spec adt; + rely is_int64 x1; + when adt == set_rec_run_gprs_spec 1 (VZ64 x1) adt; + when' x2 == get_psci_result_forward_x2_spec adt; + rely is_int64 x2; + when adt == set_rec_run_gprs_spec 2 (VZ64 x2) adt; + when' x3 == get_psci_result_forward_x3_spec adt; + rely is_int64 x3; + when adt == set_rec_run_gprs_spec 3 (VZ64 x3) adt; + when adt == set_rec_run_gprs_spec 4 (VZ64 0) adt; + when adt == set_rec_run_gprs_spec 5 (VZ64 0) adt; + when adt == set_rec_run_gprs_spec 6 (VZ64 0) adt; + Some (adt, 0) + else + Some (adt, 1) + else + when adt == set_rec_regs_spec rec 0 (VZ64 SMC_RETURN_UNKNOWN_FUNCTION) adt; + Some (adt, 1). End SpecLow. diff --git a/proof/RealmSyncHandler/Specs/handle_realm_rsi.v b/proof/RealmSyncHandler/Specs/handle_realm_rsi.v index 8a0aa70..fc9e881 100644 --- a/proof/RealmSyncHandler/Specs/handle_realm_rsi.v +++ b/proof/RealmSyncHandler/Specs/handle_realm_rsi.v @@ -12,7 +12,55 @@ Local Open Scope Z_scope. Section Spec. Definition handle_realm_rsi_spec (rec: Pointer) (adt: RData) : option (RData * Z) := - None. + when' function_id == get_rec_regs_spec rec 0 adt; + when' arg1 == get_rec_regs_spec rec 1 adt; + when' arg2 == get_rec_regs_spec rec 2 adt; + when' arg3 == get_rec_regs_spec rec 3 adt; + rely is_int64 function_id; rely is_int64 arg1; rely is_int64 arg2; rely is_int64 arg3; + if function_id =? SMC_RSI_ABI_VERSION then + when adt == set_rec_regs_spec rec 1 (VZ64 RSI_ABI_VERSION) adt; + when adt == set_rec_regs_spec rec 0 (VZ64 STATUS_SUCCESS) adt; + Some (adt, 1) + else + if ((function_id >=? SMC32_PSCI_BASE) && (function_id <=? SMC32_PSCI_MAX)) || + ((function_id >=? SMC64_PSCI_BASE) && (function_id <=? SMC64_PSCI_MAX)) + then + when adt == psci_rsi_spec rec function_id (VZ64 arg1) (VZ64 arg2) (VZ64 arg3) adt; + when' x0 == get_psci_result_x0_spec adt; + rely is_int64 x0; + when adt == set_rec_regs_spec rec 0 (VZ64 x0) adt; + when' x1 == get_psci_result_x1_spec adt; + rely is_int64 x1; + when adt == set_rec_regs_spec rec 1 (VZ64 x1) adt; + when' x2 == get_psci_result_x2_spec adt; + rely is_int64 x2; + when adt == set_rec_regs_spec rec 2 (VZ64 x2) adt; + when' x3 == get_psci_result_x3_spec adt; + rely is_int64 x3; + when adt == set_rec_regs_spec rec 3 (VZ64 x3) adt; + when forward == get_psci_result_forward_psci_call_spec adt; + rely is_int forward; + if forward =? 1 then + when adt == set_rec_run_exit_reason_spec (VZ64 EXIT_REASON_PSCI) adt; + when adt == set_rec_run_gprs_spec 0 (VZ64 function_id) adt; + when' x1 == get_psci_result_forward_x1_spec adt; + rely is_int64 x1; + when adt == set_rec_run_gprs_spec 1 (VZ64 x1) adt; + when' x2 == get_psci_result_forward_x2_spec adt; + rely is_int64 x2; + when adt == set_rec_run_gprs_spec 2 (VZ64 x2) adt; + when' x3 == get_psci_result_forward_x3_spec adt; + rely is_int64 x3; + when adt == set_rec_run_gprs_spec 3 (VZ64 x3) adt; + when adt == set_rec_run_gprs_spec 4 (VZ64 0) adt; + when adt == set_rec_run_gprs_spec 5 (VZ64 0) adt; + when adt == set_rec_run_gprs_spec 6 (VZ64 0) adt; + Some (adt, 0) + else + Some (adt, 1) + else + when adt == set_rec_regs_spec rec 0 (VZ64 SMC_RETURN_UNKNOWN_FUNCTION) adt; + Some (adt, 1). End Spec. diff --git a/proof/RunComplete/CodeProof/complete_hvc_exit.v b/proof/RunComplete/CodeProof/complete_hvc_exit.v index 2c6826e..586b951 100644 --- a/proof/RunComplete/CodeProof/complete_hvc_exit.v +++ b/proof/RunComplete/CodeProof/complete_hvc_exit.v @@ -27,10 +27,10 @@ Section CodeProof. Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}. Let L : compatlayer (cdata RData) := - _get_rec_last_run_info_esr ↦ gensem get_rec_last_run_info_esr_spec - ⊕ _set_rec_regs ↦ gensem set_rec_regs_spec - ⊕ _get_rec_run_gprs ↦ gensem get_rec_run_gprs_spec - ⊕ _reset_last_run_info ↦ gensem reset_last_run_info_spec + _get_rec_last_run_info_esr ↦ gensem get_rec_last_run_info_esr_spec + ⊕ _set_rec_regs ↦ gensem set_rec_regs_spec + ⊕ _get_rec_run_gprs ↦ gensem get_rec_run_gprs_spec + ⊕ _reset_last_run_info ↦ gensem reset_last_run_info_spec . Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L. @@ -46,34 +46,113 @@ Section CodeProof. Hypothesis h_get_rec_last_run_info_esr_s : Genv.find_symbol ge _get_rec_last_run_info_esr = Some b_get_rec_last_run_info_esr. Hypothesis h_get_rec_last_run_info_esr_p : Genv.find_funct_ptr ge b_get_rec_last_run_info_esr = Some (External (EF_external _get_rec_last_run_info_esr - (signature_of_type (Tcons Tptr Tnil) tulong cc_default)) - (Tcons Tptr Tnil) tulong cc_default). + (signature_of_type (Tcons Tptr Tnil) tulong cc_default)) + (Tcons Tptr Tnil) tulong cc_default). Local Opaque get_rec_last_run_info_esr_spec. Variable b_set_rec_regs: block. Hypothesis h_set_rec_regs_s : Genv.find_symbol ge _set_rec_regs = Some b_set_rec_regs. Hypothesis h_set_rec_regs_p : Genv.find_funct_ptr ge b_set_rec_regs = Some (External (EF_external _set_rec_regs - (signature_of_type (Tcons Tptr (Tcons tuint (Tcons tulong Tnil))) tvoid cc_default)) - (Tcons Tptr (Tcons tuint (Tcons tulong Tnil))) tvoid cc_default). + (signature_of_type (Tcons Tptr (Tcons tuint (Tcons tulong Tnil))) tvoid cc_default)) + (Tcons Tptr (Tcons tuint (Tcons tulong Tnil))) tvoid cc_default). Local Opaque set_rec_regs_spec. Variable b_get_rec_run_gprs: block. Hypothesis h_get_rec_run_gprs_s : Genv.find_symbol ge _get_rec_run_gprs = Some b_get_rec_run_gprs. Hypothesis h_get_rec_run_gprs_p : Genv.find_funct_ptr ge b_get_rec_run_gprs = Some (External (EF_external _get_rec_run_gprs - (signature_of_type (Tcons tuint Tnil) tulong cc_default)) - (Tcons tuint Tnil) tulong cc_default). + (signature_of_type (Tcons tuint Tnil) tulong cc_default)) + (Tcons tuint Tnil) tulong cc_default). Local Opaque get_rec_run_gprs_spec. Variable b_reset_last_run_info: block. Hypothesis h_reset_last_run_info_s : Genv.find_symbol ge _reset_last_run_info = Some b_reset_last_run_info. Hypothesis h_reset_last_run_info_p : Genv.find_funct_ptr ge b_reset_last_run_info = Some (External (EF_external _reset_last_run_info - (signature_of_type (Tcons Tptr Tnil) tvoid cc_default)) - (Tcons Tptr Tnil) tvoid cc_default). + (signature_of_type (Tcons Tptr Tnil) tvoid cc_default)) + (Tcons Tptr Tnil) tvoid cc_default). Local Opaque reset_last_run_info_spec. + Lemma complete_hvc_exit_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: complete_hvc_exit_spec0 (rec_base, rec_offset) d = Some d'), + exists le', (exec_stmt ge env le ((m, d): mem) complete_hvc_exit_body E0 le' (m, d') Out_normal). + Proof. + solve_code_proof Hspec complete_hvc_exit_body. + - get_loop_body. clear_hyp. + set (Hloop := C3). simpl; solve_proof_low. + remember + (PTree.set _i (Vint (Int.repr 0)) + (PTree.set _esr (Vlong (Int64.repr z0)) + (PTree.set _t'1 (Vlong (Int64.repr z0)) le))) as le_loop. + remember 7 as num. + set (P := fun le0 m0 => m0 = (m, d) /\ le0 = le_loop). + set (Q := fun (le0: temp_env) m0 => m0 = (m, r) /\ + le0 ! _rec = Some (Vptr rec_base (Int.repr rec_offset))). + set (Inv := fun le0 m0 n => exists i' adt', + complete_hvc_exit_loop0 (Z.to_nat (num - n)) 0 rec_base rec_offset d = + Some (Int.unsigned i', adt') /\ Int.unsigned i' = num - n /\ + m0 = (m, adt') /\ 0 <= n /\ n <= num /\ le0 ! _i = Some (Vint i') /\ + le0 ! _rec = Some (Vptr rec_base (Int.repr rec_offset))). + assert(loop_succ: forall N, Z.of_nat N <= num -> exists i' adt', + complete_hvc_exit_loop0 (Z.to_nat (num - Z.of_nat N)) 0 rec_base rec_offset d = + Some (Int.unsigned i', adt')). + { add_int Hloop z1; try somega. + induction N. rewrite Z.sub_0_r. rewrite Hloop. intros. repeat eexists; reflexivity. + intros. erewrite loop_ind_sub1 in IHN; try omega. + rewrite Nat2Z.inj_succ, succ_plus_1 in H. + assert(Hcc: Z.of_nat N <= num) by omega. + apply IHN in Hcc. destruct Hcc as (? & ? & Hnext). + Local Opaque Z.of_nat. simpl in Hnext. clear Heqle_loop. + simpl_func Hnext; try add_int' z; try somega; repeat eexists. } + assert (T: LoopProofSimpleWhile.t (external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops L) cond body ge (PTree.empty _) P Q). + { apply LoopProofSimpleWhile.make with (W:=Z) (lt:=fun z1 z2 => (0 <= z2 /\ z1 < z2)) (I:=Inv). + - apply Zwf_well_founded. + - unfold P, Inv. intros ? ? CC. destruct CC as [CC1 CC2]. + rewrite CC2 in *. exists num. + replace (num - num) with 0 by omega. simpl. + exists (Int.repr 0). exists d. + rewrite Heqnum. rewrite Heqle_loop. + repeat eexists; first [reflexivity|assumption|solve_proof_low]. + - intros ? ? ? I. unfold Inv in I. destruct I as (? & ? & ? & ? & ? & ? & ? & ? & ?). + set (Hnow := H). + rewrite Heqbody, Heqcond in *. + destruct (n >? 0) eqn:Hn; bool_rel. + + eexists. eexists. split_and. + * solve_proof_low. + * solve_proof_low. + * intro CC. inversion CC. + * assert(Hlx: Z.of_nat (Z.to_nat (n-1)) <= num) by (rewrite Z2Nat.id; omega). + apply loop_succ in Hlx. rewrite Z2Nat.id in Hlx; try omega. + intro. destruct Hlx as (? & ? & Hnext). duplicate Hnext. + rewrite loop_nat_sub1 in Hnext; try somega. + simpl in Hnext. rewrite Hnow in Hnext. + autounfold in Hnext; repeat simpl_hyp Hnext; + repeat destruct_con; bool_rel; contra; inversion Hnext. + rewrite H8, H9 in *; eexists; eexists; split. solve_proof_low. + exists (n-1); split. split; solve_proof_low. + solve_proof_low; unfold Inv; repeat eexists; first[eassumption|solve_proof_low]. + + eexists. eexists. split_and. + * solve_proof_low. + * solve_proof_low. + * intro. unfold Q. + assert (n=0) by omega. clear Heqle_loop. subst. + sstep. rewrite Hloop in Hnow. inv Hnow. + split_and; first[reflexivity|solve_proof_low]. + * intro CC. inversion CC. } + assert (Pre: P le_loop (m, d)) by (split; reflexivity). + pose proof (LoopProofSimpleWhile.termination _ _ _ _ _ _ T _ (m, d) Pre) as LoopProof. + destruct LoopProof as (le' & m' & (exec & Post)). + unfold exec_stmt in exec. rewrite Heqle_loop in exec. + unfold Q in Post. destruct Post as (Post & Hle'). rewrite Post in exec. + eexists; solve_proof_low. + - eexists. solve_proof_low. somega. + Qed. + End BodyProof. End CodeProof. diff --git a/proof/TableAux/CodeProof/granule_fill_table.v b/proof/TableAux/CodeProof/granule_fill_table.v index deb743e..637d77a 100644 --- a/proof/TableAux/CodeProof/granule_fill_table.v +++ b/proof/TableAux/CodeProof/granule_fill_table.v @@ -55,6 +55,85 @@ Section CodeProof. Tnil tvoid cc_default). Local Opaque barrier_spec. + Lemma granule_fill_table_body_correct: + forall m d d' env le pte_base pte_offset pte_val pte_inc + (Henv: env = PTree.empty _) + (Hinv: high_level_invariant d) + (HPTpte: PTree.get _pte le = Some (Vptr pte_base (Int.repr pte_offset))) + (HPTpte_val: PTree.get _pte_val le = Some (Vlong pte_val)) + (HPTpte_inc: PTree.get _pte_inc le = Some (Vlong pte_inc)) + (Hspec: granule_fill_table_spec0 (pte_base, pte_offset) (VZ64 (Int64.unsigned pte_val)) (VZ64 (Int64.unsigned pte_inc)) d = Some d'), + exists le', (exec_stmt ge env le ((m, d): mem) granule_fill_table_body E0 le' (m, d') Out_normal). + Proof. + solve_code_proof Hspec granule_fill_table_body; try solve [eexists; solve_proof_low]. + get_loop_body. clear_hyp. + set (Hloop := C1). + remember (PTree.set _i (Vint (Int.repr 0)) le) as le_loop. + remember 512 as num. + set (P := fun le0 m0 => m0 = (m, d) /\ le0 = le_loop). + set (Q := fun (le0: temp_env) m0 => m0 = (m, d')). + set (Inv := fun le0 m0 n => exists i' ptev' adt1, + granule_fill_table_loop0 (Z.to_nat (num - n)) 0 (pte_base, pte_offset) + (Int64.unsigned pte_val) (Int64.unsigned pte_inc) d + = Some (Int.unsigned i', Int64.unsigned ptev', adt1) /\ Int.unsigned i' = num - n /\ + m0 = (m, adt1) /\ 0 <= n /\ n <= num /\ le0 ! _i = Some (Vint i') /\ + le0 ! _pte = Some (Vptr pte_base (Int.repr pte_offset)) /\ + le0 ! _pte_val = Some (Vlong ptev') /\ + le0 ! _pte_inc = Some (Vlong pte_inc)). + assert(loop_succ: forall N, Z.of_nat N <= num -> exists i' ptev' adt', + granule_fill_table_loop0 (Z.to_nat (num - Z.of_nat N)) 0 (pte_base, pte_offset) + (Int64.unsigned pte_val) (Int64.unsigned pte_inc) d + = Some (Int.unsigned i', Int64.unsigned ptev', adt')). + { add_int Hloop z; try somega. add_int64 Hloop z0; try somega. + induction N. rewrite Z.sub_0_r. rewrite Hloop. intros. repeat eexists; reflexivity. + intros. erewrite loop_ind_sub1 in IHN; try omega. + rewrite Nat2Z.inj_succ, succ_plus_1 in H. + assert(Hcc: Z.of_nat N <= num) by omega. + apply IHN in Hcc. destruct Hcc as (? & ? & ? & Hnext). + Local Opaque Z.of_nat. simpl in Hnext. clear Heqle_loop. + simpl_func Hnext; try add_int' z1; try somega; try add_int64' z2; try somega; repeat eexists. } + assert (T: LoopProofSimpleWhile.t (external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops L) cond body ge (PTree.empty _) P Q). + { apply LoopProofSimpleWhile.make with (W:=Z) (lt:=fun z1 z2 => (0 <= z2 /\ z1 < z2)) (I:=Inv). + - apply Zwf_well_founded. + - unfold P, Inv. intros ? ? CC. destruct CC as [CC1 CC2]. + rewrite CC2 in *. exists num. + replace (num - num) with 0 by omega. simpl. add_int' 0; try somega. + rewrite Heqnum. rewrite Heqle_loop. + repeat eexists; first [reflexivity|assumption|solve_proof_low]. + - intros ? ? ? I. unfold Inv in I. destruct I as (? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ?). + set (Hnow := H). + rewrite Heqbody, Heqcond in *. + destruct (n >? 0) eqn:Hn; bool_rel. + + eexists. eexists. split_and. + * solve_proof_low. + * solve_proof_low. + * intro CC. inversion CC. + * assert(Hlx: Z.of_nat (Z.to_nat (n-1)) <= num) by (rewrite Z2Nat.id; omega). + apply loop_succ in Hlx. rewrite Z2Nat.id in Hlx; try omega. + intro. destruct Hlx as (? & ? & ? & Hnext). duplicate Hnext. + rewrite loop_nat_sub1 in Hnext; try somega. + simpl in Hnext. rewrite Hnow in Hnext. + autounfold in Hnext; repeat simpl_hyp Hnext; + repeat destruct_con; bool_rel; contra; inversion Hnext. + rewrite H10, H11, H12 in *; eexists; eexists; split. solve_proof_low. + exists (n-1); split. split; solve_proof_low. + solve_proof_low; unfold Inv; repeat eexists; first[eassumption|solve_proof_low]. + + eexists. eexists. split_and. + * solve_proof_low. + * solve_proof_low. + * intro. unfold Q. + assert (n=0) by omega. clear Heqle_loop. subst. + sstep. rewrite Hloop in Hnow. inv Hnow. + split_and; first[reflexivity|solve_proof_low]. + * intro CC. inversion CC. } + assert (Pre: P le_loop (m, d)) by (split; reflexivity). + pose proof (LoopProofSimpleWhile.termination _ _ _ _ _ _ T _ (m, d) Pre) as LoopProof. + destruct LoopProof as (le' & m' & (exec & Post)). + unfold exec_stmt in exec. rewrite Heqle_loop in exec. + unfold Q in Post. rewrite Post in exec. + eexists; solve_proof_low. + Qed. + End BodyProof. End CodeProof. diff --git a/proof/TableAux/CodeProof/table_has_destroyed.v b/proof/TableAux/CodeProof/table_has_destroyed.v index 0c5a251..d56ef05 100644 --- a/proof/TableAux/CodeProof/table_has_destroyed.v +++ b/proof/TableAux/CodeProof/table_has_destroyed.v @@ -46,6 +46,108 @@ Section CodeProof. (Tcons Tptr (Tcons tulong Tnil)) tulong cc_default). Local Opaque pgte_read_spec. + + Lemma table_has_destroyed_body_correct: + forall m d env le table_base table_offset res + (Henv: env = PTree.empty _) + (Hinv: high_level_invariant d) + (HPTtable: PTree.get _table le = Some (Vptr table_base (Int.repr table_offset))) + (Hspec: table_has_destroyed_spec0 (table_base, table_offset) d = Some (Int.unsigned res)), + exists le', (exec_stmt ge env le ((m, d): mem) table_has_destroyed_body E0 le' (m, d) (Out_return (Some (Vint res, tuint)))). + Proof. + solve_code_proof Hspec table_has_destroyed_body; try solve [eexists; solve_proof_low]. + get_loop_body. clear_hyp. + set (Hloop := C). simpl; solve_proof_low. + remember (PTree.set _i (Vlong (Int64.repr 0)) le) as le_loop. + remember 512 as num. + set (P := fun le0 m0 => m0 = (m, d) /\ le0 = le_loop). + set (Q := fun (le0: temp_env) m0 => m0 = (m, d)). + set (Inv := fun le0 m0 n => exists i' res', + table_has_destroyed_loop0 (Z.to_nat (num - n)) 0 0 (table_base, table_offset) d + = Some (Int64.unsigned i', Int.unsigned res') /\ Int64.unsigned i' = num - n /\ + m0 = (m, d) /\ 0 <= n /\ n <= num /\ le0 ! _i = Some (Vlong i') /\ + le0 ! _table = Some (Vptr table_base (Int.repr table_offset))). + assert(loop_succ: forall N, Z.of_nat N <= num -> exists i' res', + table_has_destroyed_loop0 (Z.to_nat (num - Z.of_nat N)) 0 0 (table_base, table_offset) d + = Some (Int64.unsigned i', Int.unsigned res')). + { add_int64 Hloop z; try somega. + induction N. rewrite Z.sub_0_r. rewrite Hloop. intros. repeat eexists; reflexivity. + intros. erewrite loop_ind_sub1 in IHN; try omega. + rewrite Nat2Z.inj_succ, succ_plus_1 in H. + assert(Hcc: Z.of_nat N <= num) by omega. + apply IHN in Hcc. destruct Hcc as (? & ? & Hnext). + Local Opaque Z.of_nat. simpl in Hnext. clear Heqle_loop. + simpl_func Hnext; try add_int64' z0; try somega; try add_int' z1; try somega; repeat eexists. } + assert (T: LoopProofSimpleWhile.t (external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops L) cond body ge (PTree.empty _) P Q). + { apply LoopProofSimpleWhile.make with (W:=Z) (lt:=fun z1 z2 => (0 <= z2 /\ z1 < z2)) (I:=Inv). + - apply Zwf_well_founded. + - unfold P, Inv. intros ? ? CC. destruct CC as [CC1 CC2]. + rewrite CC2 in *. exists num. + replace (num - num) with 0 by omega. simpl. + exists (Int64.repr 0). exists (Int.repr 0). + rewrite Heqnum. rewrite Heqle_loop. + repeat eexists; first [reflexivity|assumption|solve_proof_low]. + - intros ? ? ? I. unfold Inv in I. destruct I as (? & ? & ? & ? & ? & ? & ? & ? & ?). + set (Hnow := H). + rewrite Heqbody, Heqcond in *. + destruct (n >? 0) eqn:Hn; bool_rel. + + eexists. eexists. split_and. + * solve_proof_low. + * solve_proof_low. + * intro CC. inversion CC. + * assert(Hlx: Z.of_nat (Z.to_nat (n-1)) <= num) by (rewrite Z2Nat.id; omega). + apply loop_succ in Hlx. rewrite Z2Nat.id in Hlx; try omega. + intro. destruct Hlx as (? & ? & Hnext). duplicate Hnext. + rewrite loop_nat_sub1 in Hnext; try somega. + simpl in Hnext. rewrite Hnow in Hnext. + autounfold in Hnext; repeat simpl_hyp Hnext; + repeat destruct_con; bool_rel; contra; inversion Hnext. + rewrite H8, H9 in *; eexists; eexists; split. + set (ZZ := Int64.repr z1). + replace z1 with (Int64.unsigned ZZ) in C2. + solve_proof_low. + match goal with + | [|- match ?v with Some _ => _ | None => None end = _] => + replace v with (Some (VZ64 (Int64.unsigned ZZ))) + end. + reflexivity. + somega. replace ZZ with (Int64.repr z1) by reflexivity. + solve_proof_low. + exists (n-1); split. split; solve_proof_low. + solve_proof_low; unfold Inv; repeat eexists; first[eassumption|solve_proof_low]. + rewrite H8, H9. rewrite D. solve_proof_low. + rewrite H8. solve_proof_low. + + rewrite H8, H9 in *; eexists; eexists; split. + set (ZZ := Int64.repr z1). + replace z1 with (Int64.unsigned ZZ) in C2. + solve_proof_low. + match goal with + | [|- match ?v with Some _ => _ | None => None end = _] => + replace v with (Some (VZ64 (Int64.unsigned ZZ))) + end. + reflexivity. + somega. somega. somega. + replace ZZ with (Int64.repr z1) by reflexivity. + solve_proof_low. + exists (n-1); split. split; solve_proof_low. + solve_proof_low; unfold Inv; repeat eexists; first[eassumption|solve_proof_low]. + + eexists. eexists. split_and. + * solve_proof_low. + * solve_proof_low. + * intro. unfold Q. + assert (n=0) by omega. clear Heqle_loop. subst. + sstep. rewrite Hloop in Hnow. inv Hnow. + split_and; first[reflexivity|solve_proof_low]. + * intro CC. inversion CC. } + assert (Pre: P le_loop (m, d)) by (split; reflexivity). + pose proof (LoopProofSimpleWhile.termination _ _ _ _ _ _ T _ (m, d) Pre) as LoopProof. + destruct LoopProof as (le' & m' & (exec & Post)). + unfold exec_stmt in exec. rewrite Heqle_loop in exec. + unfold Q in Post. rewrite Post in exec. + eexists; solve_proof_low. + Qed. + End BodyProof. End CodeProof. diff --git a/proof/TableAux/CodeProof/table_maps_block.v b/proof/TableAux/CodeProof/table_maps_block.v index 4bef575..1901e08 100644 --- a/proof/TableAux/CodeProof/table_maps_block.v +++ b/proof/TableAux/CodeProof/table_maps_block.v @@ -64,6 +64,168 @@ Section CodeProof. (Tcons tulong (Tcons tulong Tnil)) tuint cc_default). Local Opaque addr_is_level_aligned_spec. + + 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. + + Lemma table_maps_block_body_correct: + forall m d env le table_base table_offset level ipa_state 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)) + (HPTipa_state: PTree.get _ipa_state le = Some (Vlong ipa_state)) + (Hspec: table_maps_block_spec0 (table_base, table_offset) (VZ64 (Int64.unsigned level)) (VZ64 (Int64.unsigned ipa_state)) d = Some (Int.unsigned res)), + exists le', (exec_stmt ge env le ((m, d): mem) table_maps_block_body E0 le' (m, d) (Out_return (Some (Vint res, tuint)))). + Proof. + solve_code_proof Hspec table_maps_block_body. + - eexists. repeat big_vcgen. + solve_func64 z0. reflexivity. + symmetry. repeat sstep. assumption. somega. + solve_func64 z2. reflexivity. + symmetry. repeat sstep. + rewrite C8. reflexivity. + somega. somega. somega. somega. + solve_proof_low. + simpl. solve_proof_low. + - get_loop_body. clear_hyp. + set (Hloop := C11). simpl; solve_proof_low. + remember + (PTree.set _i (Vint (Int.repr 0)) + (PTree.set _ret (Vint (Int.repr 1)) + (PTree.set _t'5 (Vint (Int.repr z3)) + (PTree.set _base_pa (Vlong (Int64.repr z2)) + (PTree.set _t'2 (Vlong (Int64.repr z2)) + (PTree.set _pgte (Vlong (Int64.repr z0)) + (PTree.set _t'1 (Vlong (Int64.repr z0)) le))))))) + as le_loop. + remember 512 as num. + set (P := fun le0 m0 => m0 = (m, d) /\ le0 = le_loop). + set (Q := fun (le0: temp_env) m0 => m0 = (m, d) /\ le0 ! _ret = Some (Vint res)). + set (Inv := fun le0 m0 n => exists i' ret', + table_maps_block_loop0 (Z.to_nat (num - n)) 0 1 (table_base, table_offset) z2 + (Int64.unsigned level) (Int64.unsigned ipa_state) d = + Some (Int.unsigned i', Int.unsigned ret') /\ Int.unsigned i' = num - n /\ + m0 = (m, d) /\ 0 <= n /\ n <= num /\ le0 ! _i = Some (Vint i') /\ + le0 ! _table = Some (Vptr table_base (Int.repr table_offset)) /\ + le0 ! _level = Some (Vlong level) /\ + le0 ! _ipa_state = Some (Vlong ipa_state) /\ + le0 ! _ret = Some (Vint ret') /\ + le0 ! _base_pa = Some (Vlong (Int64.repr z2))). + assert(loop_succ: forall N, Z.of_nat N <= num -> exists i' ret', + table_maps_block_loop0 (Z.to_nat (num - Z.of_nat N)) 0 1 + (table_base, table_offset) z2 + (Int64.unsigned level) (Int64.unsigned ipa_state) d = + Some (Int.unsigned i', Int.unsigned ret')). + { add_int Hloop z4; try somega. + induction N. rewrite Z.sub_0_r. rewrite Hloop. intros. repeat eexists; reflexivity. + intros. erewrite loop_ind_sub1 in IHN; try omega. + rewrite Nat2Z.inj_succ, succ_plus_1 in H. + assert(Hcc: Z.of_nat N <= num) by omega. + apply IHN in Hcc. destruct Hcc as (? & ? & Hnext). + Local Opaque Z.of_nat. simpl in Hnext. clear Heqle_loop. + simpl_func Hnext; try add_int' z; try somega; try add_int' z1; try somega; repeat eexists. } + assert (T: LoopProofSimpleWhile.t (external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops L) cond body ge (PTree.empty _) P Q). + { apply LoopProofSimpleWhile.make with (W:=Z) (lt:=fun z1 z2 => (0 <= z2 /\ z1 < z2)) (I:=Inv). + - apply Zwf_well_founded. + - unfold P, Inv. intros ? ? CC. destruct CC as [CC1 CC2]. + rewrite CC2 in *. exists num. + replace (num - num) with 0 by omega. simpl. + exists (Int.repr 0). exists (Int.repr 1). + rewrite Heqnum. rewrite Heqle_loop. + repeat eexists; first [reflexivity|assumption|solve_proof_low]. + - intros ? ? ? I. unfold Inv in I. + destruct I as (? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ?). + set (Hnow := H). + rewrite Heqbody, Heqcond in *. + destruct (n >? 0) eqn:Hn; bool_rel. + + eexists. eexists. split_and. + * solve_proof_low. + * solve_proof_low. + * intro CC. inversion CC. + * assert(Hlx: Z.of_nat (Z.to_nat (n-1)) <= num) by (rewrite Z2Nat.id; omega). + apply loop_succ in Hlx. rewrite Z2Nat.id in Hlx; try omega. + intro. destruct Hlx as (? & ? & Hnext). duplicate Hnext. + rewrite loop_nat_sub1 in Hnext; try somega. + simpl in Hnext. rewrite Hnow in Hnext. + autounfold in Hnext; repeat simpl_hyp Hnext; + repeat destruct_con; bool_rel; contra; inversion Hnext. + rewrite H12, H13 in *; eexists; eexists; split. + repeat big_vcgen. + solve_func64 z1. reflexivity. + symmetry. repeat sstep. assumption. somega. + solve_proof_low. somega. somega. somega. somega. somega. somega. + somega. somega. simpl. + solve_proof_low. solve_proof_low. + solve_proof_low. somega. + exists (n-1); split. split; solve_proof_low. + solve_proof_low; unfold Inv; repeat eexists; first[eassumption|solve_proof_low]. + rewrite <- (Int.repr_unsigned x2). rewrite <- H13. + rewrite Int.repr_unsigned. assumption. + + rewrite H12, H13 in *; eexists; eexists; split. + repeat big_vcgen. + solve_func64 z1. reflexivity. + symmetry. repeat sstep. assumption. somega. + solve_proof_low. somega. somega. somega. somega. somega. somega. + somega. somega. simpl. + solve_proof_low. solve_proof_low. + solve_proof_low. somega. + exists (n-1); split. split; solve_proof_low. + solve_proof_low; unfold Inv; repeat eexists; first[eassumption|solve_proof_low]. + rewrite H12. rewrite H13. rewrite D. sstep. reflexivity. + rewrite H12. sstep. omega. + + rewrite H12, H13 in *; eexists; eexists; split. + repeat big_vcgen. + solve_func64 z1. reflexivity. + symmetry. repeat sstep. assumption. somega. + solve_proof_low. somega. somega. somega. somega. somega. somega. + somega. somega. somega. somega. simpl. + solve_proof_low. solve_proof_low. + solve_proof_low. somega. + exists (n-1); split. split; solve_proof_low. + solve_proof_low; unfold Inv; repeat eexists; first[eassumption|solve_proof_low]. + rewrite H12. rewrite H13. rewrite D. sstep. reflexivity. + rewrite H12. sstep. omega. + + eexists. eexists. split_and. + * solve_proof_low. + * solve_proof_low. + * intro. unfold Q. + assert (n=0) by omega. clear Heqle_loop. subst. + sstep. rewrite Hloop in Hnow. inv Hnow. + split_and; first[reflexivity|solve_proof_low]. + * intro CC. inversion CC. } + assert (Pre: P le_loop (m, d)) by (split; reflexivity). + pose proof (LoopProofSimpleWhile.termination _ _ _ _ _ _ T _ (m, d) Pre) as LoopProof. + destruct LoopProof as (le' & m' & (exec & Post)). + unfold exec_stmt in exec. rewrite Heqle_loop in exec. + unfold Q in Post. destruct Post as (Post & Hle'). rewrite Post in exec. + + eexists. repeat big_vcgen. + solve_func64 z0. reflexivity. + symmetry. repeat sstep. assumption. somega. somega. + solve_func64 z2. reflexivity. + symmetry. repeat sstep. + solve_func z3. reflexivity. + symmetry. sstep. assumption. somega. somega. somega. somega. + solve_proof_low. simpl. + solve_proof_low. + Qed. + + + End BodyProof. End CodeProof. diff --git a/proof/TableAux/LowSpecs/granule_fill_table.v b/proof/TableAux/LowSpecs/granule_fill_table.v index 7704085..4f9c9d5 100644 --- a/proof/TableAux/LowSpecs/granule_fill_table.v +++ b/proof/TableAux/LowSpecs/granule_fill_table.v @@ -16,7 +16,7 @@ Section SpecLow. | S n' => match granule_fill_table_loop0 n' i pte pte_val pte_inc adt with | Some (i, pte_val, adt) => - rely is_int64 i; rely is_int64 pte_val; + rely is_int i; rely is_int64 pte_val; when adt == pgte_write_spec pte (VZ64 i) (VZ64 pte_val) adt; Some (i + 1, pte_val + pte_inc, adt) | _ => None @@ -29,7 +29,7 @@ Section SpecLow. rely is_int64 pte_val; rely is_int64 pte_inc; match granule_fill_table_loop0 (Z.to_nat PGTES_PER_TABLE) 0 pte pte_val pte_inc adt with | Some (i, pte_val, adt) => - rely is_int64 i; rely is_int64 pte_val; + rely is_int i; rely is_int64 pte_val; Some adt | _ => None end diff --git a/proof/TableAux/LowSpecs/table_maps_block.v b/proof/TableAux/LowSpecs/table_maps_block.v index 8800509..e852100 100644 --- a/proof/TableAux/LowSpecs/table_maps_block.v +++ b/proof/TableAux/LowSpecs/table_maps_block.v @@ -16,7 +16,7 @@ Section SpecLow. | S n' => match table_maps_block_loop0 n' i ret table base_pa level ipa_state adt with | Some (i, ret) => - rely is_int64 i; rely is_int ret; + rely is_int i; rely is_int ret; when' pgte == pgte_read_spec table (VZ64 i) adt; rely is_int64 pgte; let expected_pa := base_pa + i * GRANULE_SIZE in @@ -46,7 +46,7 @@ Section SpecLow. if aligned =? 0 then Some 0 else match table_maps_block_loop0 (Z.to_nat PGTES_PER_TABLE) 0 1 table base_pa level ipa_state adt with | Some (i, ret) => - rely is_int64 i; rely is_int ret; + rely is_int i; rely is_int ret; Some ret | _ => None end diff --git a/proof/TableWalk/CodeProof/table_walk_lock_unlock.v b/proof/TableWalk/CodeProof/table_walk_lock_unlock.v index f567ea8..bb80735 100644 --- a/proof/TableWalk/CodeProof/table_walk_lock_unlock.v +++ b/proof/TableWalk/CodeProof/table_walk_lock_unlock.v @@ -128,6 +128,207 @@ Section CodeProof. (Tcons tulong Tnil) tvoid cc_default). Local Opaque set_wi_index_spec. + Fixpoint table_walk_lock_unlock_loop0 (n: nat) (l: Z) (tbl: Pointer) (last_tbl: Pointer) (map_addr: Z) (adt: RData) := + match n with + | O => Some (l, tbl, last_tbl, adt) + | S n' => + match table_walk_lock_unlock_loop0 n' l tbl last_tbl map_addr adt with + | Some (l, (tbl_base, tbl_ofst), (last_tbl_base, last_tbl_ofst), adt) => + rely is_int l; rely is_int tbl_ofst; rely is_int last_tbl_ofst; + when null == is_null_spec (tbl_base, tbl_ofst) adt; + rely is_int null; + if null =? 0 then + when' idx == addr_to_idx_spec (VZ64 map_addr) (VZ64 l) adt; + rely is_int64 idx; + when'' tbl_base, tbl_ofst, adt == find_next_level_idx_spec (tbl_base, tbl_ofst) (VZ64 idx) adt; + rely is_int tbl_ofst; + when null == is_null_spec (tbl_base, tbl_ofst) adt; + rely is_int null; + if null =? 0 then + when adt == granule_lock_spec (tbl_base, tbl_ofst) adt; + when adt == granule_unlock_spec (last_tbl_base, last_tbl_ofst) adt; + Some (l + 1, (tbl_base, tbl_ofst), (tbl_base, tbl_ofst), adt) + else + when adt == granule_unlock_spec (last_tbl_base, last_tbl_ofst) adt; + Some (l + 1, (tbl_base, tbl_ofst), (last_tbl_base, last_tbl_ofst), adt) + else Some (l + 1, (tbl_base, tbl_ofst), (last_tbl_base, last_tbl_ofst), adt) + | _ => None + end + end. + + Definition table_walk_lock_unlock_spec0 (g_rd: Pointer) (map_addr: Z64) (level: Z64) (adt: RData) : option RData := + match map_addr, level with + | VZ64 map_addr, VZ64 level => + when'' rd_base, rd_ofst, adt == granule_map_spec g_rd SLOT_RD adt; + rely is_int rd_ofst; + when'' g_root_base, g_root_ofst == get_rd_g_rtt_spec (rd_base, rd_ofst) adt; + rely is_int g_root_ofst; + when adt == buffer_unmap_spec (rd_base, rd_ofst) adt; + when adt == granule_lock_spec (g_root_base, g_root_ofst) adt; + match table_walk_lock_unlock_loop0 (Z.to_nat level) 0 (g_root_base, g_root_ofst) (g_root_base, g_root_ofst) map_addr adt with + | Some (l, (tbl_base, tbl_ofst), (last_tbl_base, last_tbl_ofst), adt) => + rely is_int l; rely is_int tbl_ofst; rely is_int last_tbl_ofst; + when adt == set_wi_g_llt_spec (tbl_base, tbl_ofst) adt; + when' idx == addr_to_idx_spec (VZ64 map_addr) (VZ64 level) adt; + rely is_int64 idx; + when adt == set_wi_index_spec (VZ64 idx) adt; + Some adt + | _ => None + end + end. + + 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. + + Lemma table_walk_lock_unlock_body_correct: + forall m d d' env le g_rd_base g_rd_offset map_addr level + (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_walk_lock_unlock_spec0 (g_rd_base, g_rd_offset) (VZ64 (Int64.unsigned map_addr)) (VZ64 (Int64.unsigned level)) d = Some d'), + exists le', (exec_stmt ge env le ((m, d): mem) table_walk_lock_unlock_body E0 le' (m, d') Out_normal). + Proof. + solve_code_proof Hspec table_walk_lock_unlock_body. + get_loop_body. clear_hyp. + set (Hloop := C8). simpl; solve_proof_low. + remember + (PTree.set _last_tbl (Vptr p3 (Int.repr z0)) + (PTree.set _tbl (Vptr p3 (Int.repr z0)) + (PTree.set _t'3 (Vptr p3 (Int.repr z0)) + (PTree.set _g_root (Vptr p3 (Int.repr z0)) + (PTree.set _t'2 (Vptr p3 (Int.repr z0)) + (PTree.set _rd (Vptr p1 (Int.repr z)) + (PTree.set _t'1 (Vptr p1 (Int.repr z)) + (PTree.set _last_level (Vlong (Int64.repr 0)) + (PTree.set _l (Vlong (Int64.repr 0)) le))))))))) + as le_loop. + remember (Int64.unsigned level) as num. + set (P := fun le0 m0 => m0 = (m, r1) /\ le0 = le_loop). + set (Q := fun (le0: temp_env) m0 => m0 = (m, r2) /\ + le0 ! _map_addr = Some (Vlong map_addr) /\ + le0 ! _level = Some (Vlong level) /\ + le0 ! _tbl = Some (Vptr p9 (Int.repr z2))). + set (Inv := fun le0 m0 n => exists l' tbl_base' tbl_ofst' last_tbl_base' last_tbl_ofst' adt', + table_walk_lock_unlock_loop0 (Z.to_nat (num - n)) 0 + (p3, z0) (p3, z0) (Int64.unsigned map_addr) r1 = + Some (Int64.unsigned l', (tbl_base', tbl_ofst'), + (last_tbl_base', last_tbl_ofst'), adt') /\ + Int64.unsigned l' = num - n /\ + m0 = (m, adt') /\ 0 <= n /\ n <= num /\ + le0 ! _l = Some (Vlong l') /\ + le0 ! _map_addr = Some (Vlong map_addr) /\ + le0 ! _level = Some (Vlong level) /\ + le0 ! _tbl = Some (Vptr tbl_base' (Int.repr tbl_ofst')) /\ + le0 ! _last_tbl = Some (Vptr last_tbl_base' (Int.repr last_tbl_ofst'))). + assert(loop_succ: forall N, Z.of_nat N <= num -> exists l' tbl_base' tbl_ofst' last_tbl_base' last_tbl_ofst' adt', + table_walk_lock_unlock_loop0 (Z.to_nat (num - Z.of_nat N)) 0 + (p3, z0) (p3, z0) (Int64.unsigned map_addr) r1 = + Some (Int64.unsigned l', (tbl_base', tbl_ofst'), + (last_tbl_base', last_tbl_ofst'), adt')). + { add_int64 Hloop z1; try somega. + add_int Hloop z2; try somega. + add_int Hloop z3; try somega. + induction N. rewrite Z.sub_0_r. rewrite Hloop. intros. repeat eexists; reflexivity. + intros. erewrite loop_ind_sub1 in IHN; try omega. + rewrite Nat2Z.inj_succ, succ_plus_1 in H. + assert(Hcc: Z.of_nat N <= num) by omega. + apply IHN in Hcc. destruct Hcc as (? & ? & ? & ? & ? & ? & Hnext). + Local Opaque Z.of_nat. simpl in Hnext. clear Heqle_loop. + simpl_func Hnext; + try add_int64' z4; try somega; try add_int' z6; try somega; + try add_int' z7; try somega; repeat eexists. } + assert (T: LoopProofSimpleWhile.t (external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops L) cond body ge (PTree.empty _) P Q). + { apply LoopProofSimpleWhile.make with (W:=Z) (lt:=fun z1 z2 => (0 <= z2 /\ z1 < z2)) (I:=Inv). + - apply Zwf_well_founded. + - unfold P, Inv. intros ? ? CC. destruct CC as [CC1 CC2]. + rewrite CC2 in *. exists num. + replace (num - num) with 0 by omega. simpl. + exists (Int64.repr 0). eexists. eexists. + eexists. eexists. eexists. + rewrite Heqnum. rewrite Heqle_loop. + repeat eexists; first [reflexivity|assumption|solve_proof_low]. + - intros ? ? ? I. unfold Inv in I. + destruct I as (? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ?). + set (Hnow := H). + rewrite Heqbody, Heqcond in *. + destruct (n >? 0) eqn:Hn; bool_rel. + + eexists. eexists. split_and. + * solve_proof_low. + * solve_proof_low. + * intro CC. inversion CC. + * assert(Hlx: Z.of_nat (Z.to_nat (n-1)) <= num) by (rewrite Z2Nat.id; omega). + apply loop_succ in Hlx. rewrite Z2Nat.id in Hlx; try omega. + intro. destruct Hlx as (? & ? & ? & ? & ? & ? & Hnext). duplicate Hnext. + rewrite loop_nat_sub1 in Hnext; try somega. + simpl in Hnext. rewrite Hnow in Hnext. + autounfold in Hnext; repeat simpl_hyp Hnext; + repeat destruct_con; bool_rel; contra; inversion Hnext. + rewrite H12 in *. rewrite H13 in *. rewrite H14 in *. + rewrite H15 in *. rewrite H16 in *. + eexists; eexists; split. + repeat big_vcgen. solve_func z4. reflexivity. + symmetry. sstep. assumption. somega. + solve_proof_low. simpl. + solve_proof_low. solve_proof_low. + solve_proof_low. + exists (n-1); split. split; solve_proof_low. + solve_proof_low; unfold Inv; repeat eexists; first[eassumption|solve_proof_low]. + + rewrite H12 in *. rewrite H13 in *. rewrite H14 in *. + rewrite H15 in *. rewrite H16 in *. + eexists; eexists; split. + repeat big_vcgen. solve_func z4. reflexivity. + symmetry. sstep. assumption. somega. + solve_proof_low. simpl. + solve_proof_low. solve_proof_low. + solve_proof_low. + exists (n-1); split. split; solve_proof_low. + solve_proof_low; unfold Inv; repeat eexists; first[eassumption|solve_proof_low]. + + rewrite H12 in *. rewrite H13 in *. rewrite H14 in *. + rewrite H15 in *. rewrite H16 in *. + eexists; eexists; split. + repeat big_vcgen. solve_func z4. reflexivity. + symmetry. sstep. assumption. somega. + solve_proof_low. simpl. + solve_proof_low. solve_proof_low. + solve_proof_low. + exists (n-1); split. split; solve_proof_low. + solve_proof_low; unfold Inv; repeat eexists; first[eassumption|solve_proof_low]. + + eexists. eexists. split_and. + * solve_proof_low. + * solve_proof_low. + * intro. unfold Q. + assert (n=0) by omega. clear Heqle_loop. subst. + sstep. rewrite Hloop in Hnow. inv Hnow. + split_and; first[reflexivity|solve_proof_low]. + * intro CC. inversion CC. } + assert (Pre: P le_loop (m, r1)) by (split; reflexivity). + pose proof (LoopProofSimpleWhile.termination _ _ _ _ _ _ T _ (m, r1) Pre) as LoopProof. + destruct LoopProof as (le' & m' & (exec & Post)). + unfold exec_stmt in exec. rewrite Heqle_loop in exec. + unfold Q in Post. destruct Post as (Post & Hle'). rewrite Post in exec. + + destruct Hle' as (? & ? & ?). + eexists; solve_proof_low. + solve_func64 z5. reflexivity. + symmetry. sstep. rewrite <- Heqnum. assumption. + sstep. sstep. assumption. somega. + Qed. + End BodyProof. End CodeProof.