✨ Exercises 7

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.

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.

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.
 
 
 

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 Σ →