Commit fdc2167f authored by Léon Gondelman's avatar Léon Gondelman

separate tests for unknown case

parent b45f1e33
......@@ -15,6 +15,7 @@ theories/vcgen/denv.v
theories/vcgen/splitenv.v
theories/vcgen/vcgen.v
theories/vcgen/tests/basics.v
theories/vcgen/tests/unknowns.v
theories/vcgen/tests/test.v
theories/vcgen/tests/swap.v
theories/tests/test1.v
......
......@@ -16,3 +16,7 @@ Notation "e1 ;ᶜ e2" := (e1%E ;;;; e2%E)
format "'[' '[hv' '[' e1 ']' ;ᶜ ']' '/' e2 ']'") : expr_scope.
Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 +ᶜ e2" := (a_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 -ᶜ e2" := (a_bin_op MinusOp e1%E e2%E) (at level 80) : expr_scope.
Notation "'allocᶜ' e1" := (a_alloc e1%E) (at level 80) : expr_scope.
......@@ -136,76 +136,4 @@ Section tests_vcg.
(a_store (a_ret #l) (a_ret #2)))%E True (λ v, True).
Proof. iIntros "Hl". vcg_solver. Abort.
Lemma test4 (l k : loc) (e: expr) `{Closed [] e}:
( Φ v, k C v - (k C #12 - Φ v) - awp e True Φ) -
l C #1 -
k C #10 -
awp
(a_bin_op PlusOp (a_store (a_ret #l) (a_ret #2)) e;;;;
(a_store (a_ret #l) e))
True (λ v, True).
Proof.
iIntros "#He Hl Hk". vcg_solver.
iIntros "Hk". iApply ("He" with "Hk"); iIntros "Hk".
iExists [k;l], [Some (DenvItem ULvl 1 (dLitV (dLitInt 12)))].
iExists (dLitV (dLitInt 10)). iSplit; [done|]. iSplit; [done|].
iFrame "Hk"; iSplitR; first done.
simpl. iIntros "!> Hk Hl".
iApply ("He" with "Hk"); iIntros "Hk".
iExists [k;l], [Some (DenvItem ULvl 1 (dLitV (dLitInt 12)));
Some (DenvItem ULvl 1 (dLitV (dLitInt 2)))].
iExists (dLitV (dLitInt 12)). iSplit; [done|]. iSplit; [done|].
iFrame "Hl Hk". iSplitR; first done.
simpl. auto.
Qed.
Lemma test5 (k : loc) :
k C #10 -
awp
(a_bin_op PlusOp (a_store (a_alloc (a_ret #11)) (a_load (a_ret #k)))
(a_ret #2))
True (λ v, True).
Proof.
iIntros "Hk". vcg_solver.
iIntros "Hk".
iApply a_alloc_spec.
iApply awp_ret. iApply wp_value.
iIntros (l) "Hl".
iExists [k;l], [Some (DenvItem ULvl (1/2) (dLitV (dLitInt 10)));
Some (DenvItem ULvl 1 (dLitV (dLitInt 11)))],
(dLitV (dLitLoc (dLoc 1))).
iSplit; first done.
iSplit. iPureIntro. apply prefix_cons, prefix_nil.
iFrame "Hl Hk". iSplitR; first done.
simpl. auto.
Qed.
(*
Lemma test6 (l k : loc) (e1 e2 : expr) `{Closed [] e1, Closed [] e2}:
(∀ Φ, Φ #11 -∗ awp e1 True Φ) -∗
(∀ Φ, Φ #12 -∗ awp e2 True Φ) -∗
l ↦C #1 -∗
k ↦C #1 -∗
awp (a_bin_op PlusOp
(a_store (a_ret #l) (a_ret #2))
(a_store (a_ret #k) e1 ;;;; e2)) True (λ v, l ↦C[LLvl] #2 ∗ k ↦C #11).
Proof.
iIntros "He1 He2 Hl Hk". vcg_solver.
iIntros "Hk".
iApply "He1".
(* Now we need some way to mechanically continue *)
iApply (optimize_sound [] with "[-]");
[iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
(* This stuff should happen automagically *)
iExists _. iFrame "Hk".
iApply (optimize_sound [] with "[-]");
[iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
iIntros "?".
iApply "He2".
iApply (optimize_sound [] with "[-]");
[iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
iExists (dValUnknown (#14)). eauto with iFrame.
Qed.
*)
End tests_vcg.
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen.
From iris_c.c_translation Require Import monad translation proofmode notation.
From iris_c.lib Require Import locking_heap U.
Section tests_vcg.
Context `{amonadG Σ}.
Lemma test4 (l k : loc) (e: expr) `{Closed [] e}:
( Φ v, k C v - (k C #12 - Φ v) - awp e True Φ) -
l C #1 -
k C #10 -
awp
(l = 2 + e ;
l = e)
True (λ v, True).
Proof.
iIntros "#He Hl Hk". vcg_solver.
iIntros "Hk". iApply ("He" with "Hk"); iIntros "Hk".
iExists [k;l], [Some (DenvItem ULvl 1 (dLitV (dLitInt 12)))].
iExists (dLitV (dLitInt 10)). iSplit; [done|]. iSplit; [done|].
iFrame "Hk"; iSplitR; first done.
simpl. iIntros "!> Hk Hl".
iApply ("He" with "Hk"); iIntros "Hk".
iExists [k;l], [Some (DenvItem ULvl 1 (dLitV (dLitInt 12)));
Some (DenvItem ULvl 1 (dLitV (dLitInt 2)))].
iExists (dLitV (dLitInt 12)). iSplit; [done|]. iSplit; [done|].
iFrame "Hl Hk". iSplitR; first done.
simpl. auto.
Qed.
Lemma test5 (k : loc) :
k C #10 - awp (alloc 11 = ∗ᶜ♯k + 2) True (λ v, True).
Proof.
iIntros "Hk". vcg_solver.
iIntros "Hk".
iApply a_alloc_spec.
iApply awp_ret. iApply wp_value.
iIntros (l) "Hl".
iExists [k;l], [Some (DenvItem ULvl (1/2) (dLitV (dLitInt 10)));
Some (DenvItem ULvl 1 (dLitV (dLitInt 11)))],
(dLitV (dLitLoc (dLoc 1))).
iSplit; first done.
iSplit. iPureIntro. apply prefix_cons, prefix_nil.
iFrame "Hl Hk". iSplitR; first done.
simpl. auto.
Qed.
(*
Lemma test6 (l k : loc) (e1 e2 : expr) `{Closed [] e1, Closed [] e2}:
(∀ Φ, Φ #11 -∗ awp e1 True Φ) -∗
(∀ Φ, Φ #12 -∗ awp e2 True Φ) -∗
l ↦C #1 -∗
k ↦C #1 -∗
awp (a_bin_op PlusOp
(a_store (a_ret #l) (a_ret #2))
(a_store (a_ret #k) e1 ;;;; e2)) True (λ v, l ↦C[LLvl] #2 ∗ k ↦C #11).
Proof.
iIntros "He1 He2 Hl Hk". vcg_solver.
iIntros "Hk".
iApply "He1".
(* Now we need some way to mechanically continue *)
iApply (optimize_sound [] with "[-]");
[iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
(* This stuff should happen automagically *)
iExists _. iFrame "Hk".
iApply (optimize_sound [] with "[-]");
[iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
iIntros "?".
iApply "He2".
iApply (optimize_sound [] with "[-]");
[iApply wp_interp_sane_sound|by rewrite /denv_interp /=]; simpl.
iExists (dValUnknown (#14)). eauto with iFrame.
Qed.
*)
End tests_vcg.
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