From 9717179a5d60c3b8dd0e2d35c12b5be4cfb31113 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 28 May 2016 19:03:59 +0200 Subject: [PATCH] Add fine-grained stack --- F_mu_ref_par/examples/stack/FG_stack.v | 379 +++++++++++++++++++++++++ _CoqProject | 3 +- 2 files changed, 381 insertions(+), 1 deletion(-) create mode 100644 F_mu_ref_par/examples/stack/FG_stack.v diff --git a/F_mu_ref_par/examples/stack/FG_stack.v b/F_mu_ref_par/examples/stack/FG_stack.v new file mode 100644 index 0000000..d3e753b --- /dev/null +++ b/F_mu_ref_par/examples/stack/FG_stack.v @@ -0,0 +1,379 @@ +From iris.program_logic Require Import language. +From iris_logrel.F_mu_ref_par Require Import lang typing rules. + +Section FG_stack. + Context {Σ : gFunctors} {iI : heapIG Σ}. + + Definition FG_StackType τ := + (TRec (Tref (TSum TUnit (TProd τ.[ren (+1)] (TVar 0))))). + + (* Fine-grained push *) + Definition FG_push (st : expr) : expr := + Lam (App (Lam + (* try push *) + (If (CAS (st.[ren (+4)]) (Var 1) + (Fold (Alloc (InjR (Pair (Var 3) (Var 1))))) + ) + Unit (* push succeeds we return unit *) + (App (Var 2) (Var 3)) (* push fails, we try again *) + ) + ) + (Load st.[ren (+2)]) (* read the stack pointer *) + ). + + Lemma FG_push_folding (st : expr) : + FG_push st = + Lam (App (Lam + (* try push *) + (If (CAS (st.[ren (+4)]) (Var 1) + (Fold (Alloc (InjR (Pair (Var 3) (Var 1))))) + ) + Unit (* push succeeds we return unit *) + (App (Var 2) (Var 3)) (* push fails, we try again *) + ) + ) + (Load st.[ren (+2)]) (* read the stack pointer *) + ). + Proof. trivial. Qed. + + Section FG_push_type. + (* The following assumption is simply ** WRONG ** *) + (* We assume it though to just be able to prove that the + stack we are implementing is /type-sane/ so to speak! *) + Context (HEQTP : ∀ τ, EqType (FG_StackType τ)). + + Lemma FG_push_type st Γ τ : + typed Γ st (Tref (FG_StackType τ)) → + typed Γ (FG_push st) (TArrow τ TUnit). + Proof. + intros H1. repeat (econstructor; eauto using HEQTP). + - eapply (context_weakening [_; _; _; _]); eauto. + - by asimpl. + - eapply (context_weakening [_; _]); eauto. + Qed. + + End FG_push_type. + + Definition FG_pushV (st : expr) : val := + LamV (App (Lam + (* try push *) + (If (CAS (st.[ren (+4)]) (Var 1) + (Fold (Alloc (InjR (Pair (Var 3) (Var 1))))) + ) + Unit (* push succeeds we return unit *) + (App (Var 2) (Var 3)) (* push fails, we try again *) + ) + ) + (Load st.[ren (+2)]) (* read the stack pointer *) + ). + + Lemma FG_push_to_val st : to_val (FG_push st) = Some (FG_pushV st). + Proof. trivial. Qed. + + Lemma FG_push_of_val st : of_val (FG_pushV st) = FG_push st. + Proof. trivial. Qed. + + Global Opaque FG_pushV. + + Lemma FG_push_closed (st : expr) : + (∀ f, st.[f] = st) → ∀ f, (FG_push st).[f] = FG_push st. + Proof. intros H f. asimpl. unfold FG_push. rewrite ?H; trivial. Qed. + + Lemma FG_push_subst (st : expr) f : + (FG_push st).[f] = FG_push st.[f]. + Proof. unfold FG_push. by asimpl. Qed. + + Global Opaque FG_push. + + (* Fine-grained push *) + Definition FG_pop (st : expr) : expr := + Lam (App (Lam + (App + (Lam + ( + Case (Var 1) + (InjL Unit) + ( (* try popping *) + If + (CAS + (st.[ren (+7)]) + (Fold (Var 4)) + (Snd (Var 0)) + ) + (InjR (Fst (Var 0))) (* pop succeeds *) + (App (Var 5) (Var 6)) (* pop fails, we retry*) + ) + ) + ) + ( + (Load (Var 1)) + ) + ) + ) + (Unfold (Load st.[ren (+ 2)])) + ). + + Lemma FG_pop_folding (st : expr) : + FG_pop st = + Lam (App (Lam + ( App + (Lam + ( + Case (Var 1) + (InjL Unit) + ( (* try popping *) + If + (CAS + (st.[ren (+7)]) + (Fold (Var 4)) + (Snd (Var 0)) + ) + (InjR (Fst (Var 0))) (* pop succeeds *) + (App (Var 5) (Var 6)) (* pop fails, we retry*) + ) + ) + ) + ( + (Load (Var 1)) + ) + ) + ) + (Unfold (Load st.[ren (+ 2)])) + ). + Proof. trivial. Qed. + + Section FG_pop_type. + (* The following assumption is simply ** WRONG ** *) + (* We assume it though to just be able to prove that the + stack we are implementing is /type-sane/ so to speak! *) + Context (HEQTP : ∀ τ, EqType (FG_StackType τ)). + + Lemma FG_pop_type st Γ τ : + typed Γ st (Tref (FG_StackType τ)) → + typed Γ (FG_pop st) (TArrow TUnit (TSum TUnit τ)). + Proof. + intros H1. repeat (econstructor; eauto using HEQTP). + - eapply (context_weakening [_; _; _; _; _; _; _]); eauto. + - asimpl; trivial. + - eapply (context_weakening [_; _]); eauto. + Qed. + + End FG_pop_type. + + Definition FG_popV (st : expr) : val := + LamV + (App + (Lam + ( App + (Lam + ( + Case (Var 1) + (InjL Unit) + ( (* try popping *) + If + (CAS + (st.[ren (+7)]) + (Fold (Var 4)) + (Snd (Var 0)) + ) + (InjR (Fst (Var 0))) (* pop succeeds *) + (App (Var 5) (Var 6)) (* pop fails, we retry*) + ) + ) + ) + ( + (Load (Var 1)) + ) + ) + ) + (Unfold (Load st.[ren (+ 2)])) + ). + + Lemma FG_pop_to_val st : to_val (FG_pop st) = Some (FG_popV st). + Proof. trivial. Qed. + + Lemma FG_pop_of_val st : of_val (FG_popV st) = FG_pop st. + Proof. trivial. Qed. + + Global Opaque FG_popV. + + Lemma FG_pop_closed (st : expr) : + (∀ f, st.[f] = st) → ∀ f, (FG_pop st).[f] = FG_pop st. + Proof. intros H f. asimpl. unfold FG_pop. rewrite ?H; trivial. Qed. + + Lemma FG_pop_subst (st : expr) f : + (FG_pop st).[f] = FG_pop st.[f]. + Proof. unfold FG_pop. by asimpl. Qed. + + Global Opaque FG_pop. + + (* Fine-grained iter *) + Definition FG_iter (f : expr) : expr := + Lam + (Case (Load (Unfold (Var 1))) + Unit + (App (Lam (App (Var 3) (Snd (Var 2)))) (* recursive_call *) + (App f.[ren (+3)] (Fst (Var 0))) + ) + ). + + Lemma FG_iter_folding (f : expr) : + FG_iter f = + Lam + (Case (Load (Unfold (Var 1))) + Unit + (App (Lam (App (Var 3) (Snd (Var 2)))) (* recursive_call *) + (App f.[ren (+3)] (Fst (Var 0))) + ) + ). + Proof. trivial. Qed. + + Lemma FG_iter_type f Γ τ : + typed Γ f (TArrow τ TUnit) → + typed Γ (FG_iter f) (TArrow (FG_StackType τ) TUnit). + Proof. + intros H1. + econstructor. + eapply (Case_typed _ _ _ _ TUnit); + [| repeat constructor + | repeat econstructor; eapply (context_weakening [_; _; _]); eauto]. + econstructor. + replace (Tref (TSum TUnit (TProd τ (FG_StackType τ)))) with + ((Tref (TSum TUnit (TProd τ.[ren(+1)] (TVar 0)))).[(FG_StackType τ)/]) + by (by asimpl). + repeat econstructor. + Qed. + + Definition FG_iterV (f : expr) : val := + LamV + (Case (Load (Unfold (Var 1))) + Unit + (App (Lam (App (Var 3) (Snd (Var 2)))) (* recursive_call *) + (App f.[ren (+3)] (Fst (Var 0))) + ) + ). + + Lemma FG_iter_to_val st : to_val (FG_iter st) = Some (FG_iterV st). + Proof. trivial. Qed. + + Lemma FG_iter_of_val st : of_val (FG_iterV st) = FG_iter st. + Proof. trivial. Qed. + + Global Opaque FG_popV. + + Lemma FG_iter_closed (f : expr) : + (∀ g, f.[g] = f) → ∀ g, (FG_iter f).[g] = FG_iter f. + Proof. intros H g. asimpl. unfold FG_iter. rewrite ?H; trivial. Qed. + + Lemma FG_iter_subst (f : expr) g : + (FG_iter f).[g] = FG_iter f.[g]. + Proof. unfold FG_iter. by asimpl. Qed. + + Global Opaque FG_iter. + + Definition FG_read_iter (st : expr) : expr := + Lam (App (FG_iter (Var 1)) (Load st.[ren (+2)])). + + Lemma FG_read_iter_type st Γ τ : + typed Γ st (Tref (FG_StackType τ)) → + typed Γ (FG_read_iter st) + (TArrow (TArrow τ TUnit) TUnit). + Proof. + intros H1; repeat econstructor. + - eapply FG_iter_type; by constructor. + - by eapply (context_weakening [_;_]). + Qed. + + Transparent FG_iter. + + Lemma FG_read_iter_closed (st : expr) : + (∀ f, st.[f] = st) → + ∀ f, (FG_read_iter st).[f] = FG_read_iter st. + Proof. + intros H1 f. unfold FG_read_iter, FG_iter. asimpl. + by rewrite ?H1. + Qed. + + Lemma FG_read_iter_subst (st : expr) g : + (FG_read_iter st).[g] = FG_read_iter st.[g]. + Proof. by unfold FG_read_iter; asimpl. Qed. + + Global Opaque FG_iter. + + Definition FG_stack_body (st : expr) : expr := + Pair (Pair (FG_push st) (FG_pop st)) (FG_read_iter st). + + Section FG_stack_body_type. + (* The following assumption is simply ** WRONG ** *) + (* We assume it though to just be able to prove that the + stack we are implementing is /type-sane/ so to speak! *) + Context (HEQTP : ∀ τ, EqType (FG_StackType τ)). + + Lemma FG_stack_body_type st Γ τ : + typed Γ st (Tref (FG_StackType τ)) → + typed Γ (FG_stack_body st) + (TProd + (TProd (TArrow τ TUnit) (TArrow TUnit (TSum TUnit τ))) + (TArrow (TArrow τ TUnit) TUnit) + ). + Proof. + intros H1. + repeat (econstructor; eauto using FG_push_type, + FG_pop_type, FG_read_iter_type). + Qed. + + End FG_stack_body_type. + + Opaque FG_read_iter. + + Lemma FG_stack_body_closed (st : expr) : + (∀ f, st.[f] = st) → + ∀ f, (FG_stack_body st).[f] = FG_stack_body st. + Proof. + intros H1 f. unfold FG_stack_body. asimpl. + rewrite FG_push_closed; trivial. + rewrite FG_pop_closed; trivial. + by rewrite FG_read_iter_closed. + Qed. + + Definition FG_stack : expr := + TLam (App (Lam (FG_stack_body (Var 1))) + (Alloc (Fold (Alloc (InjL Unit))))). + + Section FG_stack_type. + (* The following assumption is simply ** WRONG ** *) + (* We assume it though to just be able to prove that the + stack we are implementing is /type-sane/ so to speak! *) + Context (HEQTP : ∀ τ, EqType (FG_StackType τ)). + + Lemma FG_stack_type Γ : + typed Γ (FG_stack) + (TForall + (TProd + (TProd + (TArrow (TVar 0) TUnit) + (TArrow TUnit (TSum TUnit (TVar 0))) + ) + (TArrow (TArrow (TVar 0) TUnit) TUnit) + )). + Proof. + repeat econstructor. + - eapply FG_push_type; try constructor; simpl; eauto. + - eapply FG_pop_type; try constructor; simpl; eauto. + - eapply FG_read_iter_type; constructor; by simpl. + - asimpl. repeat constructor. + Qed. + + End FG_stack_type. + + Lemma FG_stack_closed f : + FG_stack.[f] = FG_stack. + Proof. + unfold FG_stack. + asimpl; rewrite ?FG_push_subst ?FG_pop_subst. + asimpl. rewrite ?FG_read_iter_subst. by asimpl. + Qed. + + Transparent FG_read_iter. + +End FG_stack. \ No newline at end of file diff --git a/_CoqProject b/_CoqProject index eaac5bd..a7e0bca 100644 --- a/_CoqProject +++ b/_CoqProject @@ -31,4 +31,5 @@ F_mu_ref_par/soundness_binary.v F_mu_ref_par/examples/lock.v F_mu_ref_par/examples/counter.v F_mu_ref_par/examples/stack/stack_rules.v -F_mu_ref_par/examples/stack/CG_stack.v \ No newline at end of file +F_mu_ref_par/examples/stack/CG_stack.v +F_mu_ref_par/examples/stack/FG_stack.v \ No newline at end of file -- GitLab