From fbb63c51b2e5fe7298a7e51c3b22e1504effc387 Mon Sep 17 00:00:00 2001 From: berpeti Date: Thu, 9 Oct 2025 11:48:49 +0200 Subject: [PATCH 1/7] Describe dead code elimination in c_seq --- src/FrameStack/Optimisations/SeqDeadCode.v | 232 +++++++++++++++++++++ 1 file changed, 232 insertions(+) create mode 100644 src/FrameStack/Optimisations/SeqDeadCode.v diff --git a/src/FrameStack/Optimisations/SeqDeadCode.v b/src/FrameStack/Optimisations/SeqDeadCode.v new file mode 100644 index 0000000..864812e --- /dev/null +++ b/src/FrameStack/Optimisations/SeqDeadCode.v @@ -0,0 +1,232 @@ +From CoreErlang.FrameStack Require Import SubstSemanticsLemmas + CIU + CTX + Compatibility. + +Import ListNotations. + +Definition is_exit_bif (modu func : string) (n : nat) : bool := +match convert_string_to_code (modu, func) with +| BThrow | BExit => Nat.eqb n 1 +| BError => Nat.eqb n 1 || Nat.eqb n 2 +| _ => false +end. + +Definition is_safe (modu func : string) (n : nat) : bool := +match convert_string_to_code (modu, func) with +| BEq | BTypeEq | BNeq | BTypeNeq +| BLe | BLt | BGe | BGt => Nat.eqb n 2 +(**) +| BIsAtom | BIsNumber | BIsBoolean | BIsInteger => Nat.eqb n 1 +(* TODO: rest of the bifs in erl_bifs.erl *) +| _ => false +end. + +Fixpoint will_fail (e : Exp) : bool := +match e with +| ELet _ e1 e2 => will_fail e1 || will_fail e2 +| EPrimOp name _ => match convert_primop_to_code name with + | PMatchFail => true + | _ => false + end +| ECall (VVal (VLit (Atom modu))) (VVal (VLit (Atom func))) args => + is_exit_bif modu func (length args) +| _ => false +end. + +Fixpoint is_safe_simple (e : Exp) : bool := +match e with +| VVal (VLit _) => true +| VVal (VFunId _) => false +| VVal (VVar _) => true +| EExp (ECons e1 e2) => is_safe_simple e1 && is_safe_simple e2 +| EExp (ETuple l) => forallb is_safe_simple l +| EExp (ECall (VVal (VLit (Atom modu))) (VVal (VLit (Atom func))) args) => + is_safe modu func (length args) (* TODO: missing parts *) +| _ => false +end. + +Fixpoint seq_elim (e : Exp) : Exp := +(* match fuel with + | O => e (* out of fuel: return original expression unchanged *) + | S => *) + match e with + | VVal v => VVal v + | EExp nv => + match nv with + | EFun vl body => + EExp (EFun vl (seq_elim body)) + | EValues l => + EExp (EValues (map (fun x => seq_elim x) l)) + | ECons hd tl => + EExp (ECons (seq_elim hd) (seq_elim tl)) + | ETuple l => + EExp (ETuple (map (fun x => seq_elim x) l)) + | EMap l => + EExp (EMap (map (fun '(a,b) => (seq_elim a, seq_elim b)) l)) + | ECall m f l => + EExp (ECall (seq_elim m) (seq_elim f) (map (fun x => seq_elim x) l)) + | EPrimOp fn l => + EExp (EPrimOp fn (map (fun x => seq_elim x) l)) + | EApp e0 l => + EExp (EApp (seq_elim e0) (map (fun x => seq_elim x) l)) + | ECase e0 branches => + let e0' := seq_elim e0 in + let branches' := map (fun '(p,g,b) => (p, seq_elim g, seq_elim b)) branches in + EExp (ECase e0' branches') + | ELet n e1 e2 => + EExp (ELet n (seq_elim e1) (seq_elim e2)) + | ESeq e1 e2 => + (* First fold the left part *) + let e1' := seq_elim e1 in + let e2' := seq_elim e2 in + if will_fail e1' then e1' + else + match is_safe_simple e1', is_safe_simple e2' with + | true, _ => e2' + | false, true => e1' + | false, false => ESeq e1' e2' + end + | ELetRec l ebody => + let l' := map (fun '(n, e0) => (n, seq_elim e0)) l in + EExp (ELetRec l' (seq_elim ebody)) + | ETry e1 vl1 e2 vl2 e3 => + EExp (ETry (seq_elim e1) vl1 (seq_elim e2) vl2 (seq_elim e3)) + end + end +(* end *). + +Fixpoint size_val (v : Val) : nat := + match v with + | VNil => 1 + | VLit _ => 1 + | VPid _ => 1 + | VCons hd tl => 1 + size_val hd + size_val tl + | VTuple l => 1 + fold_left (fun acc v => acc + size_val v) l 0 + | VMap pairs => 1 + fold_left (fun acc '(a,b) => acc + size_val a + size_val b) pairs 0 + | VVar _ => 1 + | VFunId _ => 1 + | VClos ext _ _ e => 1 + fold_left (fun acc '(_,_,e0) => acc + size_exp e0) ext 0 + size_exp e + end +with size_exp (e : Exp) : nat := + match e with + | VVal v => 1 + size_val v + | EExp nv => 1 + size_nonval nv + end +with size_nonval (nv : NonVal) : nat := + match nv with + | EFun _ e => size_exp e + | EValues l => fold_left (fun acc e => acc + size_exp e) l 0 + | ECons hd tl => size_exp hd + size_exp tl + | ETuple l => fold_left (fun acc e => acc + size_exp e) l 0 + | EMap l => fold_left (fun acc '(a,b) => acc + size_exp a + size_exp b) l 0 + | ECall m f l => size_exp m + size_exp f + fold_left (fun acc e => acc + size_exp e) l 0 + | EPrimOp _ l => fold_left (fun acc e => acc + size_exp e) l 0 + | EApp e l => size_exp e + fold_left (fun acc e => acc + size_exp e) l 0 + | ECase e branches => size_exp e + fold_left (fun acc '(_,g,b) => acc + size_exp g + size_exp b) branches 0 + | ELet _ e1 e2 => size_exp e1 + size_exp e2 + | ESeq e1 e2 => size_exp e1 + size_exp e2 + | ELetRec l e => fold_left (fun acc '(_,e0) => acc + size_exp e0) l 0 + size_exp e + | ETry e1 _ e2 _ e3 => size_exp e1 + size_exp e2 + size_exp e3 + end. + +Lemma closed_seq_elim Γ e : + EXP Γ ⊢ e -> EXP Γ ⊢ (seq_elim e). +Proof. +Admitted. + +Lemma will_fail_exception : + forall e, will_fail e -> + exists exc, ⟨[], e⟩ -->* RExc exc. +Proof. + +Admitted. + +Require Import SubstSemanticsLabeled. +Lemma is_safe_simple_no_effects: + forall e, is_safe_simple e -> + exists vs, ⟨[], e⟩ -[ [] ]->ₗ* ⟨[], RValSeq vs⟩. +Proof. + +Admitted. + +Lemma eval_seq_optim_1 : + forall e1 e2 res, + ⟨ [], (° ESeq e1 e2)⟩ -->* res -> + ⟨ [], (if will_fail (seq_elim e1) + then seq_elim e1 + else + if is_safe_simple (seq_elim e1) + then seq_elim e2 + else + if is_safe_simple (seq_elim e2) + then seq_elim e1 + else ° ESeq (seq_elim e1) (seq_elim e2)) ⟩ -->* res. +Proof. + +Admitted. + +Lemma eval_seq_optim_2 : + forall e1 e2 res, + ⟨ [], (if will_fail (seq_elim e1) + then seq_elim e1 + else + if is_safe_simple (seq_elim e1) + then seq_elim e2 + else + if is_safe_simple (seq_elim e2) + then seq_elim e1 + else ° ESeq (seq_elim e1) (seq_elim e2)) ⟩ -->* res + -> + ⟨ [], (° ESeq e1 e2)⟩ -->* res. +Proof. + +Admitted. + +Theorem seq_optim Γ (e : Exp) : + EXP Γ ⊢ e -> + CIU_open Γ e (seq_elim e). +Proof. + remember (size_exp e) as n. + assert (size_exp e <= n) by lia. clear Heqn. + revert e H Γ. + induction n using lt_wf_ind. destruct e; simpl; intros. + { apply CIU_iff_Rrel. auto. } + pose proof CIU_IsPreCtxRel as CONG. + destruct e; simpl. + * apply CONG; auto. + - by destruct_scopes. + - apply closed_seq_elim. by destruct_scopes. + - eapply H. 2: reflexivity. 2: by destruct_scopes. + simpl in H0. lia. + * admit. + * admit. + * admit. + * admit. + * admit. + * admit. + * admit. + * admit. + * admit. + * split. 2: split. + - apply -> subst_preserves_scope_red. 2: exact H2. scope_solver. + - apply -> subst_preserves_scope_red. 2: exact H2. + repeat case_match. + 1-3: constructor; apply closed_seq_elim; by destruct_scopes. + do 3 constructor; + destruct_scopes; + by apply closed_seq_elim. + - intros. destruct H4. + simpl in *. + + * admit. + * admit. +Admitted. + +Theorem seq_optim (e : Exp) : + EXPCLOSED e -> + CIU (seq_elim e) e. +Proof. + +Qed. + From b95fcefed819c74c8760af7d0b421eef3c2c0fa2 Mon Sep 17 00:00:00 2001 From: berpeti Date: Tue, 14 Oct 2025 15:47:20 +0200 Subject: [PATCH 2/7] Major progress with helpers to seq optim --- src/FrameStack/Optimisations/SeqDeadCode.v | 446 +++++++++++++++++++-- 1 file changed, 404 insertions(+), 42 deletions(-) diff --git a/src/FrameStack/Optimisations/SeqDeadCode.v b/src/FrameStack/Optimisations/SeqDeadCode.v index 864812e..8921414 100644 --- a/src/FrameStack/Optimisations/SeqDeadCode.v +++ b/src/FrameStack/Optimisations/SeqDeadCode.v @@ -1,7 +1,8 @@ -From CoreErlang.FrameStack Require Import SubstSemanticsLemmas +From CoreErlang.FrameStack Require Export SubstSemanticsLemmas CIU CTX Compatibility. +Require Export Basics. Import ListNotations. @@ -36,9 +37,9 @@ end. Fixpoint is_safe_simple (e : Exp) : bool := match e with -| VVal (VLit _) => true | VVal (VFunId _) => false -| VVal (VVar _) => true +| VVal (VVar _) => true +| VVal _ => true | EExp (ECons e1 e2) => is_safe_simple e1 && is_safe_simple e2 | EExp (ETuple l) => forallb is_safe_simple l | EExp (ECall (VVal (VLit (Atom modu))) (VVal (VLit (Atom func))) args) => @@ -82,10 +83,11 @@ Fixpoint seq_elim (e : Exp) : Exp := let e2' := seq_elim e2 in if will_fail e1' then e1' else - match is_safe_simple e1', is_safe_simple e2' with - | true, _ => e2' - | false, true => e1' - | false, false => ESeq e1' e2' + match is_safe_simple e1' (* , is_safe_simple e2' *) with + | true (* , _ *) => e2' + (* | false, true => e1' <- this only needs to be done + when using 'effect' *) + | false (* , false *) => ESeq e1' e2' end | ELetRec l ebody => let l' := map (fun '(n, e0) => (n, seq_elim e0)) l in @@ -97,17 +99,17 @@ Fixpoint seq_elim (e : Exp) : Exp := (* end *). Fixpoint size_val (v : Val) : nat := - match v with + 1 (* match v with | VNil => 1 | VLit _ => 1 | VPid _ => 1 | VCons hd tl => 1 + size_val hd + size_val tl - | VTuple l => 1 + fold_left (fun acc v => acc + size_val v) l 0 - | VMap pairs => 1 + fold_left (fun acc '(a,b) => acc + size_val a + size_val b) pairs 0 + | VTuple l => 1 + list_sum (map size_val l) + | VMap pairs => 1 + list_sum (map (fun '(a, b) => size_val a + size_val b) pairs) | VVar _ => 1 | VFunId _ => 1 | VClos ext _ _ e => 1 + fold_left (fun acc '(_,_,e0) => acc + size_exp e0) ext 0 + size_exp e - end + end *) with size_exp (e : Exp) : nat := match e with | VVal v => 1 + size_val v @@ -116,41 +118,240 @@ with size_exp (e : Exp) : nat := with size_nonval (nv : NonVal) : nat := match nv with | EFun _ e => size_exp e - | EValues l => fold_left (fun acc e => acc + size_exp e) l 0 + | EValues l => list_sum (map size_exp l) | ECons hd tl => size_exp hd + size_exp tl - | ETuple l => fold_left (fun acc e => acc + size_exp e) l 0 - | EMap l => fold_left (fun acc '(a,b) => acc + size_exp a + size_exp b) l 0 - | ECall m f l => size_exp m + size_exp f + fold_left (fun acc e => acc + size_exp e) l 0 - | EPrimOp _ l => fold_left (fun acc e => acc + size_exp e) l 0 - | EApp e l => size_exp e + fold_left (fun acc e => acc + size_exp e) l 0 - | ECase e branches => size_exp e + fold_left (fun acc '(_,g,b) => acc + size_exp g + size_exp b) branches 0 + | ETuple l => list_sum (map size_exp l) + | EMap l => list_sum (map (fun '(a, b) => size_exp a + size_exp b) l) + | ECall m f l => size_exp m + size_exp f + list_sum (map size_exp l) + | EPrimOp _ l => list_sum (map size_exp l) + | EApp e l => size_exp e + list_sum (map size_exp l) + | ECase e branches => size_exp e + list_sum (map ( + fun '(p, g, e) => size_exp g + size_exp e + ) branches) | ELet _ e1 e2 => size_exp e1 + size_exp e2 | ESeq e1 e2 => size_exp e1 + size_exp e2 - | ELetRec l e => fold_left (fun acc '(_,e0) => acc + size_exp e0) l 0 + size_exp e + | ELetRec l e => list_sum (map (fun '(_, a) => size_exp a) l) + size_exp e | ETry e1 _ e2 _ e3 => size_exp e1 + size_exp e2 + size_exp e3 end. +Ltac do_step := econstructor; [constructor;auto| simpl]. + +Lemma will_fail_subst: + forall e ξ, + will_fail e = true -> + will_fail e.[ξ] = true. +Proof. + intro. remember (size_exp e) as n. + assert (size_exp e <= n) by lia. clear Heqn. + revert e H. + induction n using lt_wf_ind. destruct e; simpl; intros. + assumption. + destruct e; simpl in *; try assumption. + { + destruct m; simpl in *; try congruence. + destruct e; simpl in *; try congruence. + destruct l0; simpl in *; try congruence. + destruct f; simpl in *; try congruence. + destruct e; simpl in *; try congruence. + destruct l0; simpl in *; try congruence. + by rewrite length_map. + } + { + apply orb_true_iff in H1 as [H1 | H1]; eapply H in H1; try rewrite H1. + all: auto. + 1,3: lia. + by rewrite orb_comm. + } +Qed. + +Lemma is_safe_simple_subst: + forall e Γ ξ, + SUBSCOPE Γ ⊢ ξ ∷ 0 -> + EXP Γ ⊢ e -> + is_safe_simple e = true -> + is_safe_simple e.[ξ] = true. +Proof. + intro. remember (size_exp e) as n. + assert (size_exp e <= n) by lia. clear Heqn. + revert e H. + induction n using lt_wf_ind. destruct e; simpl; intros. + * destruct e; simpl in *; try assumption. + - inv H2. inv H6. specialize (H1 n0 ltac:(lia)). + destruct ξ. + + destruct v; try reflexivity. inv H1. lia. + + reflexivity. + - inv H3. + * destruct e; simpl in *; try assumption. + - apply andb_true_iff in H3 as [H3_1 H3_2]. + destruct_scopes. + eapply H in H3_1. eapply H in H3_2. by rewrite H3_1, H3_2. + all: try eassumption. + all: lia. + - apply forallb_forall. intros. + apply in_map_iff in H4 as [newx [Heq H4]]. subst. + eapply forallb_forall in H3. 2: exact H4. + eapply H; try eassumption. + + pose proof elem_of_list_split l newx. + apply elem_of_list_In in H4. + apply H5 in H4 as [? [? H4]]. subst l. + rewrite map_app, list_sum_app. slia. + + apply elem_of_list_In in H4. + inv H2. inv H7. apply indexed_to_forall in H6. + eapply list.Forall_forall in H6; eassumption. + - destruct m; simpl in *; try congruence. + destruct e; simpl in *; try congruence. + destruct l0; simpl in *; try congruence. + destruct f; simpl in *; try congruence. + destruct e; simpl in *; try congruence. + destruct l0; simpl in *; try congruence. + by rewrite length_map. +Qed. + Lemma closed_seq_elim Γ e : EXP Γ ⊢ e -> EXP Γ ⊢ (seq_elim e). Proof. Admitted. +Lemma subst_preserves_size : + forall e ξ, + size_exp (e.[ξ]) = size_exp e. +Proof. + +Admitted. + Lemma will_fail_exception : - forall e, will_fail e -> - exists exc, ⟨[], e⟩ -->* RExc exc. + forall e res, will_fail e = true -> + ⟨[], e⟩ -->* res -> + exists exc, res = RExc exc. Proof. - + intro. remember (size_exp e) as n. + assert (size_exp e <= n) by lia. clear Heqn. + revert e H. + induction n using lt_wf_ind. rename H into IH. + destruct e; simpl; try congruence. + destruct e; simpl; try congruence. + * destruct m; simpl; try congruence. + destruct e; simpl; try congruence. + destruct l0; simpl; try congruence. + destruct f; simpl; try congruence. + destruct e; simpl; try congruence. + destruct l0; simpl; try congruence. + intros Hsize ???. + destruct H0 as [k [Hres D]]. + inv D. inv_result. + inv H0. inv H1. + inv H0. inv H2. + inv H0. inv H1. + inv H0. inv H2. + inv H0. inv H1. + unfold is_exit_bif in H. case_match; try congruence. + - destruct l; simpl in H; try congruence. + destruct l; simpl in H; try congruence. + 2: destruct l; simpl in H; try congruence. + (* single param exception *) + + inv H0. + pose proof (proj1 (semantic_iff_termination k _ _) + (ex_intro _ res (conj Hres H2))) as TERM. + apply term_eval_empty in TERM as [rese [ke [Hrese [D Hlt]]]]. + eapply frame_indep_core in D. + pose proof (transitive_eval_rev_lt H2 Hlt D). simpl in H, D. + destruct rese; try by inv_result. + ** inv H. inv H3. + simpl in H11. unfold eval in H11. rewrite H1 in H11. + case_match; try congruence. + inv H11. inv H6. by eexists. inv H3. + ** inv H. inv H3. inv H6. by eexists. inv H. + (* two param exception *) + + inv H0. + pose proof (proj1 (semantic_iff_termination k _ _) + (ex_intro _ res (conj Hres H2))) as TERM. + apply term_eval_empty in TERM as [rese [ke [Hrese [D Hlt]]]]. + eapply frame_indep_core in D. + pose proof (transitive_eval_rev_lt H2 Hlt D). simpl in H, D. + destruct rese; try by inv_result. + ** inv H. inv H3. + pose proof (proj1 (semantic_iff_termination k0 _ _) + (ex_intro _ res (conj Hres H6))) as TERM. + apply term_eval_empty in TERM as [rese2 [ke2 [Hrese2 [D2 Hlt2]]]]. + eapply frame_indep_core in D2. + pose proof (transitive_eval_rev_lt H6 Hlt2 D2). + simpl in H, D2. + destruct rese2; try by inv_result. + -- inv H. inv H4. + simpl in H13. unfold eval in H13. rewrite H1 in H13. + case_match; try congruence. + inv H13. inv H8. by eexists. inv H4. + -- inv H. inv H4. inv H8. by eexists. inv H. + ** inv H. inv H3. inv H6. by eexists. inv H. + - destruct l; simpl in H; try congruence. + destruct l; simpl in H; try congruence. + (* single param exception - as above *) + inv H0. + pose proof (proj1 (semantic_iff_termination k _ _) + (ex_intro _ res (conj Hres H2))) as TERM. + apply term_eval_empty in TERM as [rese [ke [Hrese [D Hlt]]]]. + eapply frame_indep_core in D. + pose proof (transitive_eval_rev_lt H2 Hlt D). simpl in H, D. + destruct rese; try by inv_result. + + inv H. inv H3. + simpl in H11. unfold eval in H11. rewrite H1 in H11. + case_match; try congruence. + inv H11. inv H6. by eexists. inv H3. + + inv H. inv H3. inv H6. by eexists. inv H. + - destruct l; simpl in H; try congruence. + destruct l; simpl in H; try congruence. + (* single param exception - as above *) + inv H0. + pose proof (proj1 (semantic_iff_termination k _ _) + (ex_intro _ res (conj Hres H2))) as TERM. + apply term_eval_empty in TERM as [rese [ke [Hrese [D Hlt]]]]. + eapply frame_indep_core in D. + pose proof (transitive_eval_rev_lt H2 Hlt D). simpl in H, D. + destruct rese; try by inv_result. + + inv H. inv H3. + simpl in H11. unfold eval in H11. rewrite H1 in H11. + case_match; try congruence. + inv H11. inv H6. by eexists. inv H3. + + inv H. inv H3. inv H6. by eexists. inv H. + * intros Hsize ???. case_match; try congruence. + destruct H0 as [k [Hres D]]. + inv D. inv_result. + inv H0. inv H2. admit. (* DOABLE, by induction *) + * intros. destruct H1 as [k [Hres D]]. + inv D. inv_result. + inv H1. + pose proof (proj1 (semantic_iff_termination k0 _ _) + (ex_intro _ res (conj Hres H2))) as TERM. + apply term_eval_empty in TERM as [rese [ke [Hrese [D Hlt]]]]. + eapply frame_indep_core in D as D'. + pose proof (transitive_eval_rev_lt H2 Hlt D'). simpl in H, D'. + apply orb_true_iff in H0 as [|]. + - simpl in *. + specialize (IH (size_exp e1) ltac:(lia) e1 ltac:(lia) + rese H0 (ex_intro _ ke (conj Hrese D))) as [exc Hexc]. + subst. inv H1. inv H4. inv H7. + by eexists. + inv H1. + - simpl in *. inv Hrese. + + inv H1. inv H4. + inv H7. by eexists. inv H1. + + inv H1. inv H4. + ospecialize* (IH (size_exp e2) ltac:(lia) e2.[list_subst vs idsubst] _ + res _ (ex_intro _ k (conj Hres H7))). + ** rewrite subst_preserves_size. lia. + ** by rewrite will_fail_subst. + ** assumption. Admitted. Require Import SubstSemanticsLabeled. Lemma is_safe_simple_no_effects: - forall e, is_safe_simple e -> + forall e, is_safe_simple e = true -> exists vs, ⟨[], e⟩ -[ [] ]->ₗ* ⟨[], RValSeq vs⟩. Proof. Admitted. -Lemma eval_seq_optim_1 : +(* Lemma eval_seq_optim_1 : forall e1 e2 res, ⟨ [], (° ESeq e1 e2)⟩ -->* res -> ⟨ [], (if will_fail (seq_elim e1) @@ -181,24 +382,41 @@ Lemma eval_seq_optim_2 : ⟨ [], (° ESeq e1 e2)⟩ -->* res. Proof. -Admitted. +Admitted. *) -Theorem seq_optim Γ (e : Exp) : - EXP Γ ⊢ e -> - CIU_open Γ e (seq_elim e). +(* +This won't work, because bodies of binders (e.g., EFun) are not closed! + +Theorem seq_optim (e : Exp) : + EXPCLOSED e -> + CIU e (seq_elim e). Proof. remember (size_exp e) as n. assert (size_exp e <= n) by lia. clear Heqn. - revert e H Γ. + revert e H. induction n using lt_wf_ind. destruct e; simpl; intros. - { apply CIU_iff_Rrel. auto. } - pose proof CIU_IsPreCtxRel as CONG. + { apply CIU_iff_Rrel_closed. intros. apply Rrel_Fundamental_closed. + scope_solver. } destruct e; simpl. - * apply CONG; auto. + * apply CIU_iff_Rrel_closed. + intros. apply Rrel_exp_compat_closed. + apply Erel_Fun_compat_closed. - by destruct_scopes. - apply closed_seq_elim. by destruct_scopes. - eapply H. 2: reflexivity. 2: by destruct_scopes. simpl in H0. lia. +Qed. *) + +(* Lemma seq_elim_subst e ξ: + (seq_elim e).[ξ] = seq_elim (e.[ξ]). +Proof. + remember (size_exp e) as n. + assert (size_exp e <= n) by lia. clear Heqn. + revert e H ξ. + induction n using lt_wf_ind. destruct e; simpl; intros. + reflexivity. + destruct e; simpl in *; try assumption. + * erewrite H. reflexivity. 2: reflexivity. lia. * admit. * admit. * admit. @@ -208,17 +426,161 @@ Proof. * admit. * admit. * admit. - * split. 2: split. - - apply -> subst_preserves_scope_red. 2: exact H2. scope_solver. - - apply -> subst_preserves_scope_red. 2: exact H2. - repeat case_match. - 1-3: constructor; apply closed_seq_elim; by destruct_scopes. - do 3 constructor; - destruct_scopes; - by apply closed_seq_elim. - - intros. destruct H4. - simpl in *. + * case_match. 2: case_match. 3: case_match. + - eapply will_fail_subst in H1. + erewrite H in H1. rewrite H1. 3: reflexivity. 2: lia. + erewrite H. reflexivity. 2: reflexivity. lia. + - + * admit. + * admit. +Admitted. *) + +Lemma CIU_irrefl : + forall (e : Exception) (vs : ValSeq), + CIU e vs -> False. +Proof. + intros. destruct H as [? [? H]]. + Check FTry. + ospecialize* (H [FTry (length vs) (°inf) 3 (˝VNil)]). + * split. + - constructor; constructor. constructor. apply inf_scope. do 2 constructor. + - constructor; constructor. + * eexists. destruct e as [[? ?] ?]. constructor. + do 3 constructor. + * inv H. inv H2. + rewrite eclosed_ignores_sub in H10. 2: constructor; apply inf_scope. + by apply inf_diverges in H10. +Qed. +Theorem seq_optim Γ (e : Exp) : + EXP Γ ⊢ e -> + CIU_open Γ e (seq_elim e) /\ + CIU_open Γ (seq_elim e) e. (* both are needed in the ind hyps. *) +Proof. + remember (size_exp e) as n. + assert (size_exp e <= n) by lia. clear Heqn. + revert e H Γ. + induction n using lt_wf_ind. destruct e; simpl; intros. + { split. all: apply CIU_iff_Rrel; auto. } + pose proof CIU_IsPreCtxRel as CONG. + destruct e; simpl. + * split. + { apply CONG; auto. + - by destruct_scopes. + - apply closed_seq_elim. by destruct_scopes. + - eapply H. 2: reflexivity. 2: by destruct_scopes. + simpl in H0. lia. + } + { + apply CONG; auto. + - apply closed_seq_elim. by destruct_scopes. + - by destruct_scopes. + - eapply H. 2: reflexivity. 2: by destruct_scopes. + simpl in H0. lia. + } + * admit. + * admit. + * admit. + * admit. + * admit. + * admit. + * admit. + * admit. + * admit. + * split. + { + split. 2: split. + - apply -> subst_preserves_scope_red. 2: exact H2. scope_solver. + - apply -> subst_preserves_scope_red. 2: exact H2. + repeat case_match. + 1-2: constructor; apply closed_seq_elim; by destruct_scopes. + do 3 constructor; + destruct_scopes; + by apply closed_seq_elim. + - intros. destruct H4. + simpl in *. + inv H4. 2: inv_result. + case_match. + 2: case_match. + { + eapply will_fail_subst in H4 as H4'. + pose proof will_fail_exception (seq_elim e1).[ξ] H4' as [exc D1]. + destruct D1 as [n1 [Hres1 D1]]. + pose proof (H (size_exp e1) ltac:(lia) e1 ltac:(lia) Γ + ltac:(by destruct_scopes)) as [CIUe1_1 CIUe1_2]. + specialize (CIUe1_1 _ H2) as [_ [_ D3]]. + simpl in D3. destruct H3. + ospecialize *(D3 (FSeq e2.[ξ]::F)). + { split. constructor. 2: assumption. + * constructor. + clear -H1 H2. + destruct_scopes. + apply -> subst_preserves_scope_exp; eassumption. + * constructor. constructor. assumption. } + { eexists. exact H9. } + destruct D3. + eapply frame_indep_nil in D1 as D1'. + eapply term_step_term in H6. 2: exact D1'. + inv H6. + eexists. + eapply step_term_term_plus. + eapply frame_indep_nil in D1. exact D1. + exact H13. + } + { + eapply is_safe_simple_subst with (ξ := ξ) in H5. + apply is_safe_simple_no_effects in H5 as D. + destruct D as [vs [k1 D]]. + apply step_rt_labeled_to_unlabeled in D. + pose proof (H (size_exp e1) ltac:(lia) e1 ltac:(lia) Γ + ltac:(by destruct_scopes)) as [CIUe1_1 CIUe1_2]. + eapply term_eval_empty in H9 as D'. + destruct D' as [res [k1' [Hres [D' Hlt]]]]. + pose proof (CIUe1_1 _ H2). + pose proof (CIUe1_2 _ H2). + assert (CIU res vs /\ CIU vs res). { + clear -D D' H6 H7 H1 H2. + apply CIU_eval_base in D' as []. + 2: { destruct_scopes. constructor. + apply -> subst_preserves_scope_exp; eassumption. + } + apply CIU_eval_base in D as []. + 2: { destruct_scopes. constructor. + apply -> subst_preserves_scope_exp; try eassumption. + by apply closed_seq_elim. + } + split. + * pose proof (CIU_transitive_closed _ _ _ H0 H6). + pose proof (CIU_transitive_closed _ _ _ H5 H3). + assumption. + * pose proof (CIU_transitive_closed _ _ _ H7 H). + pose proof (CIU_transitive_closed _ _ _ H4 H5). + assumption. + } + eapply frame_indep_core in D'. + epose proof term_step_term _ _ _ _ H9 _ _ D'. + 2: eassumption. + 2: apply closed_seq_elim; by destruct_scopes. + simpl in *. + destruct res; try by inv_result. + 2: { + destruct H8 as [C1 C2]. + clear -C1. exfalso. + by apply CIU_irrefl in C1. + } + inv H10. + apply ex_intro with (x := k0) in H12. + pose proof (H (size_exp e2) ltac:(lia) e2 ltac:(lia) Γ + ltac:(by destruct_scopes)) as [CIUe2_1 CIUe2_2]. + eapply CIUe2_1; eassumption. + } + { + + } + } + { + admit. + } * admit. * admit. Admitted. From 99da305ce9e2253705a8d57ae050d8739e590e6c Mon Sep 17 00:00:00 2001 From: berpeti Date: Wed, 15 Oct 2025 17:10:47 +0200 Subject: [PATCH 3/7] Main foundations finished for seq optim correctness --- src/FrameStack/Optimisations/SeqDeadCode.v | 254 +++++++++++++++++++-- 1 file changed, 232 insertions(+), 22 deletions(-) diff --git a/src/FrameStack/Optimisations/SeqDeadCode.v b/src/FrameStack/Optimisations/SeqDeadCode.v index 8921414..922c224 100644 --- a/src/FrameStack/Optimisations/SeqDeadCode.v +++ b/src/FrameStack/Optimisations/SeqDeadCode.v @@ -6,6 +6,14 @@ Require Export Basics. Import ListNotations. +Lemma exp_params_eval (exps : list Exp) vals : + list_biforall (fun exp val => ⟨[], RExp exp⟩ -->* RValSeq [val]) exps vals -> + forall vals0 v Fs id, + exists k, ⟨FParams id vals0 exps :: Fs, RValSeq [v]⟩ -[k]-> + ⟨FParams id (vals0 ++ removelast (v::vals)) [] :: Fs, RValSeq [last vals v]⟩. +Proof. +Admitted. + Definition is_exit_bif (modu func : string) (n : nat) : bool := match convert_string_to_code (modu, func) with | BThrow | BExit => Nat.eqb n 1 @@ -43,7 +51,10 @@ match e with | EExp (ECons e1 e2) => is_safe_simple e1 && is_safe_simple e2 | EExp (ETuple l) => forallb is_safe_simple l | EExp (ECall (VVal (VLit (Atom modu))) (VVal (VLit (Atom func))) args) => - is_safe modu func (length args) (* TODO: missing parts *) + is_safe modu func (length args) (* TODO: missing parts *) && + forallb is_safe_simple args (* NOTE: this is missing from the compiler + which uses useless call elimination + instead *) | _ => false end. @@ -204,7 +215,17 @@ Proof. destruct f; simpl in *; try congruence. destruct e; simpl in *; try congruence. destruct l0; simpl in *; try congruence. - by rewrite length_map. + rewrite length_map. + apply andb_true_iff in H3 as []. + apply andb_true_iff. split. by idtac. + apply forallb_forall. intros. + apply in_map_iff in H5 as [? [? ?]]. subst. + apply forallb_forall with (x := x0) in H4; try assumption. + eapply H. 5: exact H4. 2: reflexivity. 2: eassumption. + + apply in_split in H6 as [? [? ?]]. subst l. + rewrite map_app, list_sum_app in H0. simpl in H0. lia. + + destruct_scopes. apply indexed_to_forall in H10. + by apply Forall_forall with (x := x0) in H10. Qed. Lemma closed_seq_elim Γ e : @@ -216,7 +237,6 @@ Lemma subst_preserves_size : forall e ξ, size_exp (e.[ξ]) = size_exp e. Proof. - Admitted. Lemma will_fail_exception : @@ -316,7 +336,40 @@ Proof. * intros Hsize ???. case_match; try congruence. destruct H0 as [k [Hres D]]. inv D. inv_result. - inv H0. inv H2. admit. (* DOABLE, by induction *) + inv H0. clear IH Hsize n. + revert k0 res Hres H2. + remember [] as vals. clear Heqvals. revert vals. + (* induction - TODO separate it *) + induction l; intros. + { (* empty par list remainder *) + inv H2. inv H. + cbn in H8. unfold primop_eval in H8. + unfold eval_primop_error in H8. + rewrite H1 in H8. + destruct vals; try congruence. + destruct vals; try congruence. + inv H8. inv H0. by eexists. inv H. + } + inv H2. inv H. + pose proof (proj1 (semantic_iff_termination k _ _) + (ex_intro _ res (conj Hres H0))) as TERM. + apply term_eval_empty in TERM as [resa [ka [Hresa [D Hlt]]]]. + eapply frame_indep_core in D as D'. + pose proof (transitive_eval_rev_lt H0 Hlt D'). simpl in H, D'. + inv Hresa. 1: { inv H. inv H3. inv H6. by eexists. inv H. } + clear D'. inv H. inv H3. + - (* more than 1 param in the remainder *) + ospecialize* (IHl _ _ _ Hres). + { econstructor. constructor. congruence. eassumption. } + assumption. + - (* only 1 param in the remainder - same as in empty list *) + cbn in H12. unfold primop_eval in H12. + unfold eval_primop_error in H12. + rewrite H1 in H12. + destruct vals; simpl in *; try congruence. + + inv H12. inv H6. by eexists. inv H. + + destruct (vals ++ [v]) eqn:ERROR; try congruence. + apply app_eq_nil in ERROR as []. inv H3. * intros. destruct H1 as [k [Hres D]]. inv D. inv_result. inv H1. @@ -341,15 +394,152 @@ Proof. ** rewrite subst_preserves_size. lia. ** by rewrite will_fail_subst. ** assumption. -Admitted. +Qed. + +Lemma is_safe_eval : + forall m f n, is_safe m f n = true -> forall vals, length vals = n -> + exists v eff, eval m f vals = Some (RValSeq [v], eff). +Proof. + intros. unfold is_safe in H. case_match; try congruence. + all: apply Nat.eqb_eq in H; subst. + all: destruct vals; try by simpl in H0; congruence. + all: destruct vals; try by simpl in H0; congruence. + all: try destruct vals; try by simpl in H0; congruence. + all: clear H0. + all: unfold eval; rewrite H1. + all: unfold eval_equality, eval_cmp, eval_check; rewrite H1. + all: case_match; try by do 2 eexists. + all: case_match; try by do 2 eexists. +Qed. Require Import SubstSemanticsLabeled. Lemma is_safe_simple_no_effects: - forall e, is_safe_simple e = true -> - exists vs, ⟨[], e⟩ -[ [] ]->ₗ* ⟨[], RValSeq vs⟩. + forall e res, is_safe_simple e = true -> + (* is_result res -> *) + ⟨[], e⟩ -->* res -> (* TODO: no side effects - labeled termination needed *) + exists v, res = RValSeq [v]. Proof. - -Admitted. + intro. remember (size_exp e) as n. + assert (size_exp e <= n) by lia. clear Heqn. + revert e H. + induction n using lt_wf_ind. rename H into IH. + destruct e; simpl; try congruence. + * intros. destruct H1 as [? [? ?]]. destruct e; try congruence. + all: inv H2; (try by inv_result); + inv H3; inv H4. + all: try by eexists. + all: inv H0. + * destruct e; simpl; try congruence. + - intros Hlt res Hsafe D. + apply andb_true_iff in Hsafe as [Hsafe1 Hsafe2]. + destruct D as [k [Hres D]]. + inv D. inv_result. + inv H. + pose proof (proj1 (semantic_iff_termination k0 _ _) + (ex_intro _ res (conj Hres H0))) as TERM. + apply term_eval_empty in TERM as [restl [ktl [Hrestl [D Hlt2]]]]. + eapply frame_indep_core in D as D'. + pose proof (transitive_eval_rev_lt H0 Hlt2 D'). simpl in H, D'. + eapply conj, ex_intro with (x := ktl), IH in D; try eassumption. + 2: lia. + destruct D as [vtl ?]. subst. clear D'. + inv H. inv H2. + pose proof (proj1 (semantic_iff_termination k _ _) + (ex_intro _ res (conj Hres H5))) as TERM. + apply term_eval_empty in TERM as [reshd [khd [Hreshd [D Hlt3]]]]. + eapply frame_indep_core in D as D'. + pose proof (transitive_eval_rev_lt H5 Hlt3 D'). simpl in H, D'. + eapply conj, ex_intro with (x := khd), IH in D; try eassumption. + 2: lia. + destruct D as [vhd ?]. subst. clear D'. + inv H. inv H3. inv H7. 2: { inv H. } by eexists. + - intros. destruct H1 as [k [Hres D]]. + inv D. inv_result. inv H1. + (* induction - TODO separate it *) + remember [] as vals in H2. clear Heqvals. + revert k0 vals res H2 Hres. + induction l; intros. + { (* final step *) + inv H2. inv H1. cbn in H9. inv H9. + inv H3. 2: { inv H1. } by eexists. + } + inv H2. inv H1. + pose proof (proj1 (semantic_iff_termination _ _ _) + (ex_intro _ res (conj Hres H3))) as TERM. + apply term_eval_empty in TERM as [resa [ka [Hresa [D Hlt3]]]]. + eapply frame_indep_core in D as D'. + pose proof (transitive_eval_rev_lt H3 Hlt3 D'). simpl in H1, D'. + clear D'. + eapply conj, ex_intro with (x := ka), IH in D as [va EQ]. + 5: assumption. + 3: reflexivity. + 2: { simpl in H. lia. } + 2: { simpl in H0. by apply andb_true_iff in H0 as []. } + subst. inv H1. inv H4. + + (* params remain *) + eapply IHl. + { simpl in *. lia. } + { simpl in *. by apply andb_true_iff in H0 as []. } + { econstructor. constructor. congruence. exact H7. } + { assumption. } + + (* final step *) + cbn in H13. inv H13. + inv H7. 2: { inv H1. } by eexists. + - intros. + destruct m; simpl; try congruence. + destruct e; simpl; try congruence. + destruct l0; simpl; try congruence. + destruct f; simpl; try congruence. + destruct e; simpl; try congruence. + destruct l0; simpl; try congruence. + apply andb_true_iff in H0 as []. + destruct H1 as [k [Hres D]]. + (* decompose evaluation *) + inv D. inv_result. inv H1. + inv H3. inv H1. + inv H4. inv H1. + inv H3. inv H1. + inv H4. inv H1. + (* induction - TODO separate it *) + remember [] as vals in H3. + assert (length l = length l + length vals) by (subst vals; slia). + clear Heqvals. rewrite H1 in H0. clear H1. + revert k0 vals res H3 Hres H0. + induction l; intros. + { (* final step *) + inv H3. inv H1. cbn in H10. + pose proof is_safe_eval _ _ _ H0 vals eq_refl as [v [eff ?]]. + rewrite H1 in H10. inv H10. + inv H4. by eexists. inv H3. + } + inv H3. inv H1. + pose proof (proj1 (semantic_iff_termination _ _ _) + (ex_intro _ res (conj Hres H4))) as TERM. + apply term_eval_empty in TERM as [resa [ka [Hresa [D Hlt3]]]]. + eapply frame_indep_core in D as D'. + pose proof (transitive_eval_rev_lt H4 Hlt3 D'). simpl in H1, D'. + clear D'. + eapply conj, ex_intro with (x := ka), IH in D as [va EQ]. + 5: assumption. + 3: reflexivity. + 2: { simpl in H. lia. } + 2: { simpl in H2. by apply andb_true_iff in H2 as []. } + subst. inv H1. inv H5. + + (* params remain *) + eapply IHl. + { simpl in *. lia. } + { simpl in *. by apply andb_true_iff in H2 as []. } + { econstructor. constructor. congruence. exact H8. } + { assumption. } + { clear-H0. simpl in *. rewrite length_app. simpl. + by replace (S (length el + (length vals + 1))) with + (S (S (length el + length vals))) by lia. } + + (* final step *) + cbn in H14. + pose proof is_safe_eval _ _ _ H0 (vals ++ [va]) ltac:(rewrite length_app; slia) as [v [eff ?]]. + rewrite H1 in H14. inv H14. + inv H8. by eexists. inv H5. +Qed. (* Lemma eval_seq_optim_1 : forall e1 e2 res, @@ -504,8 +694,6 @@ Proof. 2: case_match. { eapply will_fail_subst in H4 as H4'. - pose proof will_fail_exception (seq_elim e1).[ξ] H4' as [exc D1]. - destruct D1 as [n1 [Hres1 D1]]. pose proof (H (size_exp e1) ltac:(lia) e1 ltac:(lia) Γ ltac:(by destruct_scopes)) as [CIUe1_1 CIUe1_2]. specialize (CIUe1_1 _ H2) as [_ [_ D3]]. @@ -519,26 +707,49 @@ Proof. * constructor. constructor. assumption. } { eexists. exact H9. } destruct D3. - eapply frame_indep_nil in D1 as D1'. - eapply term_step_term in H6. 2: exact D1'. - inv H6. + + apply term_eval_empty in H3 as HELPER. + destruct HELPER as [? [x0 [Helpres [HELPER _]]]]. + pose proof HELPER as EVAL. + apply (conj Helpres), ex_intro with (x := x0) in HELPER. + epose proof will_fail_exception (seq_elim e1).[ξ] _ H4' HELPER as [exc EQ]. + subst. clear HELPER. (* now we can use EVAL for showing the exception *) + + eapply frame_indep_nil in EVAL as D1'. + eapply term_step_term in H3. 2: exact D1'. + inv H3. eexists. eapply step_term_term_plus. - eapply frame_indep_nil in D1. exact D1. - exact H13. + eapply frame_indep_nil in EVAL. exact EVAL. + exact H11. } { - eapply is_safe_simple_subst with (ξ := ξ) in H5. - apply is_safe_simple_no_effects in H5 as D. - destruct D as [vs [k1 D]]. - apply step_rt_labeled_to_unlabeled in D. + eapply is_safe_simple_subst with (ξ := ξ) in H5. 2: eassumption. + 2: apply closed_seq_elim; by destruct_scopes. pose proof (H (size_exp e1) ltac:(lia) e1 ltac:(lia) Γ ltac:(by destruct_scopes)) as [CIUe1_1 CIUe1_2]. eapply term_eval_empty in H9 as D'. destruct D' as [res [k1' [Hres [D' Hlt]]]]. pose proof (CIUe1_1 _ H2). pose proof (CIUe1_2 _ H2). - assert (CIU res vs /\ CIU vs res). { + + (* modifications to use is_safe_simple_no_effects *) + pose proof (ex_intro _ k H9) as HELPER. + unshelve (epose proof (proj2 (proj2 H6) _ _ HELPER) as [? HELPER2]). + { split. + * econstructor. 2: apply H3. + constructor. apply -> subst_preserves_scope_exp. + destruct_scopes. eassumption. assumption. + * constructor; try apply H3. by simpl. + } + apply term_eval_empty in HELPER2 as [? [x1 [Helpres [HELPER2 _]]]]. + pose proof HELPER2 as D. + apply (conj Helpres), ex_intro with (x := x1) in HELPER2. + eapply is_safe_simple_no_effects in HELPER2 as [v EQ]. + subst. clear HELPER. + (***) + + assert (CIU res (RValSeq [v]) /\ CIU (RValSeq [v]) res). { clear -D D' H6 H7 H1 H2. apply CIU_eval_base in D' as []. 2: { destruct_scopes. constructor. @@ -560,7 +771,6 @@ Proof. eapply frame_indep_core in D'. epose proof term_step_term _ _ _ _ H9 _ _ D'. 2: eassumption. - 2: apply closed_seq_elim; by destruct_scopes. simpl in *. destruct res; try by inv_result. 2: { From c0e826ded883db631087b354dfec21d6232e7f76 Mon Sep 17 00:00:00 2001 From: berpeti Date: Wed, 15 Oct 2025 18:19:51 +0200 Subject: [PATCH 4/7] All supporting lemmas proved --- src/FrameStack/Optimisations/SeqDeadCode.v | 213 ++++++++++++++++++++- 1 file changed, 203 insertions(+), 10 deletions(-) diff --git a/src/FrameStack/Optimisations/SeqDeadCode.v b/src/FrameStack/Optimisations/SeqDeadCode.v index 922c224..ebde7f0 100644 --- a/src/FrameStack/Optimisations/SeqDeadCode.v +++ b/src/FrameStack/Optimisations/SeqDeadCode.v @@ -6,13 +6,13 @@ Require Export Basics. Import ListNotations. -Lemma exp_params_eval (exps : list Exp) vals : +(* Lemma exp_params_eval (exps : list Exp) vals : list_biforall (fun exp val => ⟨[], RExp exp⟩ -->* RValSeq [val]) exps vals -> forall vals0 v Fs id, exists k, ⟨FParams id vals0 exps :: Fs, RValSeq [v]⟩ -[k]-> ⟨FParams id (vals0 ++ removelast (v::vals)) [] :: Fs, RValSeq [last vals v]⟩. Proof. -Admitted. +Admitted. *) Definition is_exit_bif (modu func : string) (n : nat) : bool := match convert_string_to_code (modu, func) with @@ -109,7 +109,7 @@ Fixpoint seq_elim (e : Exp) : Exp := end (* end *). -Fixpoint size_val (v : Val) : nat := +Fixpoint (* size_val (v : Val) : nat := 1 (* match v with | VNil => 1 | VLit _ => 1 @@ -121,9 +121,9 @@ Fixpoint size_val (v : Val) : nat := | VFunId _ => 1 | VClos ext _ _ e => 1 + fold_left (fun acc '(_,_,e0) => acc + size_exp e0) ext 0 + size_exp e end *) -with size_exp (e : Exp) : nat := +with *) size_exp (e : Exp) : nat := match e with - | VVal v => 1 + size_val v + | VVal v => 1 | EExp nv => 1 + size_nonval nv end with size_nonval (nv : NonVal) : nat := @@ -231,13 +231,201 @@ Qed. Lemma closed_seq_elim Γ e : EXP Γ ⊢ e -> EXP Γ ⊢ (seq_elim e). Proof. -Admitted. + intro. remember (size_exp e) as n. + assert (size_exp e <= n) by lia. clear Heqn. + revert Γ e H0 H. + induction n using lt_wf_ind. rename H into IH. intros. + destruct e; simpl; try congruence. + destruct e; simpl; try congruence. + all: destruct_scopes; simpl in H0. + * do 2 constructor. eapply IH. 2: reflexivity. 2: assumption. lia. + * (* same for tuples, primops, similar to maps, case, app *) + do 2 constructor. intros. + rewrite length_map in H. apply H2 in H as H'. + rewrite map_nth with (d := seq_elim (˝VNil)). simpl. + eapply IH. 3: exact H'. + 2: reflexivity. + apply nth_In with (d := ˝VNil) in H. + apply In_split in H as [? [? H]]. rewrite H in H0. + rewrite map_app, list_sum_app in H0. simpl in H0. lia. + * do 2 constructor; eapply IH; try eassumption. + all: lia. + * do 2 constructor. intros. + rewrite length_map in H. apply H2 in H as H'. + rewrite map_nth with (d := seq_elim (˝VNil)). simpl. + eapply IH. 3: exact H'. + 2: reflexivity. + apply nth_In with (d := ˝VNil) in H. + apply In_split in H as [? [? H]]. rewrite H in H0. + rewrite map_app, list_sum_app in H0. simpl in H0. lia. + * do 2 constructor; intros; + rewrite length_map in H; apply H1 in H as H'1; apply H4 in H as H'2. + all: rewrite map_map. + (* only H'1 and H'2 are different in the following 2 subgoals *) + - rewrite map_nth with (d := prod_map seq_elim seq_elim (˝VNil,˝VNil)). cbn. + rewrite map_nth with (d := (˝VNil,˝VNil)) in H'1. + apply nth_In with (d := (˝VNil, ˝VNil)) in H. + apply In_split in H as [? [? H]]. rewrite H in H0. + rewrite map_app, list_sum_app in H0. simpl in H0. + destruct (nth i l); simpl in *. + eapply IH. 3: exact H'1. + 2: reflexivity. lia. + - rewrite map_nth with (d := prod_map seq_elim seq_elim (˝VNil,˝VNil)). cbn. + rewrite map_nth with (d := (˝VNil,˝VNil)) in H'2. + apply nth_In with (d := (˝VNil, ˝VNil)) in H. + apply In_split in H as [? [? H]]. rewrite H in H0. + rewrite map_app, list_sum_app in H0. simpl in H0. + destruct (nth i l); simpl in *. + eapply IH. 3: exact H'2. + 2: reflexivity. lia. + * do 2 constructor. + 2-3: eapply IH; try eassumption; lia. + intros. + rewrite length_map in H. apply H5 in H as H'. + rewrite map_nth with (d := seq_elim (˝VNil)). simpl. + eapply IH. 3: exact H'. + 2: reflexivity. + apply nth_In with (d := ˝VNil) in H. + apply In_split in H as [? [? H]]. rewrite H in H0. + rewrite map_app, list_sum_app in H0. simpl in H0. lia. + * do 2 constructor. intros. + rewrite length_map in H. apply H2 in H as H'. + rewrite map_nth with (d := seq_elim (˝VNil)). simpl. + eapply IH. 3: exact H'. + 2: reflexivity. + apply nth_In with (d := ˝VNil) in H. + apply In_split in H as [? [? H]]. rewrite H in H0. + rewrite map_app, list_sum_app in H0. simpl in H0. lia. + * do 2 constructor. + 1: eapply IH; try eassumption; lia. + intros. + rewrite length_map in H. apply H5 in H as H'. + rewrite map_nth with (d := seq_elim (˝VNil)). simpl. + eapply IH. 3: exact H'. + 2: reflexivity. + apply nth_In with (d := ˝VNil) in H. + apply In_split in H as [? [? H]]. rewrite H in H0. + rewrite map_app, list_sum_app in H0. simpl in H0. lia. + * do 2 constructor; intros. + 1: eapply IH; try eassumption; lia. + all: rewrite length_map in H; apply H5 in H as H'1; apply H6 in H as H'2. + all: repeat rewrite map_map. + (* only H'1 and H'2 are different in the following 2 subgoals *) + - rewrite map_nth with (d := prod_map (prod_map id seq_elim) seq_elim ([],˝VNil,˝VNil)). + setoid_rewrite map_nth with (d := prod_map (prod_map id seq_elim) seq_elim ([],˝VNil,˝VNil)). + setoid_rewrite map_nth with (d := prod_map (prod_map id seq_elim) seq_elim ([],˝VNil,˝VNil)) in H'1. cbn. + apply nth_In with (d := ([],˝VNil, ˝VNil)) in H. + apply In_split in H as [? [? H]]. rewrite H in H0. + rewrite map_app, list_sum_app in H0. simpl in H0. + destruct (nth i l), p; simpl in *. + eapply IH. 3: exact H'1. + 2: reflexivity. lia. + - rewrite map_nth with (d := prod_map (prod_map id seq_elim) seq_elim ([],˝VNil,˝VNil)). + setoid_rewrite map_nth with (d := prod_map (prod_map id seq_elim) seq_elim ([],˝VNil,˝VNil)). + setoid_rewrite map_nth with (d := prod_map (prod_map id seq_elim) seq_elim ([],˝VNil,˝VNil)) in H'2. cbn. + apply nth_In with (d := ([],˝VNil, ˝VNil)) in H. + apply In_split in H as [? [? H]]. rewrite H in H0. + rewrite map_app, list_sum_app in H0. simpl in H0. + destruct (nth i l), p; simpl in *. + eapply IH. 3: exact H'2. + 2: reflexivity. lia. + * do 2 constructor; eapply IH; try eassumption. + all: lia. + * (* Sequences: the only tricky case *) + case_match. + - eapply IH; try eassumption; lia. + - case_match. + + eapply IH; try eassumption; lia. + + do 2 constructor. + all: eapply IH; try eassumption; lia. + * do 2 constructor. + 2: rewrite length_map; eapply IH; try eassumption; lia. + intros. + repeat rewrite map_map. + rewrite length_map in H. apply H4 in H as H'. + setoid_rewrite map_nth with (d := prod_map id seq_elim (0,˝VNil)). simpl. + setoid_rewrite map_nth with (d := prod_map id seq_elim (0,˝VNil)) in H'. simpl in H'. + apply nth_In with (d := (0, ˝VNil)) in H. + apply In_split in H as [? [? H]]. rewrite H in H0. + rewrite map_app, list_sum_app in H0. simpl in H0. + destruct (nth i l). + rewrite length_map. + eapply IH. 3: exact H'. + 2: reflexivity. + lia. + * do 2 constructor; eapply IH; try eassumption. + all: lia. +Qed. Lemma subst_preserves_size : forall e ξ, size_exp (e.[ξ]) = size_exp e. Proof. -Admitted. + intro. remember (size_exp e) as n. rewrite Heqn. + assert (size_exp e <= n) by lia. clear Heqn. + revert e H. + induction n using lt_wf_ind. rename H into IH. intros. + destruct e; simpl in *; try congruence; + destruct e; simpl in *; try congruence. + * erewrite IH; try reflexivity. lia. + * rewrite map_map. + f_equal. f_equal. + apply map_ext_in. intros. + eapply IH; try reflexivity. + apply in_split in H0 as [? [? ?]]. subst. + rewrite map_app, list_sum_app in H. simpl in H. lia. + * erewrite IH, IH; try reflexivity; lia. + * rewrite map_map. + f_equal. f_equal. + apply map_ext_in. intros. + eapply IH; try reflexivity. + apply in_split in H0 as [? [? ?]]. subst. + rewrite map_app, list_sum_app in H. simpl in H. lia. + * rewrite map_map. + f_equal. f_equal. + apply map_ext_in. intros. destruct a. + erewrite IH, IH; try reflexivity. + all: apply in_split in H0 as [? [? ?]]; subst; + rewrite map_app, list_sum_app in H; simpl in H; lia. + * erewrite IH; try reflexivity. 2: lia. + erewrite IH; try reflexivity. 2: lia. + rewrite map_map. + f_equal. f_equal. f_equal. + apply map_ext_in. intros. + eapply IH; try reflexivity. + apply in_split in H0 as [? [? ?]]. subst. + rewrite map_app, list_sum_app in H. simpl in H. lia. + * rewrite map_map. + f_equal. f_equal. + apply map_ext_in. intros. + eapply IH; try reflexivity. + apply in_split in H0 as [? [? ?]]. subst. + rewrite map_app, list_sum_app in H. simpl in H. lia. + * erewrite IH; try reflexivity. 2: lia. + rewrite map_map. + f_equal. f_equal. f_equal. + apply map_ext_in. intros. + eapply IH; try reflexivity. + apply in_split in H0 as [? [? ?]]. subst. + rewrite map_app, list_sum_app in H. simpl in H. lia. + * erewrite IH; try reflexivity. 2: lia. + rewrite map_map. + f_equal. f_equal. f_equal. + apply map_ext_in. intros. destruct a, p. + erewrite IH, IH; try reflexivity. + all: apply in_split in H0 as [? [? ?]]; subst; + rewrite map_app, list_sum_app in H; simpl in H; lia. + * erewrite IH, IH; try reflexivity; lia. + * erewrite IH, IH; try reflexivity; lia. + * erewrite IH; try reflexivity. 2: lia. + rewrite map_map. + f_equal. f_equal. f_equal. + apply map_ext_in. intros. destruct a. + erewrite IH; try reflexivity. + all: apply in_split in H0 as [? [? ?]]; subst; + rewrite map_app, list_sum_app in H; simpl in H; lia. + * erewrite IH, IH, IH; try reflexivity; lia. +Qed. Lemma will_fail_exception : forall e res, will_fail e = true -> @@ -668,7 +856,7 @@ Proof. - eapply H. 2: reflexivity. 2: by destruct_scopes. simpl in H0. lia. } - * admit. + * * admit. * admit. * admit. @@ -785,10 +973,15 @@ Proof. eapply CIUe2_1; eassumption. } { - + (* Here, we use congruence - reshape the goal for it *) + enough (CIU_open Γ (° ESeq e1 e2) (° ESeq (seq_elim e1) (seq_elim e2))). + apply H6; try eassumption. + eexists. simpl. econstructor. eassumption. + apply CONG. 1-4: try apply closed_seq_elim; by destruct_scopes. + all: eapply H; [ | reflexivity | by destruct_scopes]; simpl in H0; lia. } } - { + { (* reverse direction *) admit. } * admit. From 77ef87ec7615a8f74d0b371238c4b18b17401470 Mon Sep 17 00:00:00 2001 From: berpeti Date: Wed, 15 Oct 2025 18:56:43 +0200 Subject: [PATCH 5/7] 1 goal missing from optim correct --- src/FrameStack/Optimisations/SeqDeadCode.v | 326 ++++++++++++++++++++- 1 file changed, 314 insertions(+), 12 deletions(-) diff --git a/src/FrameStack/Optimisations/SeqDeadCode.v b/src/FrameStack/Optimisations/SeqDeadCode.v index ebde7f0..1856675 100644 --- a/src/FrameStack/Optimisations/SeqDeadCode.v +++ b/src/FrameStack/Optimisations/SeqDeadCode.v @@ -843,7 +843,9 @@ Proof. pose proof CIU_IsPreCtxRel as CONG. destruct e; simpl. * split. - { apply CONG; auto. + { (* The bracketed subgoals in the following proofs are completely symmetric + They are proved almost always the same way, with the same script. *) + apply CONG; auto. - by destruct_scopes. - apply closed_seq_elim. by destruct_scopes. - eapply H. 2: reflexivity. 2: by destruct_scopes. @@ -856,15 +858,253 @@ Proof. - eapply H. 2: reflexivity. 2: by destruct_scopes. simpl in H0. lia. } - * - * admit. - * admit. - * admit. - * admit. - * admit. - * admit. - * admit. - * admit. + * destruct_scopes. simpl in H0. split. + { + apply CONG; auto. + - by apply indexed_to_forall in H3. + - apply indexed_to_forall in H3. + induction H3; constructor. + 2: apply IHForall. 2: by simpl in H0; lia. + by apply closed_seq_elim. + - clear - H0 H H3. induction el; constructor. + 2: apply IHel. 2: by simpl in H0; lia. + 2: intros; apply (H3 (S i)); slia. + eapply H. 2: reflexivity. 1: { simpl in H0. lia. } + apply (H3 0). slia. + } + { + apply CONG; auto. + - apply indexed_to_forall in H3. + induction H3; constructor. + 2: apply IHForall. 2: by simpl in H0; lia. + by apply closed_seq_elim. + - by apply indexed_to_forall in H3. + - clear - H0 H H3. induction el; constructor. + 2: apply IHel. 2: by simpl in H0; lia. + 2: intros; apply (H3 (S i)); slia. + eapply H. 2: reflexivity. 1: { simpl in H0. lia. } + apply (H3 0). slia. + } + * destruct_scopes. simpl in H0. split. + { + apply CONG; auto. + 1-2: by apply closed_seq_elim. + 1-2: eapply H; try reflexivity; try lia; assumption. + } + { + apply CONG; auto. + 1-2: by apply closed_seq_elim. + 1-2: eapply H; try reflexivity; try lia; assumption. + } + * destruct_scopes. simpl in H0. split. + { + apply CONG; auto. + - by apply indexed_to_forall in H3. + - apply indexed_to_forall in H3. + induction H3; constructor. + 2: apply IHForall. 2: by simpl in H0; lia. + by apply closed_seq_elim. + - clear - H0 H H3. induction l; constructor. + 2: apply IHl. 2: by simpl in H0; lia. + 2: intros; apply (H3 (S i)); slia. + eapply H. 2: reflexivity. 1: { simpl in H0. lia. } + apply (H3 0). slia. + } + { + apply CONG; auto. + - apply indexed_to_forall in H3. + induction H3; constructor. + 2: apply IHForall. 2: by simpl in H0; lia. + by apply closed_seq_elim. + - by apply indexed_to_forall in H3. + - clear - H0 H H3. induction l; constructor. + 2: apply IHl. 2: by simpl in H0; lia. + 2: intros; apply (H3 (S i)); slia. + eapply H. 2: reflexivity. 1: { simpl in H0. lia. } + apply (H3 0). slia. + } + * destruct_scopes. simpl in H0. split. + { + pose proof (Forall_pair _ _ _ _ _ H2 H5). clear H2 H5. + apply CONG; auto. + - eapply Forall_impl. 2: exact H1. intros. by destruct a. + - induction H1; constructor. 2: apply IHForall. 2: by simpl in H0; lia. + destruct x; unfold PBoth; destruct_and?; split; by apply closed_seq_elim. + - clear - H1 H H0. induction H1; constructor. + 2: apply IHForall. 2: by simpl in H0; lia. + destruct x. split; + eapply H; try reflexivity; try (simpl in H0; lia). + all: apply H1. + } + { + pose proof (Forall_pair _ _ _ _ _ H2 H5). clear H2 H5. + apply CONG; auto. + - induction H1; constructor. 2: apply IHForall. 2: by simpl in H0; lia. + destruct x; unfold PBoth; destruct_and?; split; by apply closed_seq_elim. + - eapply Forall_impl. 2: exact H1. intros. by destruct a. + - clear - H1 H H0. induction H1; constructor. + 2: apply IHForall. 2: by simpl in H0; lia. + destruct x. split; + eapply H; try reflexivity; try (simpl in H0; lia). + all: apply H1. + } + * destruct_scopes. simpl in H0. split. + { + apply CONG; auto. + 1-2: by apply closed_seq_elim. + 1-2: eapply H; try reflexivity; try assumption; lia. + - by apply indexed_to_forall in H6. + - apply indexed_to_forall in H6. + induction H6; constructor. + 2: apply IHForall. 2: by simpl in H0; lia. + by apply closed_seq_elim. + - clear - H0 H H6. induction l; constructor. + 2: apply IHl. 2: by simpl in H0; lia. + 2: intros; apply (H6 (S i)); slia. + eapply H. 2: reflexivity. 1: { simpl in H0. lia. } + apply (H6 0). slia. + } + { + apply CONG; auto. + 1-2: by apply closed_seq_elim. + 1-2: eapply H; try reflexivity; try assumption; lia. + - apply indexed_to_forall in H6. + induction H6; constructor. + 2: apply IHForall. 2: by simpl in H0; lia. + by apply closed_seq_elim. + - by apply indexed_to_forall in H6. + - clear - H0 H H6. induction l; constructor. + 2: apply IHl. 2: by simpl in H0; lia. + 2: intros; apply (H6 (S i)); slia. + eapply H. 2: reflexivity. 1: { simpl in H0. lia. } + apply (H6 0). slia. + } + * destruct_scopes. simpl in H0. split. + { + apply CONG; auto. + - by apply indexed_to_forall in H3. + - apply indexed_to_forall in H3. + induction H3; constructor. + 2: apply IHForall. 2: by simpl in H0; lia. + by apply closed_seq_elim. + - clear - H0 H H3. induction l; constructor. + 2: apply IHl. 2: by simpl in H0; lia. + 2: intros; apply (H3 (S i)); slia. + eapply H. 2: reflexivity. 1: { simpl in H0. lia. } + apply (H3 0). slia. + } + { + apply CONG; auto. + - apply indexed_to_forall in H3. + induction H3; constructor. + 2: apply IHForall. 2: by simpl in H0; lia. + by apply closed_seq_elim. + - by apply indexed_to_forall in H3. + - clear - H0 H H3. induction l; constructor. + 2: apply IHl. 2: by simpl in H0; lia. + 2: intros; apply (H3 (S i)); slia. + eapply H. 2: reflexivity. 1: { simpl in H0. lia. } + apply (H3 0). slia. + } + * destruct_scopes. simpl in H0. split. + { + apply CONG; auto. + 1: by apply closed_seq_elim. + 3: eapply H; try reflexivity; try assumption; lia. + - by apply indexed_to_forall in H6. + - apply indexed_to_forall in H6. + induction H6; constructor. + 2: apply IHForall. 2: by simpl in H0; lia. + by apply closed_seq_elim. + - clear - H0 H H6. induction l; constructor. + 2: apply IHl. 2: by simpl in H0; lia. + 2: intros; apply (H6 (S i)); slia. + eapply H. 2: reflexivity. 1: { simpl in H0. lia. } + apply (H6 0). slia. + } + { + apply CONG; auto. + 1: by apply closed_seq_elim. + 3: eapply H; try reflexivity; try assumption; lia. + - apply indexed_to_forall in H6. + induction H6; constructor. + 2: apply IHForall. 2: by simpl in H0; lia. + by apply closed_seq_elim. + - by apply indexed_to_forall in H6. + - clear - H0 H H6. induction l; constructor. + 2: apply IHl. 2: by simpl in H0; lia. + 2: intros; apply (H6 (S i)); slia. + eapply H. 2: reflexivity. 1: { simpl in H0. lia. } + apply (H6 0). slia. + } + * destruct_scopes. simpl in H0. split. + { + apply CONG; auto. + 1: by apply closed_seq_elim. + 3: eapply H; try reflexivity; try assumption; lia. + - eapply indexed_to_forall with (def := ([], ˝VNil, ˝VNil)). intros. + apply H6 in H1 as H'1. + apply H7 in H1 as H'2. + setoid_rewrite map_nth with (d := ([], ˝VNil, ˝VNil)) in H'1. + setoid_rewrite map_nth with (d := ([], ˝VNil, ˝VNil)) in H'2. + destruct nth, p. by auto. + - induction l; constructor. 2: apply IHl. 2: by simpl in H0; lia. + 2: intros; apply (H6 (S i)); slia. + 2: intros; apply (H7 (S i)); slia. + clear IHl. + destruct a, p; simpl in *. + split; apply closed_seq_elim. + 1: apply (H6 0); slia. + 1: apply (H7 0); slia. + - clear - H6 H7 H H0. induction l; constructor. + 2: apply IHl. 2: by simpl in H0; lia. + 2: intros; apply (H6 (S i)); slia. + 2: intros; apply (H7 (S i)); slia. + clear IHl. + destruct a, p. split; auto. split; + eapply H; try reflexivity; try (simpl in H0; lia). + 1: apply (H6 0); slia. + 1: apply (H7 0); slia. + } + { + apply CONG; auto. + 1: by apply closed_seq_elim. + 3: eapply H; try reflexivity; try assumption; lia. + - induction l; constructor. 2: apply IHl. 2: by simpl in H0; lia. + 2: intros; apply (H6 (S i)); slia. + 2: intros; apply (H7 (S i)); slia. + clear IHl. + destruct a, p; simpl in *. + split; apply closed_seq_elim. + 1: apply (H6 0); slia. + 1: apply (H7 0); slia. + - eapply indexed_to_forall with (def := ([], ˝VNil, ˝VNil)). intros. + apply H6 in H1 as H'1. + apply H7 in H1 as H'2. + setoid_rewrite map_nth with (d := ([], ˝VNil, ˝VNil)) in H'1. + setoid_rewrite map_nth with (d := ([], ˝VNil, ˝VNil)) in H'2. + destruct nth, p. by auto. + - clear - H6 H7 H H0. induction l; constructor. + 2: apply IHl. 2: by simpl in H0; lia. + 2: intros; apply (H6 (S i)); slia. + 2: intros; apply (H7 (S i)); slia. + clear IHl. + destruct a, p. split; auto. split; + eapply H; try reflexivity; try (simpl in H0; lia). + 1: apply (H6 0); slia. + 1: apply (H7 0); slia. + } + * destruct_scopes. simpl in H0. split. + { + apply CONG; auto. + 1-2: by apply closed_seq_elim. + 1-2: eapply H; try reflexivity; try lia; assumption. + } + { + apply CONG; auto. + 1-2: by apply closed_seq_elim. + 1-2: eapply H; try reflexivity; try lia; assumption. + } * split. { split. 2: split. @@ -984,8 +1224,70 @@ Proof. { (* reverse direction *) admit. } - * admit. - * admit. + * destruct_scopes. simpl in H0. split. + { + apply CONG; auto. + 1: rewrite length_map; by apply closed_seq_elim. + 4: eapply H; try reflexivity; try assumption; lia. + - eapply indexed_to_forall with (def := (0, ˝VNil)). intros. + apply H5 in H1 as H'1. + setoid_rewrite map_nth with (d := (0, ˝VNil)) in H'1. + destruct nth. by auto. + - eapply indexed_to_forall with (def := (0, ˝VNil)). intros. + rewrite length_map in H1. rewrite length_map. apply H5 in H1. + rewrite map_nth with (d := (0, ˝VNil)). + setoid_rewrite map_nth with (d := (0, ˝VNil)) in H1. + destruct nth. + by apply closed_seq_elim. + - clear - H5 H H0. + eapply indexed_to_biforall with (d1 := (0, ˝VNil)) (d2 := (0, ˝VNil)). + intros. rewrite length_map. split. 2: reflexivity. + intros. apply H5 in H1 as H5'. + rewrite map_nth with (d := (0, ˝VNil)). + setoid_rewrite map_nth with (d := (0, ˝VNil)) in H5'. + apply nth_In with (d := (0, ˝VNil)) in H1. + destruct nth. split. reflexivity. + eapply H; try reflexivity. 2: assumption. + apply in_split in H1 as [? [? ?]]. subst. + rewrite map_app, list_sum_app in H0. simpl in H0. lia. + } + { + apply CONG; auto. + 1: rewrite length_map; by apply closed_seq_elim. + 4: rewrite length_map; eapply H; try reflexivity; try assumption; lia. + - eapply indexed_to_forall with (def := (0, ˝VNil)). intros. + rewrite length_map in H1. rewrite length_map. apply H5 in H1. + rewrite map_nth with (d := (0, ˝VNil)). + setoid_rewrite map_nth with (d := (0, ˝VNil)) in H1. + destruct nth. + by apply closed_seq_elim. + - eapply indexed_to_forall with (def := (0, ˝VNil)). intros. + apply H5 in H1 as H'1. + setoid_rewrite map_nth with (d := (0, ˝VNil)) in H'1. + destruct nth. by auto. + - clear - H5 H H0. + eapply indexed_to_biforall with (d1 := (0, ˝VNil)) (d2 := (0, ˝VNil)). + intros. rewrite length_map. split. 2: reflexivity. + intros. apply H5 in H1 as H5'. + rewrite map_nth with (d := (0, ˝VNil)). + setoid_rewrite map_nth with (d := (0, ˝VNil)) in H5'. + apply nth_In with (d := (0, ˝VNil)) in H1. + destruct nth. split. reflexivity. + eapply H; try reflexivity. 2: assumption. + apply in_split in H1 as [? [? ?]]. subst. + rewrite map_app, list_sum_app in H0. simpl in H0. lia. + } + * destruct_scopes. simpl in H0. split. + { + apply CONG; auto. + 1-3: by apply closed_seq_elim. + 1-3: eapply H; try reflexivity; try lia; assumption. + } + { + apply CONG; auto. + 1-3: by apply closed_seq_elim. + 1-3: eapply H; try reflexivity; try lia; assumption. + } Admitted. Theorem seq_optim (e : Exp) : From 904562d8885c3d27223b83889757d7a45db63ed0 Mon Sep 17 00:00:00 2001 From: berpeti Date: Wed, 15 Oct 2025 20:48:38 +0200 Subject: [PATCH 6/7] Optimisation proved completely - refactoring is needed on the proof --- src/FrameStack/Optimisations/SeqDeadCode.v | 249 ++++++++++++++++++++- 1 file changed, 241 insertions(+), 8 deletions(-) diff --git a/src/FrameStack/Optimisations/SeqDeadCode.v b/src/FrameStack/Optimisations/SeqDeadCode.v index 1856675..6d5fb31 100644 --- a/src/FrameStack/Optimisations/SeqDeadCode.v +++ b/src/FrameStack/Optimisations/SeqDeadCode.v @@ -600,6 +600,139 @@ Proof. all: case_match; try by do 2 eexists. Qed. +(* TODO: refactor *) +Lemma is_safe_simple_no_effects_core: + forall e, is_safe_simple e = true -> + (* is_result res -> *) + exists v, ⟨[], e⟩ -->* RValSeq [v]. (* TODO: no side effects - labeled termination needed *) +Proof. + intro. remember (size_exp e) as n. + assert (size_exp e <= n) by lia. clear Heqn. + revert e H. + induction n using lt_wf_ind. rename H into IH. + destruct e; simpl; try congruence. + * intros. destruct e; try congruence; eexists; econstructor; split. + all: try do_step; try constructor. + * destruct e; simpl; try congruence. + - intros Hlt Hsafe. + apply andb_true_iff in Hsafe as [Hsafe1 Hsafe2]. + eapply IH in Hsafe1 as [? [? [? ?]]]. 3: reflexivity. 2: lia. + eapply IH in Hsafe2 as [? [? [? ?]]]. 3: reflexivity. 2: lia. + do 2 eexists. split. + 2: { + do_step. eapply transitive_eval. eapply frame_indep_nil in H2. exact H2. + do_step. eapply transitive_eval. eapply frame_indep_nil in H0. exact H0. + do_step. + constructor. + } + constructor. + - intros. + assert (X : forall vals, + exists v, ⟨[FParams ITuple vals l], RBox⟩ -->* RValSeq [v]). { + induction l; intros. + { (* final step *) + do 2 eexists. split. constructor. + econstructor. econstructor. congruence. reflexivity. constructor. + } + { (* inductive case *) + destruct l. + (* singleton l *) + * simpl in H0. rewrite andb_true_r in H0. + ospecialize* (IH). 3: exact H0. 2: reflexivity. simpl in H; lia. + destruct IH as [? [? [? ?]]]. + do 2 eexists. split. constructor. + econstructor. econstructor. congruence. + eapply frame_indep_nil in H2. eapply transitive_eval. exact H2. + econstructor. econstructor. reflexivity. constructor. + * (* non-singleton l *) + simpl in H0. apply andb_true_iff in H0 as []. + ospecialize* (IH). 3: exact H0. 2: reflexivity. simpl in H; lia. + destruct IH as [? [? [? ?]]]. + ospecialize* IHl. 1: { simpl. simpl in H. lia. } + 1: by simpl. + { + destruct IHl as [? [? [? ?]]]. inv H5. inv H6. + do 2 eexists. split. constructor. + do_step. eapply transitive_eval. eapply frame_indep_nil in H3. exact H3. + do_step. exact H7. + } + } + } + specialize (X []) as [v [k [Hv X]]]. + do 2 eexists. split. constructor. + { + do_step. + exact X. + } + - intros. + destruct m; simpl; try congruence. + destruct e; simpl; try congruence. + destruct l0; simpl; try congruence. + destruct f; simpl; try congruence. + destruct e; simpl; try congruence. + destruct l0; simpl; try congruence. + apply andb_true_iff in H0 as []. + assert (X : forall vals, is_safe s s0 (length l + length vals) = true -> + exists v, ⟨[FParams (ICall (VLit s) (VLit s0)) vals l], RBox⟩ -->* RValSeq [v]). { + + assert (forall vals s s0, is_safe s s0 (length vals) = true -> exists a b, Some (RValSeq [a], b) = create_result (ICall (VLit s) (VLit s0)) vals) as IS. { + intros. + unfold is_safe in H2. unfold create_result, eval. + case_match; try congruence. + all: unfold eval_equality, eval_cmp, eval_check; rewrite H3. + all: destruct vals; simpl in H0; try congruence. + all: try destruct vals; simpl in H0; try congruence. + all: try destruct vals; simpl in H0; try congruence. + all: repeat case_match. + all: by do 2 eexists. + } + + clear H0. induction l; intros. + { (* final step *) + specialize (IS vals s s0 H0) as [? [? ?]]. + do 2 eexists. split. constructor. + econstructor. econstructor. congruence. eassumption. constructor. + } + { (* inductive case *) + destruct l. + (* singleton l *) + * simpl in H1. rewrite andb_true_r in H1. + ospecialize* (IH). 3: exact H1. 2: reflexivity. simpl in H; lia. + destruct IH as [? [? [? ?]]]. + specialize (IS (vals ++ [x]) s s0) as [? [? ?]]. + { rewrite length_app; simpl in H0. simpl. by rewrite Nat.add_comm. } + do 2 eexists. split. constructor. + econstructor. econstructor. congruence. + eapply frame_indep_nil in H3. eapply transitive_eval. exact H3. + econstructor. econstructor. exact H4. constructor. + * (* non-singleton l *) + simpl in H1. apply andb_true_iff in H1 as []. + ospecialize* (IH). 3: exact H1. 2: reflexivity. simpl in H; lia. + destruct IH as [? [? [? ?]]]. + ospecialize* IHl. 1: { simpl. simpl in H. lia. } + 1: by simpl. + 2: { + destruct IHl as [? [? [? ?]]]. inv H6. inv H7. + do 2 eexists. split. constructor. + do_step. eapply transitive_eval. eapply frame_indep_nil in H4. exact H4. + do_step. exact H8. + } + simpl in *. rewrite length_app. simpl. + by replace (S (length l + (length vals + 1))) with + (S (S (length l + length vals))) by lia. + } + } + specialize (X [] ltac:(simpl; by rewrite Nat.add_0_r)) as [v [k [Hv X]]]. + do 2 eexists. split. constructor. + { + do 5 do_step. + exact X. + } +Unshelve. + all: try apply VNil. + all: try apply None. +Qed. + Require Import SubstSemanticsLabeled. Lemma is_safe_simple_no_effects: forall e res, is_safe_simple e = true -> @@ -1222,7 +1355,113 @@ Proof. } } { (* reverse direction *) - admit. + split. 2: split. + - apply -> subst_preserves_scope_red. 2: exact H2. + repeat case_match. + 1-2: constructor; apply closed_seq_elim; by destruct_scopes. + do 3 constructor; + destruct_scopes; + by apply closed_seq_elim. + - apply -> subst_preserves_scope_red. 2: exact H2. scope_solver. + - intros. destruct H4. + simpl in *. + case_match. + 2: case_match. + { + eapply will_fail_subst in H5 as H4'. + pose proof (H (size_exp e1) ltac:(lia) e1 ltac:(lia) Γ + ltac:(by destruct_scopes)) as [CIUe1_1 CIUe1_2]. + pose proof (CIUe1_2 _ H2) as [_ [_ D3]]. (* The other way around *) + + + pose proof H4 as EE1. + apply term_eval_empty in H4 as [res [k0 [Hres [EE2 Hlt]]]]. + apply (conj Hres), ex_intro with (x := k0) in EE2. + epose proof will_fail_exception (seq_elim e1).[ξ] _ H4' EE2 as [exc ?]. + subst. + + pose proof EE1 as EE1SAVE. + simpl in D3. apply ex_intro with (x := x) in EE1. + apply D3 in EE1. 2: { assumption. } + destruct EE1 as [k EE1]. + apply term_eval_empty in EE1 as [res2 [k1 [Hres2 [EE1 Hlt2]]]]. + unshelve (epose proof (CIU_eval_base _ _ _ _ EE1) as [CIU1 CIU2]). + { constructor. apply -> subst_preserves_scope_exp. by destruct_scopes. + assumption. } + unshelve (epose proof (CIU_eval _ _ _ EE2) as [CIU3 CIU4]). + { constructor. apply -> subst_preserves_scope_exp. + apply closed_seq_elim. by destruct_scopes. assumption. } + specialize (CIUe1_2 ξ H2). + pose proof (CIU_transitive_closed _ _ _ CIUe1_2 CIU1) as CIU5. + pose proof (CIU_transitive_closed _ _ _ CIU4 CIU5). + + destruct EE2 as [? [? EE2]]. + eapply term_step_term in EE1SAVE. 2: { eapply frame_indep_nil in EE2. exact EE2. } + inv Hres2. (* ensure res2 being an exception *) + 2: { + exfalso. destruct H4 as [? [? H4]]. + ospecialize* (H4 [FTry (length vs) (°inf) 3 (˝VNil)]). + split; constructor; simpl; try by constructor. + 1: { constructor. constructor. apply inf_scope. scope_solver. } + { + eexists. destruct exc as [[? ?] ?]. constructor. do 2 constructor. + constructor. + } + inv H4. inv H9. + rewrite eclosed_ignores_sub in H17. 2: constructor; apply inf_scope. + by apply inf_diverges in H17. + } + + apply ex_intro with (x := x - x0) in EE1SAVE. eapply H4 in EE1SAVE as [? EE1SAVE]. + 2: assumption. + eexists. + econstructor. + eapply step_term_term_plus. eapply frame_indep_nil in EE1. exact EE1. + constructor. reflexivity. eassumption. + } + { + eapply is_safe_simple_subst with (ξ := ξ) in H6. 2: eassumption. + 2: apply closed_seq_elim; by destruct_scopes. + + pose proof (H (size_exp e1) ltac:(lia) e1 ltac:(lia) Γ + ltac:(by destruct_scopes)) as [CIUe1_1 CIUe1_2]. + pose proof (CIUe1_1 _ H2). + pose proof (CIUe1_2 _ H2). + pose proof is_safe_simple_no_effects_core _ H6 as [? [? [? ?]]]. + pose proof H10 as EVAL1. + apply CIU_eval_base in H10 as [CIU1 CIU2]. + 2: { constructor. apply -> subst_preserves_scope_exp. apply closed_seq_elim. + by destruct_scopes. assumption. } + pose proof (CIU_transitive_closed _ _ _ CIU2 H8) as CIUFINAL. + assert (| FSeq e2.[ξ] :: F, (seq_elim e1).[ξ] | ↓ ). { + apply ex_intro with (x := x) in H4. + pose proof (H (size_exp e2) ltac:(lia) e2 ltac:(lia) Γ + ltac:(by destruct_scopes)) as [CIUe2_1 CIUe2_2]. + pose proof (CIUe2_1 _ H2). + pose proof (CIUe2_2 _ H2). + eapply H11 in H4 as [? H4]. 2: assumption. + eexists. + eapply step_term_term_plus. eapply frame_indep_nil in EVAL1. exact EVAL1. + constructor. exact H4. + } + apply CIU1 in H10. 2: { split; constructor; try by constructor; simpl. + 2-3: apply H3. + constructor. apply -> subst_preserves_scope_exp. by destruct_scopes. + assumption. } + apply CIUFINAL in H10 as [? ?]. 2: { split; constructor; try by constructor; simpl. + 2-3: apply H3. + constructor. apply -> subst_preserves_scope_exp. by destruct_scopes. + assumption. + } + eexists. constructor. exact H10. + } + { + (* Here, we use congruence - reshape the goal for it *) + enough (CIU_open Γ (° ESeq (seq_elim e1) (seq_elim e2)) (° ESeq e1 e2)). + apply H7; try eassumption. by eexists. + apply CONG. 1-4: try apply closed_seq_elim; by destruct_scopes. + all: eapply H; [ | reflexivity | by destruct_scopes]; simpl in H0; lia. + } } * destruct_scopes. simpl in H0. split. { @@ -1288,12 +1527,6 @@ Proof. 1-3: by apply closed_seq_elim. 1-3: eapply H; try reflexivity; try lia; assumption. } -Admitted. - -Theorem seq_optim (e : Exp) : - EXPCLOSED e -> - CIU (seq_elim e) e. -Proof. - Qed. + From 919ce78b09b5d9ab60ca2482473d36a2f86f4cbd Mon Sep 17 00:00:00 2001 From: berpeti Date: Thu, 13 Nov 2025 08:58:02 +0100 Subject: [PATCH 7/7] Update peculiar Erlang codes --- Erl_codes/b.core | 12 +++- Erl_codes/weird.erl | 142 ++++++++++++++++++++++++++++++++++++++++---- 2 files changed, 142 insertions(+), 12 deletions(-) diff --git a/Erl_codes/b.core b/Erl_codes/b.core index b64502a..dab3afa 100644 --- a/Erl_codes/b.core +++ b/Erl_codes/b.core @@ -20,7 +20,8 @@ module 'b' ['module_info'/0, 'g'/0, 'exp'/0, 'mapex'/0, - 'infex'/0] + 'infex'/0, + 'f'/1] attributes [%% Line 1 'file' = %% Line 1 @@ -34,6 +35,15 @@ module 'b' ['module_info'/0, call 'erlang':'get_module_info' ('b', _0) +'f'/1 = fun(X) -> + do + case X of + when call 'erlang':'<'(X, 0) -> 1 + when 'true' -> 2 + end + Y + + 'mapex'/0 = fun() -> letrec 'map'/2 = fun(F, L) -> diff --git a/Erl_codes/weird.erl b/Erl_codes/weird.erl index d199744..3e4074a 100644 --- a/Erl_codes/weird.erl +++ b/Erl_codes/weird.erl @@ -1,5 +1,6 @@ -module(weird). -compile(export_all). +-include_lib("eqc/include/eqc.hrl"). f() -> self() ! 1, @@ -10,12 +11,9 @@ f() -> after 0 -> [receive X -> X after 0 -> "No more values" end, receive X -> X after 0 -> "No more values" end, receive X -> X after 0 -> "No more values" end] end. -flush() -> - receive - X -> io:format("Process ~p got: ~p~n", [self(), X]), flush() - after - 0 -> ok - end. +% Sometimes this terminates, sometimes it does not +start() -> g(true). + g(X) -> case X of @@ -27,19 +25,141 @@ g(X) -> 2 when false -> ok; 7 -> finished after - 10 -> flush(), g(false) + 0 -> flush(), g(false) end. slave(Pid) -> Pid ! 1, Pid ! 2, - timer:sleep(10), +% timer:sleep(10), Pid ! 3, Pid ! 4, - timer:sleep(10), +% timer:sleep(10), Pid ! 5, Pid ! 6, - timer:sleep(10), - Pid ! 7. +% timer:sleep(10), + Pid ! 7, + timer:sleep(1000), + case is_process_alive(Pid) of + true -> exit(Pid, kill); + _ -> ok + end. + + +start_messaging() -> + Jake = spawn(weird, jake, []), + Susan = spawn(weird, susan, []), + Susan ! Jake, + timer:sleep(6000). + +jake() -> + receive + {Msg, Pid} -> io:format("Jake: Nice, Susan gave me her number: ~p ~p ~n", [Msg, Pid]), + Pid ! "Hi, I'm Jake!" + after + 1000 -> flush(), jake() + end. +susan() -> + Jake = receive X -> X end, + Jake ! "Hi", + timer:sleep(1000), + Jake ! "Heeey", + timer:sleep(1000), + Jake ! "Hellooo?", + timer:sleep(1000), + Jake ! {"Call me please, my number is XXX", self()}, + io:format("Susan: I'm waiting: ~p~n", [self()]), + receive + Msg -> io:format("Susan: I got: ~s ~n", [Msg]) + after + 3000 -> exit(Jake, kill), io:format("Susan: I leave~n") +% 0 -> exit(Jake, kill), io:format("Susan: I leave~n") + end. + +lazy_and(X, Y) -> + if X -> Y; + true -> false + end. + +prop_lazy_and1() -> + ?FORALL(B1, bool(), + ?FORALL(B2, bool(), lazy_and(B1, B2) == (B1 andalso B2))). + +prop_lazy_and2() -> + ?FORALL(B1, int(), + ?FORALL(B2, int(), lazy_and(B1, B2) == (B1 andalso B2))). + + +flush() -> + receive + X -> io:format("Jake ignored: ~p~n", [X]), flush() + after + 0 -> ok + end. + + +test() -> + spawn(fun() -> self() ! "p1" end), + spawn(fun() -> self() ! "p2" end), + receive + X -> io:format("I got: ~p~n", [X]) + end, + timer:sleep(1000), + receive + X -> ok + after + 0 -> ok + end. + +test1() -> + MyPID = self(), + spawn(fun() -> MyPID ! "p1" end), + spawn(fun() -> MyPID ! "p2" end), + receive + X -> io:format("I got: ~p~n", [X]) + end, + timer:sleep(1000), + receive + X -> ok + after + 0 -> ok + end. + +test2() -> + MyPID = self(), + spawn(fun() -> timer:sleep(0), MyPID ! "p1" end), + spawn(fun() -> MyPID ! "p2" end), + receive + X -> io:format("I got: ~p~n", [X]) + end, + timer:sleep(1000), + receive + _ -> ok + after + 0 -> ok + end. + + +start_example() -> + Fpid = spawn(weird, fun1, []), + Gpid = spawn(weird, fun2, []), + Gpid ! Fpid, + timer:sleep(2000). + +fun1() -> + receive + {X, _} -> io:format("Received: ~p~n", [X]) + after 1000 -> flush(), fun1() + end. + +fun2() -> + Fpid = receive X -> X end, + timer:sleep(1000), + Fpid ! "Hello", + timer:sleep(1000), + Fpid ! {"Hello", ok}, + timer:sleep(1000), + exit(Fpid, kill). + recurse() -> recurse().