Finished first iteration of dist language

parent c5ae06a7
Pipeline #6133 failed with stages
in 0 seconds
......@@ -75,6 +75,19 @@ theories/heap_lang/lib/ticket_lock.v
theories/heap_lang/lib/counter.v
theories/heap_lang/proofmode.v
theories/heap_lang/adequacy.v
theories/dist_lang/lang.v
theories/dist_lang/tactics.v
theories/dist_lang/lifting.v
theories/dist_lang/notation.v
theories/dist_lang/lib/spawn.v
theories/dist_lang/lib/par.v
theories/dist_lang/lib/assert.v
theories/dist_lang/lib/lock.v
theories/dist_lang/lib/spin_lock.v
theories/dist_lang/lib/ticket_lock.v
theories/dist_lang/lib/counter.v
theories/dist_lang/proofmode.v
theories/dist_lang/adequacy.v
theories/proofmode/base.v
theories/proofmode/tokens.v
theories/proofmode/coq_tactics.v
......
From iris.program_logic Require Export weakestpre adequacy.
From iris.heap_lang Require Export lifting.
From iris.dist_lang Require Export lifting.
From iris.algebra Require Import auth.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
......
This diff is collapsed.
This diff is collapsed.
From iris.base_logic Require Export gen_heap.
From iris.program_logic Require Export weakestpre lifting.
From iris.program_logic Require Import ectx_lifting.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics.
From iris.dist_lang Require Export lang.
From iris.dist_lang Require Import tactics.
From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps.
Set Default Proof Using "Type".
......@@ -15,7 +15,7 @@ Class heapG Σ := HeapG {
heapG_gen_heapG :> gen_heapG loc val Σ
}.
Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
Instance heapG_irisG `{heapG Σ} : irisG dist_lang Σ := {
iris_invG := heapG_invG;
state_interp := gen_heap_ctx
}.
......
From iris.program_logic Require Import language.
From iris.heap_lang Require Export lang tactics.
From iris.dist_lang Require Export lang tactics.
Set Default Proof Using "Type".
Coercion LitInt : Z >-> base_lit.
......@@ -153,3 +153,8 @@ Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
(Match e0 BAnon e1 x%bind e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope.
Definition tmptmp := true && false.
Definition tmp := 'let:' x := #1 in #1.
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Export tactics lifting.
From iris.dist_lang Require Export tactics lifting.
Set Default Proof Using "Type".
Import uPred.
......
From iris.heap_lang Require Export lang.
From iris.dist_lang Require Export lang.
Set Default Proof Using "Type".
Import heap_lang.
Import dist_lang.
(** We define an alternative representation of expressions in which the
embedding of values and closed expressions is explicit. By reification of
......@@ -9,8 +9,8 @@ checking, atomic checking, and conversion into values, by computation. *)
Module W.
Inductive expr :=
(* Value together with the original expression *)
| Val (v : val) (e : heap_lang.expr) (H : to_val e = Some v)
| ClosedExpr (e : heap_lang.expr) `{!Closed [] e}
| Val (v : val) (e : dist_lang.expr) (H : to_val e = Some v)
| ClosedExpr (e : dist_lang.expr) `{!Closed [] e}
(* Base lambda calculus *)
| Var (x : string)
| Rec (f x : binder) (e : expr)
......@@ -37,62 +37,62 @@ Inductive expr :=
| CAS (e0 : expr) (e1 : expr) (e2 : expr)
| FAA (e1 : expr) (e2 : expr).
Fixpoint to_expr (e : expr) : heap_lang.expr :=
Fixpoint to_expr (e : expr) : dist_lang.expr :=
match e with
| Val v e' _ => e'
| ClosedExpr e => e
| Var x => heap_lang.Var x
| Rec f x e => heap_lang.Rec f x (to_expr e)
| App e1 e2 => heap_lang.App (to_expr e1) (to_expr e2)
| Lit l => heap_lang.Lit l
| UnOp op e => heap_lang.UnOp op (to_expr e)
| BinOp op e1 e2 => heap_lang.BinOp op (to_expr e1) (to_expr e2)
| If e0 e1 e2 => heap_lang.If (to_expr e0) (to_expr e1) (to_expr e2)
| Pair e1 e2 => heap_lang.Pair (to_expr e1) (to_expr e2)
| Fst e => heap_lang.Fst (to_expr e)
| Snd e => heap_lang.Snd (to_expr e)
| InjL e => heap_lang.InjL (to_expr e)
| InjR e => heap_lang.InjR (to_expr e)
| Case e0 e1 e2 => heap_lang.Case (to_expr e0) (to_expr e1) (to_expr e2)
| Fork e => heap_lang.Fork (to_expr e)
| Alloc e => heap_lang.Alloc (to_expr e)
| Load e => heap_lang.Load (to_expr e)
| Store e1 e2 => heap_lang.Store (to_expr e1) (to_expr e2)
| CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
| FAA e1 e2 => heap_lang.FAA (to_expr e1) (to_expr e2)
| Var x => dist_lang.Var x
| Rec f x e => dist_lang.Rec f x (to_expr e)
| App e1 e2 => dist_lang.App (to_expr e1) (to_expr e2)
| Lit l => dist_lang.Lit l
| UnOp op e => dist_lang.UnOp op (to_expr e)
| BinOp op e1 e2 => dist_lang.BinOp op (to_expr e1) (to_expr e2)
| If e0 e1 e2 => dist_lang.If (to_expr e0) (to_expr e1) (to_expr e2)
| Pair e1 e2 => dist_lang.Pair (to_expr e1) (to_expr e2)
| Fst e => dist_lang.Fst (to_expr e)
| Snd e => dist_lang.Snd (to_expr e)
| InjL e => dist_lang.InjL (to_expr e)
| InjR e => dist_lang.InjR (to_expr e)
| Case e0 e1 e2 => dist_lang.Case (to_expr e0) (to_expr e1) (to_expr e2)
| Fork e => dist_lang.Fork (to_expr e)
| Alloc e => dist_lang.Alloc (to_expr e)
| Load e => dist_lang.Load (to_expr e)
| Store e1 e2 => dist_lang.Store (to_expr e1) (to_expr e2)
| CAS e0 e1 e2 => dist_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
| FAA e1 e2 => dist_lang.FAA (to_expr e1) (to_expr e2)
end.
Ltac of_expr e :=
lazymatch e with
| heap_lang.Var ?x => constr:(Var x)
| heap_lang.Rec ?f ?x ?e => let e := of_expr e in constr:(Rec f x e)
| heap_lang.App ?e1 ?e2 =>
| dist_lang.Var ?x => constr:(Var x)
| dist_lang.Rec ?f ?x ?e => let e := of_expr e in constr:(Rec f x e)
| dist_lang.App ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(App e1 e2)
| heap_lang.Lit ?l => constr:(Lit l)
| heap_lang.UnOp ?op ?e => let e := of_expr e in constr:(UnOp op e)
| heap_lang.BinOp ?op ?e1 ?e2 =>
| dist_lang.Lit ?l => constr:(Lit l)
| dist_lang.UnOp ?op ?e => let e := of_expr e in constr:(UnOp op e)
| dist_lang.BinOp ?op ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op e1 e2)
| heap_lang.If ?e0 ?e1 ?e2 =>
| dist_lang.If ?e0 ?e1 ?e2 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(If e0 e1 e2)
| heap_lang.Pair ?e1 ?e2 =>
| dist_lang.Pair ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Pair e1 e2)
| heap_lang.Fst ?e => let e := of_expr e in constr:(Fst e)
| heap_lang.Snd ?e => let e := of_expr e in constr:(Snd e)
| heap_lang.InjL ?e => let e := of_expr e in constr:(InjL e)
| heap_lang.InjR ?e => let e := of_expr e in constr:(InjR e)
| heap_lang.Case ?e0 ?e1 ?e2 =>
| dist_lang.Fst ?e => let e := of_expr e in constr:(Fst e)
| dist_lang.Snd ?e => let e := of_expr e in constr:(Snd e)
| dist_lang.InjL ?e => let e := of_expr e in constr:(InjL e)
| dist_lang.InjR ?e => let e := of_expr e in constr:(InjR e)
| dist_lang.Case ?e0 ?e1 ?e2 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(Case e0 e1 e2)
| heap_lang.Fork ?e => let e := of_expr e in constr:(Fork e)
| heap_lang.Alloc ?e => let e := of_expr e in constr:(Alloc e)
| heap_lang.Load ?e => let e := of_expr e in constr:(Load e)
| heap_lang.Store ?e1 ?e2 =>
| dist_lang.Fork ?e => let e := of_expr e in constr:(Fork e)
| dist_lang.Alloc ?e => let e := of_expr e in constr:(Alloc e)
| dist_lang.Load ?e => let e := of_expr e in constr:(Load e)
| dist_lang.Store ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Store e1 e2)
| heap_lang.CAS ?e0 ?e1 ?e2 =>
| dist_lang.CAS ?e0 ?e1 ?e2 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(CAS e0 e1 e2)
| heap_lang.FAA ?e1 ?e2 =>
| dist_lang.FAA ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(FAA e1 e2)
| to_expr ?e => e
| of_val ?v => constr:(Val v (of_val v) (to_of_val v))
......@@ -115,7 +115,7 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
| If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
is_closed X e0 && is_closed X e1 && is_closed X e2
end.
Lemma is_closed_correct X e : is_closed X e heap_lang.is_closed X (to_expr e).
Lemma is_closed_correct X e : is_closed X e dist_lang.is_closed X (to_expr e).
Proof.
revert X.
induction e; naive_solver eauto using is_closed_to_val, is_closed_weaken_nil.
......@@ -138,14 +138,14 @@ Fixpoint to_val (e : expr) : option val :=
| _ => None
end.
Lemma to_val_Some e v :
to_val e = Some v heap_lang.to_val (to_expr e) = Some v.
to_val e = Some v dist_lang.to_val (to_expr e) = Some v.
Proof.
revert v. induction e; intros; simplify_option_eq; rewrite ?to_of_val; auto.
- do 2 f_equal. apply proof_irrel.
- exfalso. unfold Closed in *; eauto using is_closed_correct.
Qed.
Lemma to_val_is_Some e :
is_Some (to_val e) is_Some (heap_lang.to_val (to_expr e)).
is_Some (to_val e) is_Some (dist_lang.to_val (to_expr e)).
Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
......@@ -174,7 +174,7 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
| FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
end.
Lemma to_expr_subst x er e :
to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
to_expr (subst x er e) = dist_lang.subst x (to_expr er) (to_expr e).
Proof.
induction e; simpl; repeat case_decide;
f_equal; eauto using subst_is_closed_nil, is_closed_to_val, eq_sym.
......
(** This file is essentially a bunch of testcases. *)
From iris.program_logic Require Export weakestpre hoare.
From iris.dist_lang Require Export lang.
From iris.dist_lang Require Import adequacy.
From iris.dist_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Section LiftingTests.
Context `{heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Definition simpl_test :
(10 = 4 + 6)%nat -
WP let: "x" := ref #1 in "x" <- !"x";; !"x" {{ v, v = #1 }}.
Proof.
iIntros "?". wp_alloc l. repeat (wp_pure _) || wp_load || wp_store.
match goal with
| |- context [ (10 = 4 + 6)%nat ] => done
end.
Qed.
Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}%I.
Proof.
iIntros "". rewrite /heap_e.
wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
Qed.
Definition heap_e2 : expr :=
let: "x" := ref #1 in
let: "y" := ref #1 in
"x" <- !"x" + #1 ;; !"x".
Lemma heap_e2_spec E : WP heap_e2 @ E {{ v, v = #2 }}%I.
Proof.
iIntros "". rewrite /heap_e2.
wp_alloc l. wp_let. wp_alloc l'. wp_let.
wp_load. wp_op. wp_store. wp_load. done.
Qed.
Definition heap_e3 : expr :=
let: "x" := #true in
let: "f" := λ: "z", "z" + #1 in
if: "x" then "f" #0 else "f" #1.
Lemma heap_e3_spec E : WP heap_e3 @ E {{ v, v = #1 }}%I.
Proof.
iIntros "". rewrite /heap_e3.
by repeat (wp_pure _).
Qed.
Definition heap_e4 : expr :=
let: "x" := (let: "y" := ref (ref #1) in ref "y") in
! ! !"x".
Lemma heap_e4_spec : WP heap_e4 {{ v, v = #1 }}%I.
Proof.
rewrite /heap_e4. wp_alloc l. wp_alloc l'. wp_let.
wp_alloc l''. wp_let. by repeat wp_load.
Qed.
Definition heap_e5 : expr :=
let: "x" := ref (ref #1) in FAA (!"x") (#10 + #1) + ! !"x".
Lemma heap_e5_spec E : WP heap_e5 @ E {{ v, v = #13 }}%I.
Proof.
rewrite /heap_e5. wp_alloc l. wp_alloc l'. wp_let.
wp_load. wp_op. wp_faa. do 2 wp_load. wp_op. done.
Qed.
Definition FindPred : val :=
rec: "pred" "x" "y" :=
let: "yp" := "y" + #1 in
if: "yp" < "x" then "pred" "x" "yp" else "y".
Definition Pred : val :=
λ: "x",
if: "x" #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
Lemma FindPred_spec n1 n2 E Φ :
n1 < n2
Φ #(n2 - 1) - WP FindPred #n2 #n1 @ E {{ Φ }}.
Proof.
iIntros (Hn) "HΦ". iLöb as "IH" forall (n1 Hn).
wp_rec. wp_let. wp_op. wp_let.
wp_op; case_bool_decide; wp_if.
- iApply ("IH" with "[%] HΦ"). omega.
- by assert (n1 = n2 - 1) as -> by omega.
Qed.
Lemma Pred_spec n E Φ : Φ #(n - 1) - WP Pred #n @ E {{ Φ }}.
Proof.
iIntros "HΦ". wp_lam.
wp_op. case_bool_decide; wp_if.
- wp_op. wp_op.
wp_apply FindPred_spec; first omega.
wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
- wp_apply FindPred_spec; eauto with omega.
Qed.
Lemma Pred_user E :
(WP let: "x" := Pred #42 in Pred "x" @ E {{ v, v = #40 }})%I.
Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
End LiftingTests.
Locate adequate.
Locate heap_e.
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).
Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment