From Staged Require Export HeapF LibFmap ExtraTactics.
From ShiftReset Require Export
Basics ShiftFree Propriety Reduction
Satisfies Biab Norm Ent GEnt
ReductionOld.
Implicit Types a v r :
val.
Section EnvFraming.
Lemma satisfies_env_frame :
forall s1 s2 h1 h2 R f k u,
~
Fmap.indom s1 k ->
satisfies (
Fmap.update s1 k u)
s2 h1 h2 R f <->
satisfies s1 (
Fmap.remove s2 k)
h1 h2 R f.
Proof.
introv Hfresh.
iff H.
{ remember (Fmap.update s1 k u) as s0.
induction H; subst s0.
{ applys s_req.
intros. specializes H1 H2 H3 H4. }
{ rewrites (>> remove_update Hfresh).
applys s_ens. heaps. }
{ applys s_bind.
specializes* IHsatisfies1.
admit.
}
{
destruct H as (b&?).
applys s_fex. exists b.
admit.
}
{
admit.
}
{
specializes IHsatisfies. constructor.
destruct (classic (k = xf)).
applys s_unk.
rewrite H1 in H. rewrite fmap_read_update in H.
admit.
admit.
admit.
}
Admitted.
Lemma ent_env_frame :
forall s1 k u f1 f2,
~
Fmap.indom s1 k ->
entails_under s1 f1 f2 ->
entails_under (
Fmap.update s1 k u)
f1 f2.
Proof.
unfold entails_under. introv Hfresh H H1.
rewrite~ satisfies_env_frame in H1.
specializes H H1.
rewrite~ <- satisfies_env_frame in H.
eassumption.
Qed.
End EnvFraming.
Reduction example
Example ex_rewrite_right:
entails (
ens_ \[
True]) (
ens_ \[
True];;
ens_ \[
True];;
ens_ \[
True]).
Proof.
rewrite <- norm_ens_ens_void.
Abort.
Example ex_rewrite_right1:
entails_under empty_env (
ens_ \[
True]) (
ens_ \[
True];;
ens_ \[
True];;
ens_ \[
True]).
Proof.
assert (forall H1 H2, entails_under empty_env (ens_ H1;; ens_ H2) (ens_ (H1 \* H2))) as ?. admit.
assert (forall H1 H2, entails_under empty_env (ens_ (H1 \* H2)) (ens_ H1;; ens_ H2)) as ?. admit.
rewrite <- H0.
rewrite <- H.
Abort.
Correspondence with the paper
Differences
-
Function pointer values vfptr enable arbitrary higher-order staged formulae. A defun staged formula (conceptually just an ens which binds a function value) and an output senv added to satisfies complete this, allowing shift bodies to return continuations.
-
The semantics guarantees that shft/Sh# continuations are shift-free by construction, by having a rs as their topmost form. This significantly simplifies the proofs of the reduction rules.
Section 4.3. Shift/Reset Reduction
The reduction rules are proved as lemmas.