From b0de8229a8a98423d6651e6d5a4db52ec8ae5c1c Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 24 Apr 2018 10:30:18 +0200
Subject: [PATCH] Integers, booleans.

---
 _CoqProject                |  2 +
 opam                       |  2 +-
 theories/typing/bool.v     | 52 +++++++++++++++++++++++
 theories/typing/int.v      | 86 ++++++++++++++++++++++++++++++++++++++
 theories/typing/programs.v |  2 +-
 5 files changed, 142 insertions(+), 2 deletions(-)
 create mode 100644 theories/typing/bool.v
 create mode 100644 theories/typing/int.v

diff --git a/_CoqProject b/_CoqProject
index 3c9e5b6b..5bfa8d16 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -27,3 +27,5 @@ theories/typing/product.v
 theories/typing/sum.v
 theories/typing/uninit.v
 theories/typing/programs.v
+theories/typing/bool.v
+theories/typing/int.v
diff --git a/opam b/opam
index 960bbe4a..3020796f 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2018-04-23.0.2e828a7c") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2018-04-23.3.1dfd6ae7") | (= "dev") }
 ]
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
new file mode 100644
index 00000000..74433575
--- /dev/null
+++ b/theories/typing/bool.v
@@ -0,0 +1,52 @@
+From lrust.typing Require Export type.
+From lrust.typing Require Import programs.
+Set Default Proof Using "Type".
+
+Section bool.
+  Context `{typeG Σ}.
+
+  Program Definition bool : type :=
+    {| st_own tid vl :=
+         match vl return _ with
+         | [ VVal #(LitInt (0|1)) ] => True
+         | _ => False
+         end%I |}.
+  Next Obligation. intros ? [|[| |[[| |[|[]|]]|]] [|]]; auto. Qed.
+  Next Obligation. intros ? [|[| |[[| |[|[]|]]|]] [|]]; apply _. Qed.
+
+  Global Instance bool_wf : TyWf bool := { ty_lfts := []; ty_wf_E := [] }.
+
+  Global Instance bool_send : Send bool.
+  Proof. done. Qed.
+End bool.
+
+Section typing.
+  Context `{typeG Σ}.
+
+  Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
+  Proof.
+    iIntros (E L tid) "_ _ $ $ _". iApply wp_value.
+    rewrite tctx_interp_singleton tctx_hasty_val' //. by destruct b.
+  Qed.
+
+  Lemma type_bool (b : Datatypes.bool) E L C T x e :
+    Closed (x :b: []) e →
+    (∀ (v : val), typed_body E L C ((v ◁ bool) :: T) (subst' x v e)) -∗
+    typed_body E L C T (let: x := #b in e).
+  Proof. iIntros. iApply type_let; [apply type_bool_instr|solve_typing|done]. Qed.
+
+  Lemma type_if E L C T e1 e2 p:
+    p ◁ bool ∈ T →
+    typed_body E L C T e1 -∗ typed_body E L C T e2 -∗
+    typed_body E L C T (if: p then e1 else e2).
+  Proof.
+    iIntros (Hp) "He1 He2". iIntros (tid) "#LFT #HE Htl HL HC HT".
+    rewrite !(embed_big_sepL _ T).
+    iDestruct (bi.big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
+    rewrite -!(embed_big_sepL _ T).
+    wp_bind p. iApply (wp_hasty with "Hp").
+    iIntros ([[| |[|[]|]]|]) "_ /="; iIntros ([]); [|]; wp_case.
+    - iApply ("He2" with "LFT HE Htl HL HC HT").
+    - iApply ("He1" with "LFT HE Htl HL HC HT").
+  Qed.
+End typing.
diff --git a/theories/typing/int.v b/theories/typing/int.v
new file mode 100644
index 00000000..a4148890
--- /dev/null
+++ b/theories/typing/int.v
@@ -0,0 +1,86 @@
+From iris.proofmode Require Import tactics.
+From lrust.typing Require Export type.
+From lrust.typing Require Import bool programs.
+Set Default Proof Using "Type".
+
+Section int.
+  Context `{typeG Σ}.
+
+  Program Definition int : type :=
+    {| st_own tid vl :=
+         match vl return _ with
+         | [ VVal #(LitInt z)] => True
+         | _ => False
+         end%I |}.
+  Next Obligation. intros ? [|[| |[[| |]|]] [|]]; auto. Qed.
+  Next Obligation. intros ? [|[| |[[| |]|]] [|]]; apply _. Qed.
+
+  Global Instance int_wf : TyWf int := { ty_lfts := []; ty_wf_E := [] }.
+
+  Global Instance int_send : Send int.
+  Proof. done. Qed.
+End int.
+
+Section typing.
+  Context `{typeG Σ}.
+
+  Lemma type_int_instr (z : Z) : typed_val #z int.
+  Proof.
+    iIntros (E L tid) "_ _ $ $ _". iApply wp_value.
+    by rewrite tctx_interp_singleton tctx_hasty_val' //.
+  Qed.
+
+  Lemma type_int (z : Z) E L C T x e :
+    Closed (x :b: []) e →
+    (∀ (v : val), typed_body E L C ((v ◁ int) :: T) (subst' x v e)) -∗
+    typed_body E L C T (let: x := #z in e).
+  Proof. iIntros. iApply type_let; [apply type_int_instr|solve_typing|done]. Qed.
+
+  Lemma type_plus_instr E L p1 p2 :
+    typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
+  Proof.
+    iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
+    wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try iDestruct "H1" as %[].
+    wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try iDestruct "H2" as %[].
+    wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
+  Qed.
+
+  Lemma type_plus E L C T T' p1 p2 x e :
+    Closed (x :b: []) e →
+    tctx_extract_ctx E L [p1 ◁ int; p2 ◁ int] T T' →
+    (∀ (v : val), typed_body E L C ((v ◁ int) :: T') (subst' x v e)) -∗
+    typed_body E L C T (let: x := p1 + p2 in e).
+  Proof. iIntros. iApply type_let; [iApply type_plus_instr|solve_typing|done]. Qed.
+
+  Lemma type_minus_instr E L p1 p2 :
+    typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
+  Proof.
+    iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
+    wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try iDestruct "H1" as %[].
+    wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try iDestruct "H2" as %[].
+    wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
+  Qed.
+
+  Lemma type_minus E L C T T' p1 p2 x e :
+    Closed (x :b: []) e →
+    tctx_extract_ctx E L [p1 ◁ int; p2 ◁ int] T T' →
+    (∀ (v : val), typed_body E L C ((v ◁ int) :: T') (subst' x v e)) -∗
+    typed_body E L C T (let: x := p1 - p2 in e).
+  Proof. iIntros. iApply type_let; [apply type_minus_instr|solve_typing|done]. Qed.
+
+  Lemma type_le_instr E L p1 p2 :
+    typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
+  Proof.
+    iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
+    wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try iDestruct "H1" as %[].
+    wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try iDestruct "H2" as %[].
+    wp_op; case_bool_decide; by rewrite tctx_interp_singleton tctx_hasty_val' //.
+  Qed.
+
+  Lemma type_le E L C T T' p1 p2 x e :
+    Closed (x :b: []) e →
+    tctx_extract_ctx E L [p1 ◁ int; p2 ◁ int] T T' →
+    (∀ (v : val), typed_body E L C ((v ◁ bool) :: T') (subst' x v e)) -∗
+    typed_body E L C T (let: x := p1 ≤ p2 in e).
+  Proof. iIntros. iApply type_let; [apply type_le_instr|solve_typing|done]. Qed.
+End typing.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index fbd892e5..c13420bd 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -1,5 +1,5 @@
 From gpfsl.lang Require Import proofmode.
-From lrust.lang Require Import memcpy.
+From lrust.lang Require Export memcpy.
 From lrust.typing Require Export type lft_contexts type_context cont_context.
 Set Default Proof Using "Type".
 
-- 
GitLab