Commit c3eda252 authored by Ike Mulder's avatar Ike Mulder
Browse files

Added more reloc examples.

parent ec9601fe
Pipeline #66157 passed with stage
in 8 minutes and 36 seconds
From reloc Require Import reloc examples.bit.
From diaframe.examples.external.reloc Require Import reloc_automation_base.
Section bit_refinement.
Context `{!relocG Σ}.
Lemma bit_refinement Δ : REL bit_bool << bit_nat : interp bitτ Δ.
Proof.
unfold bitτ; simpl.
iApply (refines_pack R).
progress repeat iApply refines_pair.
- iStepsS.
- unfold flip_nat. iStepsS.
- iStepsS.
Qed.
End bit_refinement.
\ No newline at end of file
From reloc Require Import reloc examples.cell.
From diaframe.examples.external.reloc Require Import reloc_automation_base.
Section cell_refinement.
Context `{!relocG Σ, !lockG Σ}.
Lemma cell2_cell1_refinement :
REL cell2 << cell1 : α, β, (α β) * (β α) * (β α ()).
Proof.
unfold cell1, cell2.
iApply refines_forall. iIntros "!#" (R).
iApply (refines_pack (cellR R)).
repeat iApply refines_pair.
- iSmash. exact nil.
- do 25 iStepS; do 6 iStepR; iSmash.
- do 40 iStepS; do 6 iStepR; iSmash.
Qed.
End cell_refinement.
\ No newline at end of file
From reloc.lib Require Import lock counter.
From diaframe.examples.external.reloc Require Import reloc_automation_base class_instances_reloc_logatom.
From diaframe.heap_lang Require Import stepping_tacs atomic_instances_heaplang.
From diaframe.heap_lang Require Import atomic_instances_heaplang.
Section fg_spec.
......
......@@ -9,7 +9,7 @@ From diaframe.examples.external.reloc Require Import class_instances_reloc.
From stdpp Require Import sets.
From reloc Require Import reloc lib.lock lib.counter examples.stack.CG_stack.
From reloc.logic.proofmode Require Export spec_tactics tactics.
From iris.heap_lang.lib Require Export ticket_lock.
Section main.
Context `{!relocG Σ}.
......@@ -93,9 +93,37 @@ Section main.
Global Opaque spec_ctx.
Global Instance ghost_mapsto_vals l v1 v2 :
HINT l ↦ₛ v1 [v1 = v2] [id]; l ↦ₛ v2 [v1 = v2] | 55.
Proof. iStepsS. Qed.
Global Instance mergable_consume_mapsto_own q1 q2 q l v1 v2 :
MergableConsume (l ↦ₛ{q1} v1)%I (λ p Pin Pout,
TCAnd (TCEq Pin (l ↦ₛ{q2} v2)) $
TCAnd (proofmode_classes.IsOp (A := frac.fracR) q q1 q2) $
(TCEq Pout (l ↦ₛ{q} v1 v1 = v2)))%I | 30. (* this does not include q ≤ 1! *)
Proof.
rewrite /MergableConsume => p Pin Pout [-> [+ ->]].
rewrite bi.intuitionistically_if_elim => Hq.
iStepS.
iDestruct (mapstoS_agree with "H1 H2") as "#->".
rewrite Hq. by iFrame.
Qed.
Global Instance mapsto_val_may_need_more (l : loc) (v1 v2 : val) (q1 q2 : Qp) mq q :
FracSub q2 q1 mq
TCEq mq (Some q)
HINT l ↦ₛ{q1} v1 [v'; v1 = v2 l ↦ₛ{q} v'] [id]; l ↦ₛ{q2} v2 [v1 = v2 v' = v1] | 55.
Proof.
rewrite /FracSub => <- -> v' /=.
iStepsS.
Qed.
Global Instance mapsto_val_have_enough (l : loc) (v1 v2 : val) (q1 q2 : Qp) mq :
FracSub q1 q2 mq
HINT l ↦ₛ{q1} v1 [- ; v1 = v2] [id]; l ↦ₛ{q2}v2 [v1 = v2 match mq with | Some q => l ↦ₛ{q} v1 | _ => True end] | 54.
Proof.
rewrite /= /FracSub => <-.
destruct mq; iStepsS.
iDestruct "H1" as "[H1 H1']".
iStepsS.
Qed.
Section lock_n_stack_specs.
(* spin lock specs as tp executions, so that automation can apply them *)
......@@ -168,6 +196,18 @@ Section main.
destruct vs as [|v vs]; iSmash.
Qed.
Obligation Tactic := program_verify.
Global Program Instance newlock_spec `{!lockG Σ} :
SPEC {{ True } } reloc.lib.lock.newlock #() {{ (l : loc), RET #l; R N, R ={}= γ, is_lock N γ #l R } }.
Global Program Instance acquire_spec `{!lockG Σ} (lk : val) R N :
SPEC γ, {{ is_lock N γ lk R } } reloc.lib.lock.acquire lk {{ RET #(); R lock.locked γ } }.
Global Program Instance release_spec `{!lockG Σ} (lk : val) R N :
SPEC γ, {{ is_lock N γ lk R R lock.locked γ } } reloc.lib.lock.release lk {{ RET #(); True } }.
Global Opaque is_lock reloc.lib.lock.newlock reloc.lib.lock.acquire reloc.lib.lock.release.
End lock_n_stack_specs.
End main.
......
From reloc Require Import reloc examples.symbol lib.lock lib.list.
From diaframe.examples.external.reloc Require Import reloc_automation_base.
From diaframe.lib Require Import own_hints.
From iris.algebra Require Import auth numbers.
Section symbol_refinement.
Context `{!relocG Σ, !msizeG Σ, !lock.lockG Σ}.
Definition table_inv' γ (size1 size2 tbl1 tbl2 : loc) : iProp Σ :=
( (n : nat) (ls : val), size1 {#1/2} #n size2 ↦ₛ{1/2} #n
own γ ( (MaxNat n))
tbl1 {#1/2} ls tbl2 ↦ₛ{1/2} ls
lrel_list lrel_int ls ls)%I.
Global Instance lrel_list_both_nil A :
HINT empty_hyp_first [emp] [id]; lrel_list A NILV NILV [emp].
Proof. iStepS. rewrite -lrel_list_nil. iStepsS. Qed.
Global Instance lrel_list_both_cons A v1 v2 ls1 ls2 :
HINT empty_hyp_last [ A v1 v2 lrel_list A ls1 ls2] [id];
lrel_list A (CONSV v1 ls1) (CONSV v2 ls2) [emp].
Proof. iStepS. rewrite right_id. iApply lrel_list_cons; iStepsS. Qed.
Hint Extern 4 (_ _)%nat => apply Nat.le_refl : solve_pure_add.
Lemma refinement1 :
REL symbol1 << symbol2 : () lrel_symbol.
Proof.
do 36 iStepS. unfold symbol2.
do 36 iStepR.
iAssert (|={}=> γ γl,
inv sizeN (table_inv' γ x x2 x0 x3)
is_lock (relocN.@"lock1") γl #x1 (lok_inv x x2 x0 x3 #x4) )%I
with "[H1 H2 H3 H4 H5 H6]"
as ">[%γ [%γl [#HI #HL]]]"; first by iStepsS.
iApply (refines_pack (tableR γ)).
repeat (iApply refines_pair).
- unfold eqKey; iStepsS.
- iStepsS. do 33 iStepR.
iRestore.
iStepsS. repeat iStepR.
iRestore.
iStepsS.
- iStepsS. repeat iStepR. rewrite bool_decide_true; last lia.
do 6 iStepR.
iRestore.
iStepsS. repeat iStepR.
iRestore.
repeat iApply refines_app; [iApply nth_int_typed |iStepsS..].
Qed.
Lemma refinement2 :
REL symbol2 << symbol1 : () lrel_symbol.
Proof.
do 36 iStepS. unfold symbol1.
do 36 iStepR.
iAssert (|={}=> γ γl,
inv sizeN (table_inv' γ x x2 x0 x3)
is_lock (relocN.@"lock1") γl #x1 (lok_inv x x2 x0 x3 #x4) )%I
with "[H1 H2 H3 H4 H5 H6]"
as ">[%γ [%γl [#HI #HL]]]"; first by iStepsS.
iApply (refines_pack (tableR γ)).
repeat (iApply refines_pair).
- unfold eqKey; iStepsS.
- iStepsS. do 33 iStepR.
iRestore.
iStepsS. repeat iStepR.
iRestore.
iStepsS.
- iStepsS. rewrite bool_decide_true; last lia.
iStepsS. iRestore.
iStepsS. do 6 iStepR. iRestore.
iStepsS. repeat iStepR. iRestore.
repeat iApply refines_app; [iApply nth_int_typed |iStepsS..].
Qed.
End cell_refinement.
\ No newline at end of file
Supports Markdown
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