From 03665a3ebea76410f3120c57c9973d0575499bba Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Wed, 20 Dec 2023 22:06:42 +0100 Subject: [PATCH] :sparkles: Exercises 7 --- .../systemf_mu_state/exercises07.v | 187 +++++++++++++++++- theories/type_systems/systemf_mu_state/lang.v | 2 +- .../type_systems/systemf_mu_state/logrel.v | 78 +++++++- .../type_systems/systemf_mu_state/types.v | 57 ++++-- 4 files changed, 299 insertions(+), 25 deletions(-) diff --git a/theories/type_systems/systemf_mu_state/exercises07.v b/theories/type_systems/systemf_mu_state/exercises07.v index 59c2d19..ba4706c 100644 --- a/theories/type_systems/systemf_mu_state/exercises07.v +++ b/theories/type_systems/systemf_mu_state/exercises07.v @@ -69,19 +69,38 @@ Definition list_t (A : type) : type := Definition mystack : val := (* define your stack implementation, assuming "lc" is a list implementation *) - λ: "lc", #0. (* FIXME *) - + (* + mystack = λ lc, { + new := λ_, new lc.nil, + push := λ stack, λ elem, stack <- lc.cons elem !stack; (), + pop := λ stack, + let res = lc.case !stack (Inj₁ ()) (λ head, λ rest, (Inj₂ head)) in + stack <- lc.case !stack lc.nil (λ head, λ rest, rest); + res + } + *) + λ: "lc", ( + λ: BAnon, new (Fst (Fst "lc")), + λ: "stack" "elem", Snd ("stack" <- (Snd (Fst "lc")) "elem" !"stack", (Lit LitUnit)), + λ: "stack", + let: "res" := (Snd "lc")<> !"stack" (InjL (Lit LitUnit)) (λ: "head" "rest", (InjR "head")) in + Snd ( + "stack" <- (Snd "lc")<> !"stack" (Fst (Fst "lc")) (λ: "head" "rest", "rest"), + "res" + ) + ). + Definition make_mystack : val := Λ, λ: "lc", unpack "lc" as "lc" in - #0. (* FIXME *) + pack (mystack "lc"). Lemma make_mystack_typed Σ n Γ : TY Σ; n; Γ ⊢ make_mystack : (∀: list_t #0 → stack_t #0). Proof. repeat solve_typing_fast. -Admitted. +Qed. (** Exercise 2 (LN Exercise 46): Obfuscated code *) @@ -104,24 +123,172 @@ Proof. + apply IH; done. Qed. +(* Woah great lemma *) +Lemma rtc_contextual_step_fill' K e₁ e₂ e₃ e₄ h h' : + rtc contextual_step (e₂, h) (e₃, h') → + e₁ = fill K e₂ → + e₄ = fill K e₃ → + rtc contextual_step (e₁, h) (e₄, h'). +Proof. + intros H -> ->. + exact (rtc_contextual_step_fill K _ _ _ _ H). +Qed. + (* You may use the [new_fresh] and [init_heap_singleton] lemmas to allocate locations *) +(* +E := let x = new (λx : int. x + x) in + let f = (λg : int -> int. let f = !x in x <- g; f 11) in + f (λx : int. f (λy : int. x)) + f (λx : int. x + 9) + +~> λx: int, x + x ∈ [xl] + let f = (λg : int -> int. let h = !xl in xl <- g; h 11) in + f (λz : int. f (λy : int. z)) + f (λz : int. z + 9) + +~> λx : int, x + x ∈ [xl] + (λg : int -> int. let h = !xl in xl <- g; h 11) + (λz : int. (λg : int -> int. let h = !xl in xl <- g; h 11) (λy : int. z)) + + (λg : int -> int. let h = !xl in xl <- g; h 11) (λz : int. z + 9) + +~>* λx : int, x + x ∈ [xl] + (λg : int -> int. let h = !xl in xl <- g; h 11) + (λz : int. (λg : int -> int. let h = !xl in xl <- g; h 11) (λy : int. z)) + + (xl <- (λz : int. z + 9); (λx, x + x) 11) + +~>* (λz : int. z + 9) ∈ [xl] + (λg : int -> int. let h = !xl in xl <- g; h 11) + (λz : int. (λg : int -> int. let h = !xl in xl <- g; h 11) (λy : int. z)) + + 22 + +~> (λz : int. z + 9) ∈ [xl] + (xl <- (λz : int. (λg : int -> int. let h = !xl in xl <- g; h 11) (λy : int. z)); + (λz : int. z + 9) 11) + + 22 + +~>* (λz : int. (λg : int -> int. let h = !xl in xl <- g; h 11) (λy : int. z)) ∈ [xl] + 20 + 22 + +~> 42 ? +*) + +Ltac beta := ( + eapply rtc_l; first ( + eapply base_contextual_step; + eapply BetaS; [ auto | reflexivity ]; + simpl + ) +). + Lemma obf_expr_eval : - ∃ h', rtc contextual_step (obf_expr, ∅) (of_val #0 (* FIXME: what is the result? *), h'). + ∃ h', rtc contextual_step (obf_expr, ∅) (of_val #42, h'). Proof. eexists. unfold obf_expr. - (* TODO: exercise *) -Admitted. + eapply rtc_l. + eapply (Ectx_step [AppRCtx _]); [reflexivity | reflexivity | ]. + have h₁ : of_val (λ: "x", "x" + "x") = (λ: "x", "x" + "x")%E. reflexivity. + rewrite <-h₁. + apply new_fresh. + simpl. + + beta. + + beta. + + etransitivity. + eapply (rtc_contextual_step_fill' [BinOpRCtx PlusOp _]); [ | simpl; reflexivity | simpl; reflexivity ]. + { + beta. + + eapply rtc_l. + eapply (Ectx_step [AppRCtx _]); [reflexivity | reflexivity | ]. + eapply LoadS. + auto. + beta. + + (* Store *) + eapply rtc_l. + eapply (Ectx_step [AppRCtx _]); [reflexivity | reflexivity | ]. + econstructor; [ eauto | eauto ]. + simpl. + + beta. + + beta. + + eapply rtc_l. + eapply base_contextual_step. + eapply BinOpS; [ auto | auto | auto ]. + simpl. + + have h₂ : (Lit (Z.add 11 11)) = of_val (LitV 22). + reflexivity. + rewrite h₂. + reflexivity. + } + + + etransitivity. + eapply (rtc_contextual_step_fill' [BinOpLCtx PlusOp (LitV 22)]); [ | reflexivity | reflexivity ]. + { + beta. + simpl. + + eapply rtc_l. + eapply (Ectx_step [AppRCtx _]); [reflexivity | reflexivity | ]. + eapply LoadS. + auto. + + beta. + simpl. + + eapply rtc_l. + eapply (Ectx_step [AppRCtx _]); [reflexivity | reflexivity | ]. + eapply StoreS; [ auto | auto ]. + simpl. + + beta. + simpl. + beta. + simpl. + + eapply rtc_l. + eapply base_contextual_step. + eapply BinOpS; [ auto | auto | auto ]. + simpl. + + reflexivity. + } + + eapply rtc_l. + eapply base_contextual_step. + eapply BinOpS; [ auto | auto | auto ]. + simpl. + reflexivity. +Qed. (** Exercise 4 (LN Exercise 48): Fibonacci *) +(* +Idea: use the heap to get recursivity + +fibonacci := λ n, + let rec := new (λ m, 0) in + rec <- λ m, if m <= 1 then m else (!rec (m-1)) + (!rec (m-2)) end; + !rec n +*) + +Definition fibonacci : val := λ: "n", + let: "rec" := new (λ: "m", #0) in + Snd (Pair + ("rec" <- (λ: "m", if: "m" ≤ #1 then "m" else (!"rec" ("m" - #1)) + (!"rec" ("m" - #2)))) + (!"rec" "n") + ) +. -Definition fibonacci : val := #0. (* FIXME *) - Lemma fibonacci_typed Σ n Γ : TY Σ; n; Γ ⊢ fibonacci : (Int → Int). Proof. repeat solve_typing_fast. -Admitted. +Qed. diff --git a/theories/type_systems/systemf_mu_state/lang.v b/theories/type_systems/systemf_mu_state/lang.v index fc0a055..517d95e 100644 --- a/theories/type_systems/systemf_mu_state/lang.v +++ b/theories/type_systems/systemf_mu_state/lang.v @@ -309,7 +309,7 @@ Lemma base_step_to_val e1 e2 e2' σ1 σ2 σ2' : base_step (e1, σ1) (e2', σ2') → is_Some (to_val e2) → is_Some (to_val e2'). Proof. inversion 1; inversion 1; naive_solver. Qed. -Lemma new_fresh v σ : +Lemma new_fresh v (σ : heap) : let l := fresh_locs (dom σ) in base_step (New (of_val v), σ) (Lit $ LitLoc l, init_heap l 1 v σ). Proof. diff --git a/theories/type_systems/systemf_mu_state/logrel.v b/theories/type_systems/systemf_mu_state/logrel.v index 52e0286..82ebce8 100644 --- a/theories/type_systems/systemf_mu_state/logrel.v +++ b/theories/type_systems/systemf_mu_state/logrel.v @@ -1662,9 +1662,81 @@ Lemma compat_store Δ Γ e1 e2 a : TY Δ; Γ ⊨ e2 : a → TY Δ; Γ ⊨ (e1 <- e2) : Unit. Proof. - (* you may find the lemmas [wsat_lookup, wsat_update] above helpful. *) - (* TODO: exercise *) -Admitted. + intros Hsem₁ Hsem₂. + intros θ δ k W Hctx. + + eapply (bind [StoreRCtx (subst_map θ e1)]). + eapply Hsem₂; done. + + intros j v2 W₁ j_le_k W₁_sup_W Hlog_v2. + simpl. + + eapply (bind [StoreLCtx v2]). + eapply Hsem₁. + eapply (sem_context_rel_mono _ _ _ _ _ _ _ j_le_k W₁_sup_W). + done. + + intros i v1 W₂ i_le_j W₂_sup_W₁ Hlog_v1. + + simpl. + simp type_interp. + intros e' h h' W₃ l W₃_sup_W₂ Hwsat l_le_i Hred. + + simp type_interp in Hlog_v1. + destruct Hlog_v1 as (lref & -> & m & I & Hlook & ->). + have Hwsat₂ := wsat_wext _ _ _ _ Hwsat. + specialize (Hwsat₂ _ W₃_sup_W₂). + eapply wsat_lookup in Hwsat₂; last exact Hlook. + destruct Hwsat₂ as (h₂ & h₂_ss_h & (v3 & -> & Hty3)). + have Hlook' : h !! lref = Some v3. + { + eapply lookup_weaken; [ | exact h₂_ss_h ]. + apply lookup_insert. + } + have Hlook'' : ∃ m', W₃ !! m' = Some (λ σ' : heap, ∃ v, σ' = <[lref:=v]> ∅ ∧ TY 0; ∅ ⊢ v : a). + { + eapply wext_lookup. + exact W₃_sup_W₂. + exact Hlook. + } + + eapply store_nsteps_inv in Hred as [ (-> & -> & -> & Hnred) | (-> & Hstep) ]. + - exfalso; apply Hnred. + + econstructor; eexists; eapply base_contextual_step; eapply StoreS. + exact Hlook'. + rewrite to_of_val. + reflexivity. + - have Hunit : e' = Lit (LitUnit). + { + inversion Hstep; done. + } + have Hheap : h' = <[lref := v2]> h. + { + inversion Hstep. + rewrite to_of_val in H5. + injection H5; intros <-. + reflexivity. + } + + rewrite Hunit Hheap. + exists #(). + exists W₃. + repeat split; [ reflexivity | | simp type_interp; reflexivity]. + + destruct Hlook'' as (m' & Hlook''). + eapply wsat_update; [ exact Hwsat | | ]. + exact Hlook''. + intros σ (v4 & -> & Hty4). + split. + eexists; apply lookup_insert. + exists v2. + split. + apply insert_insert. + + rewrite syn_fo_typed_val. + exact Hlog_v2. +Qed. diff --git a/theories/type_systems/systemf_mu_state/types.v b/theories/type_systems/systemf_mu_state/types.v index 0b020ed..9e8a93c 100644 --- a/theories/type_systems/systemf_mu_state/types.v +++ b/theories/type_systems/systemf_mu_state/types.v @@ -688,6 +688,13 @@ Lemma store_inversion Σ n Γ e1 e2 B: ∃ A, B = Unit ∧ TY Σ; n; Γ ⊢ e1 : Ref A ∧ TY Σ; n; Γ ⊢ e2 : A. Proof. inversion 1; subst; eauto. Qed. +Lemma heap_inversion {Σ n Γ} {l : loc} {A}: + TY Σ; n; Γ ⊢ #l : Ref A → + Σ !! l = Some A. +Proof. + inversion 1; subst; eauto. +Qed. + Lemma typed_substitutivity Σ n e e' Γ (x: string) A B : heap_ctx_wf 0 Σ → TY Σ; 0; ∅ ⊢ e' : A → @@ -1173,7 +1180,18 @@ Proof. - rewrite lookup_insert_ne //=. eauto. Qed. - +Lemma heap_type_lookup {Σ n h l v A}: + heap_type h Σ → + heap_ctx_wf n Σ → + Σ !! l = Some A → + h !! l = Some v → + TY Σ; 0; ∅ ⊢ v : A. +Proof. + intros Hhty Hwf HΣl Hhl. + destruct (Hhty l A HΣl) as (v' & Heq & res). + rewrite Heq in Hhl; injection Hhl; intros ->. + exact res. +Qed. Lemma typed_preservation_base_step Σ e e' h h' A: heap_ctx_wf 0 Σ → @@ -1245,16 +1263,33 @@ Proof. exists Σ; split_and!; [done..|]. eapply unroll_inversion in Hty as (B & -> & Hty). eapply roll_inversion in Hty as (C & Heq & Hty). injection Heq as ->. done. - - (* new *) - (* TODO: exercise *) - admit. - - (* load *) - (* TODO: exercise *) - admit. - - (* store *) - (* TODO: exercise *) - admit. -Admitted. + - eapply new_inversion in Hty as (B & -> & Hty). + (* Welcome to underscore land *) + have Hhty2 := heap_type_insert _ _ _ _ _ _ Hhty H Hty H0. + exists (<[ l := B ]> Σ). + repeat split. + + eapply (heap_ctx_insert _ _ _ _ Hhty H). + + rewrite init_heap_singleton. + (* Imagine flagging your functions as simpl *) + rewrite insert_union_singleton_l. + exact Hhty2. + + eapply heap_ctx_wf_insert. + assumption. + eapply syn_typed_wf. + exact (ctx_wf_empty 0). + exact Hwf'. + exact Hty. + + econstructor. + by apply lookup_insert. + - exists Σ; split_and!; [done..|]. + eapply load_inversion in Hty. + eapply heap_inversion in Hty. + exact (heap_type_lookup Hhty Hwf' Hty H). + - eapply store_inversion in Hty as (B & -> & Hty₁ & Hty₂). + exists Σ; split_and!; try done. + apply heap_inversion in Hty₁. + eapply heap_type_update; [ assumption | exact Hty₁ | exact Hty₂ | exact H0 ]. +Qed. Lemma typed_preservation Σ e e' h h' A: heap_ctx_wf 0 Σ →