Created
March 14, 2024 16:20
-
-
Save Janno/91fc68661c99eae1e7bcc983b5eabf4d to your computer and use it in GitHub Desktop.
fast.v fails immediately, slow.v takes forever
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Module Test1. | |
| Axiom Timeless : forall {X:Type} (x:X), Prop. | |
| Axiom biIndex : Type. | |
| Axiom gFunctors : Type. | |
| Axiom genv : Type. | |
| Axiom State : Set. | |
| Axiom code : Set. | |
| Axiom roundup_gname : Set. | |
| Axiom ptr : Set. | |
| Record bi : Type := Bi | |
| { bi_car :> Type; | |
| bi_sep : forall (_ : bi_car) (_ : bi_car), bi_car; | |
| bi_exist : forall (A : Type) (_ : forall _ : A, bi_car), bi_car; | |
| }. | |
| Axiom cpp_logic : biIndex -> gFunctors -> Type. | |
| Axiom bm_cpu_GlobalCfg : Type. | |
| Axiom bm_dram_bm_aux_1_bm_dram_GlobalCfg : Type. | |
| Axiom bm_dram_bm_aux_1_bm_dram_GlobalGName : bm_dram_bm_aux_1_bm_dram_GlobalCfg -> Set. | |
| Axiom bm_dram_bm_aux_1_bm_dram_GlobalG : forall {ti : biIndex} {Σ : gFunctors}, cpp_logic ti Σ -> Set. | |
| Axiom bm_cpu_GlobalG : forall {ti : biIndex} {Σ : gFunctors}, cpp_logic ti Σ -> Set. | |
| Axiom user_signal_AbsPred : forall {thread_info : biIndex} {_Σ : gFunctors}, cpp_logic thread_info _Σ -> forall {_ : genv}, Type. | |
| Axiom G : forall {ti : biIndex} {_Σ : gFunctors} (Σ : cpp_logic ti _Σ) {σ : genv}, bm_cpu_GlobalCfg -> @user_signal_AbsPred ti _Σ Σ σ -> Type. | |
| Record seal (A : Type) (f : A) : Type := Build_seal { unseal : A; seal_eq : @eq A unseal f }. | |
| Axiom monPred : forall (_ : biIndex) (_ : bi), Type. | |
| Axiom monPred_sep_def : forall {I : biIndex} {PROP : bi} (_ : monPred I PROP) (_ : monPred I PROP), monPred I PROP. | |
| Axiom monPred_sep_aux : | |
| forall {I : biIndex} {PROP : bi}, | |
| @seal (forall (_ : monPred I PROP) (_ : monPred I PROP), monPred I PROP) (@monPred_sep_def I PROP). | |
| Definition monPred_sep : | |
| forall (I : biIndex) (PROP : bi) (_ : monPred I PROP) (_ : monPred I PROP), monPred I PROP | |
| := | |
| fun (I : biIndex) (PROP : bi) => @unseal _ _ (@monPred_sep_aux I PROP). | |
| Axiom iPropI : forall Σ : gFunctors, bi. | |
| Axiom TODO: forall{P:Type}, P. | |
| Definition mpredI := | |
| fun (thread_info : biIndex) (Σ : gFunctors) => | |
| {| | |
| bi_car := monPred thread_info (iPropI Σ); | |
| bi_sep := @monPred_sep _ _; | |
| bi_exist := TODO; | |
| |}. | |
| Arguments mpredI {thread_info Σ}. | |
| Axiom __at_body : forall {ti : biIndex} {Σ : gFunctors} {_Σ : cpp_logic ti Σ}, ptr -> @mpredI ti Σ -> @mpredI ti Σ. | |
| Goal | |
| forall (Tr : forall PROP : bi, bi_car PROP) (H : bm_cpu_GlobalCfg) (H0 : bm_dram_bm_aux_1_bm_dram_GlobalCfg) | |
| (ti : biIndex) (_Σ : gFunctors) (Σ : cpp_logic ti _Σ) (σ : genv) (H2 : @user_signal_AbsPred ti _Σ Σ σ) | |
| (H5 : @bm_dram_bm_aux_1_bm_dram_GlobalGName H0) (H7 : @bm_dram_bm_aux_1_bm_dram_GlobalG ti _Σ Σ) (H8 : @bm_cpu_GlobalG ti _Σ Σ) | |
| (G0 : @G ti _Σ Σ σ H H2) (to_code_nvs : code) (vcpusharedg : roundup_gname) (body : @mpredI ti _Σ) | |
| (recall_bit : bool) | |
| (novastateinv : forall (_ : @bm_dram_bm_aux_1_bm_dram_GlobalGName H0) (_ : @bm_dram_bm_aux_1_bm_dram_GlobalG ti _Σ Σ) | |
| (_ : @bm_cpu_GlobalG ti _Σ Σ) (_ : @G ti _Σ Σ σ H H2) (_ : roundup_gname) | |
| (_ : bool) (_ : bool) (_ : bool), @mpredI ti _Σ) | |
| (ecInv0 : forall _ : bool, @mpredI ti _Σ) | |
| (_ : forall (a1 : ptr) (a3 : bool), | |
| @Timeless (bi_car (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (ecInv0 a3) | |
| (@bi_exist (@mpredI ti _Σ) State | |
| (fun m : State => | |
| @bi_exist (@mpredI ti _Σ) bool | |
| (fun about_to_ipc_reply : bool => | |
| @bi_exist (@mpredI ti _Σ) bool | |
| (fun past_recall_in_roundup_impl : bool => | |
| @bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) | |
| (novastateinv H5 H7 H8 G0 vcpusharedg about_to_ipc_reply a3 | |
| past_recall_in_roundup_impl ) | |
| (@__at_body ti _Σ Σ a1 (Tr _)))))))))))), | |
| @Timeless (bi_car (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (ecInv0 recall_bit) | |
| (@bi_exist (@mpredI ti _Σ) State | |
| (fun m : State => | |
| @bi_exist (@mpredI ti _Σ) bool | |
| (fun about_to_ipc_reply : bool => | |
| @bi_exist (@mpredI ti _Σ) bool | |
| (fun past_recall_in_roundup_impl : bool => | |
| @bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) | |
| (novastateinv H5 H7 H8 G0 vcpusharedg about_to_ipc_reply recall_bit | |
| past_recall_in_roundup_impl ) body))))))))). | |
| intros * T. | |
| Timeout 1 Fail autoapply T with typeclass_instances. | |
| End Test1. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Module Test1. | |
| Axiom Timeless : forall {X:Type} (x:X), Prop. | |
| Axiom biIndex : Type. | |
| Axiom gFunctors : Type. | |
| Axiom genv : Type. | |
| Axiom State : Set. | |
| Axiom code : Set. | |
| Axiom roundup_gname : Set. | |
| Axiom ptr : Set. | |
| Record bi : Type := Bi | |
| { bi_car :> Type; | |
| bi_sep : forall (_ : bi_car) (_ : bi_car), bi_car; | |
| bi_exist : forall (A : Type) (_ : forall _ : A, bi_car), bi_car; | |
| }. | |
| Axiom cpp_logic : biIndex -> gFunctors -> Type. | |
| Axiom bm_cpu_GlobalCfg : Type. | |
| Axiom bm_dram_bm_aux_1_bm_dram_GlobalCfg : Type. | |
| Axiom bm_dram_bm_aux_1_bm_dram_GlobalGName : bm_dram_bm_aux_1_bm_dram_GlobalCfg -> Set. | |
| Axiom bm_dram_bm_aux_1_bm_dram_GlobalG : forall {ti : biIndex} {Σ : gFunctors}, cpp_logic ti Σ -> Set. | |
| Axiom bm_cpu_GlobalG : forall {ti : biIndex} {Σ : gFunctors}, cpp_logic ti Σ -> Set. | |
| Axiom user_signal_AbsPred : forall {thread_info : biIndex} {_Σ : gFunctors}, cpp_logic thread_info _Σ -> forall {_ : genv}, Type. | |
| Axiom G : forall {ti : biIndex} {_Σ : gFunctors} (Σ : cpp_logic ti _Σ) {σ : genv}, bm_cpu_GlobalCfg -> @user_signal_AbsPred ti _Σ Σ σ -> Type. | |
| Record seal (A : Type) (f : A) : Type := Build_seal { unseal : A; seal_eq : @eq A unseal f }. | |
| Axiom monPred : forall (_ : biIndex) (_ : bi), Type. | |
| Axiom monPred_sep_def : forall {I : biIndex} {PROP : bi} (_ : monPred I PROP) (_ : monPred I PROP), monPred I PROP. | |
| Axiom monPred_sep_aux : | |
| forall {I : biIndex} {PROP : bi}, | |
| @seal (forall (_ : monPred I PROP) (_ : monPred I PROP), monPred I PROP) (@monPred_sep_def I PROP). | |
| Definition monPred_sep : | |
| forall (I : biIndex) (PROP : bi) (_ : monPred I PROP) (_ : monPred I PROP), monPred I PROP | |
| := | |
| fun (I : biIndex) (PROP : bi) => @unseal _ _ (@monPred_sep_aux I PROP). | |
| Axiom iPropI : forall Σ : gFunctors, bi. | |
| Axiom TODO: forall{P:Type}, P. | |
| Definition mpredI := | |
| fun (thread_info : biIndex) (Σ : gFunctors) => | |
| {| | |
| bi_car := monPred thread_info (iPropI Σ); | |
| bi_sep := @monPred_sep _ _; | |
| bi_exist := TODO; | |
| |}. | |
| Arguments mpredI {thread_info Σ}. | |
| Axiom __at_body : forall {ti : biIndex} {Σ : gFunctors} {_Σ : cpp_logic ti Σ}, ptr -> @mpredI ti Σ -> @mpredI ti Σ. | |
| Goal | |
| forall (Tr : forall PROP : bi, bi_car PROP) (H : bm_cpu_GlobalCfg) (H0 : bm_dram_bm_aux_1_bm_dram_GlobalCfg) | |
| (ti : biIndex) (_Σ : gFunctors) (Σ : cpp_logic ti _Σ) (σ : genv) (H2 : @user_signal_AbsPred ti _Σ Σ σ) | |
| (H5 : @bm_dram_bm_aux_1_bm_dram_GlobalGName H0) (H7 : @bm_dram_bm_aux_1_bm_dram_GlobalG ti _Σ Σ) (H8 : @bm_cpu_GlobalG ti _Σ Σ) | |
| (G0 : @G ti _Σ Σ σ H H2) (to_code_nvs : code) (vcpusharedg : roundup_gname) (body : @mpredI ti _Σ) | |
| (recall_bit : bool) | |
| (novastateinv : forall (_ : @bm_dram_bm_aux_1_bm_dram_GlobalGName H0) (_ : @bm_dram_bm_aux_1_bm_dram_GlobalG ti _Σ Σ) | |
| (_ : @bm_cpu_GlobalG ti _Σ Σ) (_ : @G ti _Σ Σ σ H H2) (_ : roundup_gname) (_ : code) | |
| (_ : bool) (_ : bool) (_ : bool), @mpredI ti _Σ) | |
| (ecInv0 : forall _ : bool, @mpredI ti _Σ) | |
| (_ : forall (a1 : ptr) (a3 : bool), | |
| @Timeless (bi_car (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (ecInv0 a3) | |
| (@bi_exist (@mpredI ti _Σ) State | |
| (fun m : State => | |
| @bi_exist (@mpredI ti _Σ) bool | |
| (fun about_to_ipc_reply : bool => | |
| @bi_exist (@mpredI ti _Σ) bool | |
| (fun past_recall_in_roundup_impl : bool => | |
| @bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) | |
| (novastateinv H5 H7 H8 G0 vcpusharedg to_code_nvs about_to_ipc_reply a3 | |
| past_recall_in_roundup_impl ) | |
| (@__at_body ti _Σ Σ a1 (Tr _)))))))))))), | |
| @Timeless (bi_car (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (ecInv0 recall_bit) | |
| (@bi_exist (@mpredI ti _Σ) State | |
| (fun m : State => | |
| @bi_exist (@mpredI ti _Σ) bool | |
| (fun about_to_ipc_reply : bool => | |
| @bi_exist (@mpredI ti _Σ) bool | |
| (fun past_recall_in_roundup_impl : bool => | |
| @bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) (Tr (@mpredI ti _Σ)) | |
| (@bi_sep (@mpredI ti _Σ) | |
| (novastateinv H5 H7 H8 G0 vcpusharedg to_code_nvs about_to_ipc_reply recall_bit | |
| past_recall_in_roundup_impl ) body))))))))). | |
| intros * T. | |
| Timeout 10 autoapply T with typeclass_instances. | |
| End Test1. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment