Skip to content

Instantly share code, notes, and snippets.

@jldodds
Created January 29, 2015 00:19
Show Gist options
  • Save jldodds/74ff4574991855ec1498 to your computer and use it in GitHub Desktop.
Save jldodds/74ff4574991855ec1498 to your computer and use it in GitHub Desktop.
Ltac run_rtac reify term_table tac_sound reduce :=
start_timer "total";
start_timer "02 match_tactic";
lazymatch type of tac_sound with
| forall t, @rtac_sound _ _ _ _ _ _ (?tac _) =>
let namee := fresh "e" in
match goal with
| |- ?P =>
stop_timer "02 match_tactic";
start_timer "03 reification";
reify_aux reify term_table P namee;
stop_timer "03 reification";
start_timer "04 match type";
let tbl := get_tbl in
let t := constr:(Some typrop) in
let goal := namee in
match t with
| Some ?t =>
let goal_result := constr:(run_tac' (tac tbl) (GGoal namee)) in
stop_timer"04 match type";
start_timer "05 vm_compute";
let result := eval vm_compute in goal_result in
stop_timer "05 vm_compute";
start_timer "06 match result";
match result with
| More_ ?s ?g =>
let g' := g in
set (sv := s);
stop_timer "06 match result";
start_timer "07 goalD";
let gd_prop :=
constr:(goalD_Prop tbl nil nil g') in
stop_timer "07 goalD";
start_timer "08 reduce";
let gd' :=
reduce hd gd_prop in
stop_timer "08 reduce";
start_timer "09 cut1";
cut (gd'); [ stop_timer "09 cut1";
start_timer "10 change";
(* change (gd_prop ->
exprD_Prop tbl nil nil namee);
*)
stop_timer "10 change";
start_timer "11 cut2";
cut (goal_result = More_ sv g');
[ stop_timer "11 cut2";
start_timer "12 exact";
(*set (pf := *)
exact_no_check
(@run_rtac_More tbl (tac tbl)
sv g' namee (tac_sound tbl))
(*;
exact pf*)
| stop_timer "12 exact";
start_timer "13 VM_CAST";
vm_cast_no_check
(@eq_refl _ (More_ sv g'))
]
| stop_timer "13 VM_CAST"; clear (*g'*) sv ]
| Solved ?s =>
exact_no_check (@run_rtac_Solved tbl (tac tbl) s namee (tac_sound tbl)
(@eq_refl (Result (CTop nil nil)) (Solved s) <: run_tac' (tac tbl) (GGoal goal) = Solved s))
| Fail => idtac "Tactic" tac "failed."
| _ => idtac "Error: run_rtac could not resolve the result from the tactic :" tac
end
| None => idtac "expression " goal "is ill typed" t
end
end; try (clear namee; clear_tbl)
| _ => idtac tac_sound "is not a soudness theorem."
end; stop_timer "total".
Ltac rforward := run_rtac reify_vst term_table (SYMEXE_sound 1000) cbv_denote.
Ltac rforward_admit := run_rtac reify_vst term_table (SYMEXE_sound 1000) admit.
Local Open Scope logic.
Require Import reverse_defs.
Existing Instance NullExtension.Espec.
Fixpoint lots_of_sets' n p :=
match n with
| O => (Sset p (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid)))
| S n' => Ssequence (Sset p (Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid))) (lots_of_sets' n' (Psucc p))
end.
Definition lots_of_sets n := lots_of_sets' (pred n) 1%positive.
Fixpoint lots_temps' n p :=
match n with
| O => (PTree.empty _)
| S n' => PTree.set p (tptr t_struct_list, true) (lots_temps' n' (Psucc p))
end.
Definition lots_temps (n : nat) : PTree.t (type * bool) := lots_temps' (n) (1%positive).
Fixpoint lots_locals' n p :=
match n with
| O => (PTree.empty _)
| S n' => PTree.set p (Vint (Int.repr 0%Z)) (lots_locals' n' (Psucc p))
end.
Definition lots_locals (n : nat):= lots_locals' (n) (1%positive).
Fixpoint lots_vars' n p :=
match n with
| O => (PTree.empty _)
| S n' => PTree.set p (tptr t_struct_list, Vint (Int.repr 0%Z)) (lots_vars' n' (Psucc p))
end.
Definition lots_vars (n : nat):= lots_vars' (n) (1%positive).
Fixpoint lots_data_at n sh v :=
match n with
| O => nil
| S n' => data_at sh t_struct_list (Vundef, Vint Int.zero) (force_ptr v) ::
lots_data_at n' sh v
end.
Definition test_semax sets temps_tycon temps_local vars_local seps :=
forall post v sh, (semax
(mk_tycontext (lots_temps temps_tycon) (PTree.empty type) Tvoid
(PTree.empty type) (PTree.empty funspec))
(assertD [] (localD (lots_locals temps_local) (lots_vars vars_local))
(lots_data_at seps sh v))
(lots_of_sets sets)
(normal_ret_assert post)).
Goal test_semax 1 1 0 0 0.
cbv [ test_semax lots_temps lots_temps' PTree.empty
lots_of_sets lots_of_sets' lots_data_at Pos.succ PTree.set
lots_locals lots_locals' lots_vars lots_vars' pred].
intros.
Clear Timing Profile.
rforward.
Print Timing Profile.
(* 02 match_tactic: (total:0.003328, mean:0.003328, runs:1, sigma2:0.000000)
03 reification: (total:1.787002, mean:1.787002, runs:1, sigma2:0.000000)
04 match type: (total:0.007306, mean:0.007306, runs:1, sigma2:0.000000)
05 vm_compute: (total:0.690385, mean:0.690385, runs:1, sigma2:0.000000)
06 match result: (total:0.015118, mean:0.015118, runs:1, sigma2:0.000000)
07 goalD: (total:0.083754, mean:0.083754, runs:1, sigma2:0.000000)
08 reduce: (total:0.306093, mean:0.306093, runs:1, sigma2:0.000000)
09 cut1: (total:0.154493, mean:0.154493, runs:1, sigma2:0.000000)
10 change: (total:0.000002, mean:0.000002, runs:1, sigma2:0.000000)
11 cut2: (total:0.619691, mean:0.619691, runs:1, sigma2:0.000000)
12 exact: (total:0.326034, mean:0.326034, runs:1, sigma2:0.000000)
13 VM_CAST: (total:0.255638, mean:0.255638, runs:1, sigma2:0.000000)
total: (total:4.307944, mean:4.307944, runs:1, sigma2:0.000000) *)
Show Proof.
(* for a small goal:
(fun (post : environ -> mpred) (v : val) (sh : Share.t) =>
let tbl :=
FMapPositive.PositiveMap.Node
(FMapPositive.PositiveMap.Node
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ))
(Some (elem_ctor (tyArr tyenviron tympred) post))
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ)))
(Some (elem_ctor tyOracleKind NullExtension.Espec))
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ)) in
let e :=
App
(App
(App
(App (App (Inj (inr (Smx fsemax))) (Ext 1%positive))
(App
(Inj
(inr
(Smx
(ftycontext
(PTree.Node PTree.Leaf
(Some (tptr t_struct_list, true)) PTree.Leaf)
PTree.Leaf Tvoid PTree.Leaf))))
(Inj (inr (Data (fleaf tyfunspec))))))
(App
(App
(App (Inj (inr (Smx fassertD)))
(Inj (inr (Data (fnil typrop)))))
(App
(App (Inj (inr (Smx flocalD)))
(Inj (inr (Data (fleaf tyval)))))
(Inj (inr (Data (fleaf (typrod tyc_type tyval)))))))
(Inj (inr (Data (fnil tympred))))))
(Inj
(inr
(Smx
(fstatement
(Sset 1%positive
(Ecast (Econst_int (Int.repr 0) tint) (tptr tvoid))))))))
(App (Inj (inr (Smx fnormal_ret_assert))) (Ext 2%positive)) in
let sv := TopSubst (expr typ func) [] [] in
(fun
H : forall x : environ,
assertD []
(localD
(PTree.set 1
(eval_cast
(Tint I32 Signed
{| attr_volatile := false; attr_alignas := None |})
(Tpointer Tvoid
{| attr_volatile := false; attr_alignas := None |})
(Vint
{|
Int.intval := 0;
Int.intrange := Int.Z_mod_modulus_range' 0 |}))
PTree.Leaf) PTree.Leaf) [] x |-- post x =>
(fun
H0 : run_tac'
(SYMEXE_TAC_n 1000
(FMapPositive.PositiveMap.Node
(FMapPositive.PositiveMap.Node
(FMapPositive.PositiveMap.Leaf
(SymEnv.function RType_typ))
(Some (elem_ctor (tyArr tyenviron tympred) post))
(FMapPositive.PositiveMap.Leaf
(SymEnv.function RType_typ)))
(Some (elem_ctor tyOracleKind NullExtension.Espec))
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ))))
(GGoal e) =
More_ sv
(GGoal
(App
(Inj
(inl
(inl
(inr
(ModularFunc.ILogicFunc.ilf_forall tyenviron
typrop)))))
(Abs tyenviron
(App
(App
(Inj
(inl
(inl
(inr
(ModularFunc.ILogicFunc.ilf_entails
tympred)))))
(App
(App
(App
(App (Inj (inr (Smx fassertD)))
(Inj (inr (Data (fnil typrop)))))
(App
(App (Inj (inr (Smx flocalD)))
(App
(App
(Inj
(inr (Data (fset tyval 1))))
(App
(Inj (inr (Eval_f (..))))
(App
(Inj (inr (..)))
(Inj (inr (..))))))
(Inj (inr (Data (fleaf tyval))))))
(Inj
(inr
(Data
(fleaf
(typrod tyc_type tyval)))))))
(Inj (inr (Data (fnil tympred)))))
(Var 0%nat)))
(App (Inj (inl (inl (inl 2%positive)))) (Var 0%nat)))))) =>
run_rtac_More
(FMapPositive.PositiveMap.Node
(FMapPositive.PositiveMap.Node
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ))
(Some (elem_ctor (tyArr tyenviron tympred) post))
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ)))
(Some (elem_ctor tyOracleKind NullExtension.Espec))
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ)))
(SYMEXE_TAC_n 1000
(FMapPositive.PositiveMap.Node
(FMapPositive.PositiveMap.Node
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ))
(Some (elem_ctor (tyArr tyenviron tympred) post))
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ)))
(Some (elem_ctor tyOracleKind NullExtension.Espec))
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ)))) sv
(GGoal
(App
(Inj
(inl
(inl
(inr (ModularFunc.ILogicFunc.ilf_forall tyenviron typrop)))))
(Abs tyenviron
(App
(App
(Inj
(inl
(inl
(inr
(ModularFunc.ILogicFunc.ilf_entails tympred)))))
(App
(App
(App
(App (Inj (inr (Smx fassertD)))
(Inj (inr (Data (fnil typrop)))))
(App
(App (Inj (inr (Smx flocalD)))
(App
(App (Inj (inr (Data (fset tyval 1))))
(App
(Inj
(inr
(Eval_f
(feval_cast
(Tint I32 Signed ..)
(Tpointer Tvoid ..)))))
(App (Inj (inr (Value fVint)))
(Inj (inr (Const (fint ..)))))))
(Inj (inr (Data (fleaf tyval))))))
(Inj
(inr
(Data (fleaf (typrod tyc_type tyval)))))))
(Inj (inr (Data (fnil tympred)))))
(Var 0%nat)))
(App (Inj (inl (inl (inl 2%positive)))) (Var 0%nat)))))) e
(SYMEXE_sound 1000
(FMapPositive.PositiveMap.Node
(FMapPositive.PositiveMap.Node
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ))
(Some (elem_ctor (tyArr tyenviron tympred) post))
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ)))
(Some (elem_ctor tyOracleKind NullExtension.Espec))
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ)))) H0)
(eq_refl
<:run_tac'
(SYMEXE_TAC_n 1000
(FMapPositive.PositiveMap.Node
(FMapPositive.PositiveMap.Node
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ))
(Some (elem_ctor (tyArr tyenviron tympred) post))
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ)))
(Some (elem_ctor tyOracleKind NullExtension.Espec))
(FMapPositive.PositiveMap.Leaf (SymEnv.function RType_typ))))
(GGoal e) =
More_ sv
(GGoal
(App
(Inj
(inl
(inl
(inr
(ModularFunc.ILogicFunc.ilf_forall tyenviron
typrop)))))
(Abs tyenviron
(App
(App
(Inj
(inl
(inl
(inr
(ModularFunc.ILogicFunc.ilf_entails
tympred)))))
(App
(App
(App
(App (Inj (inr (Smx fassertD)))
(Inj (inr (Data (fnil typrop)))))
(App
(App (Inj (inr (Smx flocalD)))
(App
(App
(Inj (inr (Data (fset tyval 1))))
(App
(Inj
(inr
(Eval_f
(feval_cast (..) (..)))))
(App
(Inj (inr (Value fVint)))
(Inj (inr (Const (..)))))))
(Inj (inr (Data (fleaf tyval))))))
(Inj
(inr
(Data
(fleaf (typrod tyc_type tyval)))))))
(Inj (inr (Data (fnil tympred)))))
(Var 0%nat)))
(App (Inj (inl (inl (inl 2%positive)))) (Var 0%nat)))))))
H) ?139) *)
admit.
Time Qed. (*109 seconds with change for 100 vars
123 seconds without change for 100 vars
310 seconds without change for 300 vars
297 seconds with change for 300 vars
*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment