Bit flipping example

- Add more binary ops to the language
- An example refinement for module types

F_mu_ref_conc/context_refinement.v

@@ -16,7 +16,7 @@ Inductive ctx_item :=
   | CTX_CaseL (e1 : expr) (e2 : expr)
   | CTX_CaseM (e0 : expr) (e2 : expr)
   | CTX_CaseR (e0 : expr) (e1 : expr)
-  (* Nat bin op *)
+  (* Bin op *)
   | CTX_BinOpL (op : binop) (e2 : expr)
   | CTX_BinOpR (op : binop) (e1 : expr)
   (* If *)
@@ -121,12 +121,22 @@ Inductive typed_ctx_item :
   | TP_CTX_IfR Γ e0 e1 τ :
      typed Γ e0 (TBool) → typed Γ e1 τ →
      typed_ctx_item (CTX_IfR e0 e1) Γ τ Γ τ
-  | TP_CTX_BinOpL op Γ e2 :
+  | TP_CTX_BinOpL_Nat op Γ e2 τ :
      typed Γ e2 TNat →
-     typed_ctx_item (CTX_BinOpL op e2) Γ TNat Γ (binop_res_type op)
-  | TP_CTX_BinOpR op e1 Γ :
+     binop_nat_res_type op = Some τ →
+     typed_ctx_item (CTX_BinOpL op e2) Γ TNat Γ τ
+  | TP_CTX_BinOpR_Nat op e1 Γ τ :
      typed Γ e1 TNat →
-     typed_ctx_item (CTX_BinOpR op e1) Γ TNat Γ (binop_res_type op)
+     binop_nat_res_type op = Some τ →
+     typed_ctx_item (CTX_BinOpR op e1) Γ TNat Γ τ
+  | TP_CTX_BinOpL_Bool op Γ e2 τ :
+     typed Γ e2 TBool →
+     binop_bool_res_type op = Some τ →
+     typed_ctx_item (CTX_BinOpL op e2) Γ TBool Γ τ
+  | TP_CTX_BinOpR_Bool op e1 Γ τ :
+     typed Γ e1 TBool →
+     binop_bool_res_type op = Some τ →
+     typed_ctx_item (CTX_BinOpR op e1) Γ TBool Γ τ
   | TP_CTX_Fold Γ τ :
      typed_ctx_item CTX_Fold Γ τ.[(TRec τ)/] Γ (TRec τ)
   | TP_CTX_Unfold Γ τ :
@@ -313,6 +323,10 @@ Section bin_log_related_under_typed_ctx.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_nat_binop with "[]"); try fundamental; eauto.
         iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_bool_binop with "[]"); try fundamental; eauto.
+        iApply (IHK with "[Hrel]"); auto.
+      + iApply (bin_log_related_bool_binop with "[]"); try fundamental; eauto.
+        iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_fold with "[]"); try fundamental.
         iApply (IHK with "[Hrel]"); auto.
       + iApply (bin_log_related_unfold with "[]"); auto; try fundamental.

F_mu_ref_conc/examples/bit.v

+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth.
+From iris.base_logic Require Import lib.auth.
+From iris_logrel.F_mu_ref_conc Require Export examples.lock.
+From iris_logrel.F_mu_ref_conc Require Import tactics rel_tactics soundness_binary relational_properties.
+From iris.program_logic Require Import adequacy.
+
+From iris_logrel.F_mu_ref_conc Require Import hax.
+
+Definition bit_bool : val :=
+  PackV ((λ: "b", "b"), (λ: "b", BinOp Xor "b" (#♭v true)), #♭v true).
+
+Definition flip_nat : val := λ: "n",
+  if: BinOp Eq "n" (#n 0)
+  then (#n 1)
+  else (#n 0).
+Definition bit_nat : val :=
+  PackV ((λ: "b", BinOp Eq "b" (#n 0)), flip_nat, #nv 0).
+
+Section bit_refinement.
+  Context `{logrelG Σ}.
+  Variable (Δ : list (prodC valC valC -n> iProp Σ)).
+  
+  Definition bitτ : type :=
+    (TExists (TProd (TProd (TArrow (TVar 0) (TBool))
+                           (TArrow (TVar 0) (TVar 0)))
+                           (TVar 0))).
+  Lemma bit_bool_type Γ :
+    typed Γ bit_bool bitτ.
+  Proof. unfold bitτ. simpl. unlock. solve_typed.
+    (* TODO: solve_typed does not solve this one without simplifying/unlocking *)
+  Qed.
+
+  Hint Resolve bit_bool_type : typeable.
+
+  Lemma flip_nat_type Γ :
+    typed Γ flip_nat (TArrow TNat TNat).
+  Proof. solve_typed. Qed.
+
+  Hint Resolve flip_nat_type : typeable.
+  
+  Lemma bit_nat_type Γ :
+    typed Γ bit_nat bitτ.
+  Proof.
+    unfold bitτ.
+    simpl. unlock.
+    solve_typed.
+  Qed.
+
+  Hint Resolve bit_nat_type : typeable.
+  
+  Program Definition bitτi : prodC valC valC -n> iProp Σ := λne vv,
+    (⌜vv.1 = #♭v true⌝ ∗ ⌜vv.2 = #nv 0⌝ ∨ ⌜vv.1 = #♭v false⌝ ∗ ⌜vv.2 = #nv 1⌝)%I.
+  Next Obligation. solve_proper. Qed.
+
+  Instance bitτi_persistent ww : PersistentP (bitτi ww).
+  Proof. apply _. Qed.
+
+  Lemma bit_prerefinement Γ E1 :
+    {E1,E1;Δ;Γ} ⊨ bit_bool ≤log≤ bit_nat : bitτ.
+  Proof.
+    simpl.
+    iApply (bin_log_related_pack _ bitτi).
+    iApply bin_log_related_pair.
+    iApply bin_log_related_pair.
+    - iApply bin_log_related_arrow; try by unlock.
+      iAlways. iIntros ([v1 v2]) "/= #%".
+      unlock.
+      rel_rec_l.
+      rel_rec_r.
+      destruct H0 as [Hv | Hv]; inversion Hv; subst; clear.
+      (* ^ TODO simplify_eq does not work *)
+      all: rel_op_r.
+      all: rel_vals; simpl; eauto.
+    - unfold flip_nat.
+      iApply bin_log_related_arrow; try by unlock.
+      iAlways. iIntros ([v1 v2]) "/= #%".
+      unlock.
+      rel_rec_l.
+      rel_rec_r.
+      destruct H0 as [Hv | Hv]; inversion Hv; subst; clear.
+      (* ^ TODO simplify_eq does not work *)
+      all: rel_op_l; simpl.
+      all: rel_op_r; simpl.
+      + rel_if_true_r. rel_vals; simpl; eauto.
+      + rel_if_false_r. rel_vals; simpl; eauto.
+    - rel_vals; simpl; eauto.
+  Qed.
+
+End bit_refinement.

F_mu_ref_conc/examples/counter.v

@@ -100,7 +100,7 @@ Section CG_Counter.
     iApply wp_rec; eauto.
     iNext. simpl.
     wp_bind (BinOp _ _ _).
-    iApply (wp_nat_binop). iNext. iModIntro. simpl.    
+    iApply (wp_nat_binop);eauto. iNext. iModIntro. simpl.    
     wp_bind (CAS _ _ _).    
     iApply (wp_cas_suc with "[Hx]"); auto.
     iNext. iIntros "Hx".

F_mu_ref_conc/fundamental_binary.v

@@ -294,24 +294,49 @@ Section masked.
       smart_bind j (env_subst _ e2) (env_subst _ e2') "IH3" v v' "?".
   Qed.
 
-  Lemma bin_log_related_nat_binop Δ Γ op e1 e2 e1' e2' :
+  Lemma bin_log_related_nat_binop Δ Γ op e1 e2 e1' e2' τ :
     ↑specN ⊆ E →
+    binop_nat_res_type op = Some τ →
     {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TNat -∗
     {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : TNat -∗
-    {E,E;Δ;Γ} ⊨ BinOp op e1 e2 ≤log≤ BinOp op e1' e2' : binop_res_type op.
+    {E,E;Δ;Γ} ⊨ BinOp op e1 e2 ≤log≤ BinOp op e1' e2' : τ.
   Proof.
     rewrite bin_log_related_eq.
-    iIntros (?) "IH1 IH2".
+    iIntros (? Hopτ) "IH1 IH2".
     iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
     smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
     smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" w w' "IH2".
     iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
     iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
     iApply fupd_wp.
-    tp_nat_binop j; eauto; tp_normalise j.
-    iApply wp_nat_binop. iModIntro. iExists _; iSplitL; eauto.
+    destruct (binop_nat_typed_safe op n n' _ Hopτ) as [v' Hopv'].
+    tp_binop j; eauto; tp_normalise j.
+    iApply wp_nat_binop; eauto. iModIntro. iExists _; iSplitL; eauto.
     repeat iModIntro.
-    destruct op; simpl; try destruct eq_nat_dec; try destruct le_dec;
+    destruct op; simpl in Hopv'; simplify_eq/=; try destruct eq_nat_dec; try destruct le_dec;
+      try destruct lt_dec; eauto.
+  Qed.
+
+  Lemma bin_log_related_bool_binop Δ Γ op e1 e2 e1' e2' τ :
+    ↑specN ⊆ E →
+    binop_bool_res_type op = Some τ →
+    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TBool -∗
+    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : TBool -∗
+    {E,E;Δ;Γ} ⊨ BinOp op e1 e2 ≤log≤ BinOp op e1' e2' : τ.
+  Proof.
+    rewrite bin_log_related_eq.
+    iIntros (? Hopτ) "IH1 IH2".
+    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
+    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
+    smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" w w' "IH2".
+    iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
+    iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
+    iApply fupd_wp.
+    destruct (binop_bool_typed_safe op n n' _ Hopτ) as [v' Hopv'].
+    tp_binop j; eauto; tp_normalise j.
+    iApply wp_nat_binop; eauto. iModIntro. iExists _; iSplitL; eauto.
+    repeat iModIntro.
+    destruct op; simpl in Hopv'; simplify_eq/=; try destruct eq_nat_dec; try destruct le_dec;
       try destruct lt_dec; eauto.
   Qed.
 
@@ -615,6 +640,7 @@ Section masked.
     - by iApply bin_log_related_nat.
     - by iApply bin_log_related_bool.
     - by iApply (bin_log_related_nat_binop with "[]").
+    - by iApply (bin_log_related_bool_binop with "[]").
     - by iApply (bin_log_related_pair with "[]").
     - by iApply bin_log_related_fst.
     - by iApply bin_log_related_snd.

F_mu_ref_conc/lang.v

@@ -9,8 +9,8 @@ Module lang.
   Instance loc_dec_eq (l l' : loc) : Decision (l = l') := _.
 
   (** ** Expressions *)
-  Inductive binop := Add | Sub | Eq | Le | Lt.
-
+  Inductive binop := Add | Sub | Eq | Le | Lt | Xor.
+  
   Instance binop_dec_eq (op op' : binop) : Decision (op = op').
   Proof. solve_decision. Defined.
 
@@ -110,13 +110,16 @@ Module lang.
   Notation "'#♭v' b" := (BoolV b) (at level 20).
   Notation "'#nv' n" := (NatV n) (at level 20).
 
-  Fixpoint binop_eval (op : binop) : nat → nat → val :=
-    match op with
-    | Add => λ a b, #nv(a + b)
-    | Sub => λ a b, #nv(a - b)
-    | Eq => λ a b, if (eq_nat_dec a b) then #♭v true else #♭v false
-    | Le => λ a b, if (le_dec a b) then #♭v true else #♭v false
-    | Lt => λ a b, if (lt_dec a b) then #♭v true else #♭v false
+  Fixpoint binop_eval (op : binop) (v1 v2 : val) : option val :=
+    match op,v1,v2 with
+    | Add,#nv a,#nv b => Some $ #nv(a + b)
+    | Sub,#nv a,#nv b => Some $ #nv(a - b)
+    | Eq,#nv a,#nv b => Some $ if (eq_nat_dec a b) then #♭v true else #♭v false
+    | Eq,#♭v a,#♭v b => Some $ #♭v(eqb a b)
+    | Le,#nv a,#nv b => Some $ if (le_dec a b) then #♭v true else #♭v false
+    | Lt,#nv a,#nv b => Some $ if (lt_dec a b) then #♭v true else #♭v false
+    | Xor,#♭v a,#♭v b => Some $ #♭v(xorb a b)
+    | _,_,_ => None
     end.
   Instance val_inh : Inhabited val := populate UnitV.
 
@@ -296,9 +299,12 @@ Module lang.
       to_val e0 = Some v0 →
       e' = App e2 e0 →
       head_step (Case (InjR e0) e1 e2) σ e' σ []
-    (* nat bin op *)
-  | BinOpS op a b σ :
-      head_step (BinOp op (#n a) (#n b)) σ (of_val (binop_eval op a b)) σ []
+  (* nat bin op *)
+  | BinOpS op e1 e2 v1 v2 v σ :
+      to_val e1 = Some v1 →
+      to_val e2 = Some v2 →
+      binop_eval op v1 v2 = Some v →
+      head_step (BinOp op e1 e2) σ (of_val v) σ []
   (* If then else *)
   | IfFalse e1 e2 σ :
       head_step (If (#♭ false) e1 e2) σ e2 σ []
@@ -340,15 +346,6 @@ Module lang.
      σ !! l = Some v1 →
      head_step (CAS (Loc l) e1 e2) σ (#♭ true) (<[l:=v2]>σ) [].
 
-  Lemma binop_eval_closed op a b x es :
-  subst x es (of_val (binop_eval op a b)) = (of_val (binop_eval op a b)).
-  Proof. 
-    induction op; simpl; eauto;
-    match goal with
-    | |- context[if ?H then _ else _] => destruct H; auto
-    end.
-  Qed.
-  
   Lemma fill_item_val Ki e :
     is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
   Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
@@ -444,4 +441,3 @@ Ltac inv_head_step :=
      and can thus better be avoided. *)
      inversion H; subst; clear H
   end.
-

F_mu_ref_conc/rel_tactics.v

@@ -258,13 +258,16 @@ Tactic Notation "rel_case_inr_l" :=
     |try solve_closed
     |iNext (* new goal *)].
 
-Lemma tac_rel_binop_l `{logrelG Σ} Δ E1 Γ e K' op a b eres t τ Δ' :
-  e = fill K' (BinOp op (#n a) (#n b)) →
-  eres = of_val (binop_eval op a b) →
+Lemma tac_rel_binop_l `{logrelG Σ} Δ E1 Γ e K' op e1 e2 v1 v2 v eres t τ Δ' :
+  e = fill K' (BinOp op e1 e2) →
+  to_val e1 = Some v1 →
+  to_val e2 = Some v2 →
+  binop_eval op v1 v2 = Some v →
+  eres = of_val v →
   (Δ ⊢ ▷ bin_log_related E1 E1 Δ' Γ (fill K' eres) t τ) →
   (Δ ⊢ bin_log_related E1 E1 Δ' Γ e t τ).
 Proof.
-  intros ???.
+  intros ??????.
   subst e eres.
   rewrite -(bin_log_related_binop_l Δ' Γ E1); eassumption.
 Qed.
@@ -273,6 +276,9 @@ Tactic Notation "rel_op_l" :=
   iStartProof;
   eapply (tac_rel_binop_l);
     [tac_bind_helper (* e = fill K' ... *)
+    |solve_to_val
+    |solve_to_val
+    |fast_done
     |simpl; reflexivity (* eres = of_val .. *)
     |iNext (* new goal *)].
 
@@ -1002,13 +1008,16 @@ Tactic Notation "rel_if_r" :=
     |simpl; fast_done || fail "rel_if_r: cannot compute the boolean value"
     |simpl (* new goal *)].
 
-Lemma tac_rel_binop_r `{logrelG Σ} Δ E1 E2 Γ e K' op a b t Δ' τ :
+Lemma tac_rel_binop_r `{logrelG Σ} Δ E1 E2 Γ e K' op e1 e2 v1 v2 v t Δ' τ :
   nclose specN ⊆ E1 →
-  e = fill K' (BinOp op (#n a) (#n b)) →
-  (Δ ⊢ bin_log_related E1 E2 Δ' Γ t (fill K' (of_val (binop_eval op a b))) τ) →
+  e = fill K' (BinOp op e1 e2) →
+  to_val e1 = Some v1 →
+  to_val e2 = Some v2 →
+  binop_eval op v1 v2 = Some v →
+  (Δ ⊢ bin_log_related E1 E2 Δ' Γ t (fill K' (of_val v)) τ) →
   (Δ ⊢ bin_log_related E1 E2 Δ' Γ t e τ).
 Proof.
-  intros ???.
+  intros ??????.
   subst e.
   rewrite -(bin_log_related_binop_r Δ' Γ); eassumption.
 Qed.
@@ -1018,6 +1027,9 @@ Tactic Notation "rel_op_r" :=
   eapply (tac_rel_binop_r);
     [solve_ndisj || fail "rel_op_r: cannot prove 'nclose specN ⊆ ?'"
     |tac_bind_helper || fail "rel_op_r: cannot find an operator"
+    |solve_to_val
+    |solve_to_val
+    |(fast_done || eauto)
     |simpl (* new goal *)].
 
 (* TODO: tac_rel_pack_r *)

F_mu_ref_conc/relational_properties.v

@@ -282,11 +282,14 @@ Section properties.
     - by inv_head_step.
   Qed.
   
-  Lemma bin_log_related_binop_l Δ Γ E K op a b t τ :
-   ▷ ({E,E;Δ;Γ} ⊨ fill K (of_val (binop_eval op a b)) ≤log≤ t : τ)
-   ⊢ {E,E;Δ;Γ} ⊨ (fill K (BinOp op (#n a) (#n b))) ≤log≤ t : τ.
-  Proof.
-    iIntros "Hlog".
+  Lemma bin_log_related_binop_l Δ Γ E K op e1 e2 v1 v2 v t τ :
+    to_val e1 = Some v1 →
+    to_val e2 = Some v2 →
+    binop_eval op v1 v2 = Some v →
+   ▷ ({E,E;Δ;Γ} ⊨ fill K (of_val v) ≤log≤ t : τ)
+   ⊢ {E,E;Δ;Γ} ⊨ (fill K (BinOp op e1 e2)) ≤log≤ t : τ.
+  Proof.
+    iIntros (???) "Hlog".
     iApply (bin_log_pure_l with "Hlog"); auto; intros.
     - do 3 eexists. econstructor; eauto.
     - by inv_head_step.
@@ -669,12 +672,15 @@ Section properties.
     { econstructor; eauto. }
   Qed.
 
-  Lemma bin_log_related_binop_r Δ Γ E1 E2 K op a b t τ
+  Lemma bin_log_related_binop_r Δ Γ E1 E2 K op e1 e2 v1 v2 v t τ
    (Hspec : nclose specN ⊆ E1) :
-   {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (of_val (binop_eval op a b)) : τ
-   ⊢ {E1,E2;Δ;Γ} ⊨ t ≤log≤ (fill K (BinOp op (#n a) (#n b))) : τ.
+    to_val e1 = Some v1 →
+    to_val e2 = Some v2 →
+    binop_eval op v1 v2 = Some v →
+   {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (of_val v) : τ
+   ⊢ {E1,E2;Δ;Γ} ⊨ t ≤log≤ (fill K (BinOp op e1 e2)) : τ.
   Proof.
-    iIntros "Hlog".
+    iIntros (???) "Hlog".
     iApply (bin_log_pure_r with "Hlog"); auto; intros.
     { econstructor; eauto. }
   Qed.

F_mu_ref_conc/rules.v

@@ -197,8 +197,11 @@ Section lang_rules.
     intros; inv_head_step; eauto.
   Qed.
 
-  Lemma wp_nat_binop E op a b Φ :
-    ▷ (|={E}=> Φ (binop_eval op a b)) ⊢ WP BinOp op (#n a) (#n b) @ E {{ Φ }}.
+  Lemma wp_nat_binop E op e1 e2 v1 v2 v Φ :
+    to_val e1 = Some v1 →
+    to_val e2 = Some v2 →
+    binop_eval op v1 v2 = Some v →
+    ▷ (|={E}=> Φ v) ⊢ WP BinOp op e1 e2 @ E {{ Φ }}.
   Proof.
     intros. rewrite -(wp_lift_pure_det_head_step_no_fork (BinOp op _ _) (of_val _))
       -?wp_value_fupd'; eauto.

F_mu_ref_conc/rules_binary.v

@@ -340,11 +340,14 @@ Section cfg.
     spec_ctx ρ ∗ j ⤇ fill K (If (#♭ true) e1 e2) ={E}=∗ j ⤇ fill K e1.
   Proof. apply step_pure => σ; econstructor. Qed.
 
-  Lemma step_nat_binop E ρ j K op a b :
+  Lemma step_nat_binop E ρ j K op e1 e2 v1 v2 v :
+    to_val e1 = Some v1 →
+    to_val e2 = Some v2 →
+    binop_eval op v1 v2 = Some v →
     nclose specN ⊆ E →
-    spec_ctx ρ ∗ j ⤇ fill K (BinOp op (#n a) (#n b))
-      ={E}=∗ j ⤇ fill K (of_val (binop_eval op a b)).
-  Proof. apply step_pure => σ; econstructor. Qed.
+    spec_ctx ρ ∗ j ⤇ fill K (BinOp op e1 e2)
+      ={E}=∗ j ⤇ fill K (of_val v).
+  Proof. intros ???. apply step_pure => σ; econstructor; eauto. Qed.
 
   Lemma step_fork E ρ j K e :
     nclose specN ⊆ E →

F_mu_ref_conc/tactics.v

@@ -285,17 +285,20 @@ Tactic Notation "tp_rec" constr(j) :=
     |simpl_subst (* new goal *)].
 
 
-Lemma tac_tp_nat_binop `{logrelG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e op a b Q :
+Lemma tac_tp_nat_binop `{logrelG Σ} j Δ1 Δ2 E1 E2 ρ i1 i2 p K' e op e1 e2 v1 v2 v Q :
   nclose specN ⊆ E1 →
   envs_lookup i1 Δ1 = Some (p, spec_ctx ρ) →
   envs_lookup i2 Δ1 = Some (false, j ⤇ e)%I →
-  e = fill K' (BinOp op (#n a) (#n b)) →
+  e = fill K' (BinOp op e1 e2) →
+  to_val e1 = Some v1 →
+  to_val e2 = Some v2 →
+  binop_eval op v1 v2 = Some v →
   envs_simple_replace i2 false 
-    (Esnoc Enil i2 (j ⤇ fill K' (of_val (binop_eval op a b)))) Δ1 = Some Δ2 →
+    (Esnoc Enil i2 (j ⤇ fill K' (of_val v))) Δ1 = Some Δ2 →
   (Δ2 ⊢ |={E1,E2}=> Q) →
   (Δ1 ⊢ |={E1,E2}=> Q).
 Proof.
-  intros ??? Hfill ? HQ.
+  intros ??? Hfill ???? HQ.
   rewrite -(idemp uPred_and Δ1).
   rewrite {2}(envs_lookup_sound' Δ1). 2: apply H1.
   rewrite uPred.sep_elim_l uPred.always_and_sep_r.
@@ -312,17 +315,20 @@ Proof.
   done.
 Qed.
 
-Tactic Notation "tp_nat_binop" constr(j) :=
+Tactic Notation "tp_binop" constr(j) :=
   iStartProof;
   eapply (tac_tp_nat_binop j);
-    [solve_ndisj || fail "tp_nat_binop: cannot prove 'nclose specN ⊆ ?'"
-    |iAssumptionCore || fail "tp_nat_binop: cannot find spec_ctx" (* spec_ctx *)
-    |iAssumptionCore || fail "tp_nat_binop: cannot find '" j " ⤇ ?'" 
+    [solve_ndisj || fail "tp_binop: cannot prove 'nclose specN ⊆ ?'"
+    |iAssumptionCore || fail "tp_binop: cannot find spec_ctx" (* spec_ctx *)
+    |iAssumptionCore || fail "tp_binop: cannot find '" j " ⤇ ?'" 
     |tp_bind_helper
-    |env_cbv; reflexivity || fail "tp_nat_binop: this should not happen"
+    |solve_to_val || fail "tp_binop: cannot prove that the first argument is a value"
+    |solve_to_val || fail "tp_binop: cannot prove that the second argument is a value"
+    |(fast_done || auto) || fail "tp_binop: cannot evaluate the binop"
+    |env_cbv; reflexivity || fail "tp_binop: this should not happen"
     |(* new goal *)].
 
-Tactic Notation "tp_op" constr(j) := tp_nat_binop j.
+Tactic Notation "tp_op" constr(j) := tp_binop j.
 
 Lemma tac_tp_cas_fail `{logrelG Σ} j Δ1 Δ2 Δ3 E1 E2 ρ i1 i2 i3 p K' e l e1 e2 v' v1 v2 Q q :
   nclose specN ⊆ E1 →

F_mu_ref_conc/typing.v

@@ -21,11 +21,30 @@ Instance Rename_type : Rename type. derive. Defined.
 Instance Subst_type : Subst type. derive. Defined.
 Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
 
-Fixpoint binop_res_type (op : binop) : type :=
+Fixpoint binop_nat_res_type (op : binop) : option type :=
   match op with
-  | Add => TNat | Sub => TNat
-  | Eq => TBool | Le => TBool | Lt => TBool
+  | Add => Some TNat | Sub => Some TNat
+  | Eq => Some TBool | Le => Some TBool | Lt => Some TBool
+  | _ => None
   end.
+Fixpoint binop_bool_res_type (op : binop) : option type :=
+  match op with
+  | Xor => Some TBool | Eq => Some TBool
+  | _ => None
+  end.
+
+Lemma binop_nat_typed_safe (op : binop) (n1 n2 : nat) τ :
+  binop_nat_res_type op = Some τ → is_Some (binop_eval op (#nv n1) (#nv n2)).
+Proof.
+  destruct op; simpl; eauto.
+  inversion 1.
+Qed.
+
+Lemma binop_bool_typed_safe (op : binop) (b1 b2 : bool) τ :
+  binop_bool_res_type op = Some τ → is_Some (binop_eval op (#♭v b1) (#♭v b2)).
+Proof.
+  destruct op; simpl; eauto; try by inversion 1.
+Qed.
 
 Inductive EqType : type → Prop :=
   | EqTUnit : EqType TUnit
@@ -42,8 +61,14 @@ Inductive typed (Γ : stringmap type) : expr → type → Prop :=
   | Unit_typed : Γ ⊢ₜ Unit : TUnit
   | Nat_typed n : Γ ⊢ₜ #n n : TNat
   | Bool_typed b : Γ ⊢ₜ #♭ b : TBool
-  | BinOp_typed op e1 e2 :
-     Γ ⊢ₜ e1 : TNat → Γ ⊢ₜ e2 : TNat → Γ ⊢ₜ BinOp op e1 e2 : binop_res_type op
+  | BinOp_typed_nat op e1 e2 τ :      
+     Γ ⊢ₜ e1 : TNat → Γ ⊢ₜ e2 : TNat → 
+     binop_nat_res_type op = Some τ →
+     Γ ⊢ₜ BinOp op e1 e2 : τ
+  | BinOp_typed_bool op e1 e2 τ :
+     Γ ⊢ₜ e1 : TBool → Γ ⊢ₜ e2 : TBool → 
+     binop_bool_res_type op = Some τ →
+     Γ ⊢ₜ BinOp op e1 e2 : τ
   | Pair_typed e1 e2 τ1 τ2 : Γ ⊢ₜ e1 : τ1 → Γ ⊢ₜ e2 : τ2 → Γ ⊢ₜ Pair e1 e2 : TProd τ1 τ2
   | Fst_typed e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 → Γ ⊢ₜ Fst e : τ1
   | Snd_typed e τ1 τ2 : Γ ⊢ₜ e : TProd τ1 τ2 → Γ ⊢ₜ Snd e : τ2
@@ -95,16 +120,6 @@ Proof. eauto using TCAS. Qed.
 Hint Resolve TCAS' : typeable.
 Remove Hints TCAS : typeable.
 
-Lemma BINOP' Γ op e1 e2 τ :
-  Γ ⊢ₜ e1 : TNat →
-  Γ ⊢ₜ e2 : TNat → 
-  τ = binop_res_type op →
-  Γ ⊢ₜ BinOp op e1 e2 : τ.
-Proof. intros. subst τ. by econstructor. Qed.
-
-Hint Resolve BINOP' : typeable.
-Remove Hints BinOp_typed : typeable.
-
 Lemma TUNFOLD' Γ e τ τ' :
   Γ ⊢ₜ e : TRec τ →
   τ' = τ.[TRec τ/] →

_CoqProject

@@ -26,6 +26,7 @@ F_mu_ref_conc/examples/lock.v
 F_mu_ref_conc/examples/counter.v
 F_mu_ref_conc/examples/lateearlychoice.v
 F_mu_ref_conc/examples/par.v
+F_mu_ref_conc/examples/bit.v
 #F_mu_ref_conc/examples/stack/stack_rules.v
 #F_mu_ref_conc/examples/stack/CG_stack.v
 #F_mu_ref_conc/examples/stack/FG_stack.v