Commit d1ead200 authored by Ralf Jung's avatar Ralf Jung
Browse files

finish ex1!

parent 73c911a1
Things in the "logical" side of the model that could be made better:
- The invariant for one (sub-)resource should only talk about that resource.
To fix CallMapInv: replace set T by `gmap loc tag` indicating which locations are protected.
To fix TagMapInv: kill the "value" part of LMAP.
To fix LocMapInv: make it a `gmap loc tag` that all just have a singleton stack with that loc.
Then we can also make PrivLoc handle fairly uniformly locations that are "privatized" by being protected or by being local.
- No need for (persistently) public call IDs. Still need to be able to pass
ownership of *all* tag protected by a call ID though, so
`gmap call_id (ex (gmap tag loc))` seems reasonable, or else `gmap call_id (prod frac (gmap tag (ex loc)))`.
- Can the separate private/local things be better integrated to the notion of a "private location" for the purposes of stating lemmas about them?
Or will that just always be `own_local loc tag \/ (exists cid h, own_call_id cid h /\ h !! loc = Some tag)`?
Things in the "model" side:
- Can we get rid of this EndCall-based stack tracking? Would be nice to treat EndCall more like InitCall, as part of the body of the fn, instead of special-casing it so much.
......@@ -2,12 +2,9 @@ From stbor.lang Require Export defs steps_foreach steps_list.
Set Default Proof Using "Type".
Definition tag_in t (stk: stack) :=
pm opro, pm Disabled mkItem pm (Tagged t) opro stk.
Definition tag_in_stack σ l t :=
stk, σ.(sst) !! l = Some stk tag_in t stk.
Definition tag_on_top σt l tag : Prop :=
tg <$> (σt.(sst) !! l) = head = Some (Tagged tag).
(* FIXME; should not require [Unique] *)
Definition tag_on_top (stks: stacks) l tag : Prop :=
prot, (stks !! l) = head = Some (mkItem Unique (Tagged tag) prot).
(** Active protector preserving *)
Definition active_preserving (cids: call_id_stack) (stk stk': stack) :=
......@@ -637,3 +634,19 @@ Proof.
have Ltk2: (k < i1)%nat. { eapply Nat.lt_le_trans; eauto. }
by rewrite (HL1 _ _ Ltk2 HL).
(** Tag-on-top *)
Lemma tag_on_top_write σ l tg stks :
tag_on_top σ.(sst) l tg
memory_written (sst σ) (scs σ) l (Tagged tg) 1 = Some stks
tag_on_top stks l tg.
rewrite /memory_written /tag_on_top /= shift_loc_0.
destruct (sst σ !! l) eqn:Hlk; last done. simpl.
destruct s as [|it st]; first done. simpl.
destruct it as [perm tg' prot']. intros [prot ?]; simplify_eq/=.
edestruct tag_unique_head_access as [n ->].
{ eexists. done. }
simpl. intros. simplify_eq/=. eexists. rewrite lookup_insert.
simpl. done.
From stbor.sim Require Import local invariant refl tactics simple program refl_step right_step left_step.
From stbor.sim Require Import local invariant refl tactics simple program refl_step right_step left_step viewshift.
Set Default Proof Using "Type".
......@@ -70,7 +70,7 @@ Proof.
(* Copy unique (right) *)
sim_apply_r sim_body_deref_r. simpl.
sim_apply_r sim_body_copy_unique_r; [try solve_sim..|].
{ subst σt'. admit. (* show that tag_op_top is preserved. *) }
{ subst σt'. eapply steps_retag.tag_on_top_write; done. }
{ rewrite lookup_insert. done. }
apply: sim_body_result=>_. simpl.
apply: sim_body_let_r. simpl. (* FIXME: figure out why [sim_apply_r] does the wrong thing here *)
......@@ -90,10 +90,14 @@ Proof.
sim_apply_l sim_body_deref_l. simpl.
sim_apply_l sim_body_copy_unique_l; [try solve_sim..|].
{ rewrite lookup_insert. done. }
(* Finishing up. *)
eapply sim_body_viewshift.
{ do 6 eapply viewshift_frame_r. eapply vs_call_empty_public. }
apply: sim_body_result=>Hval. simpl. split.
- eexists. split; first done. admit. (* end_call_sat *)
- eexists. split; first done. eapply res_end_call_sat; first done.
- constructor; simpl; auto.
(** Top-level theorem: Two programs that only differ in the
"ex1" function are related. *)
......@@ -727,6 +727,7 @@ Proof.
intros. simpl. by apply POST.
(** For writing to owned *or* public locations. *)
Lemma sim_body_write_related_values
fs ft (r: resUR) k0 h0 n l tg Ts Tt v σs σt Φ
(EQS: tsize Ts = tsize Tt)
......@@ -1039,12 +1040,13 @@ Lemma sim_body_write_owned
fs ft (r r' r'' rs: resUR) h n l tg T s σs σt Φ:
tsize T = 1%nat
r r' res_tag tg tkUnique h
is_Some (h !! l)
arel rs s s (* assuming to-write values are related *)
r' r'' rs
( α', memory_written σt.(sst) σt.(scs) l (Tagged tg) (tsize T) = Some α'
let σs' := mkState (write_mem l [s] σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc) in
let σt' := mkState (write_mem l [s] σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc) in
tag_on_top σt l tg
tag_on_top σt.(sst) l tg
Φ (r' res_tag tg tkUnique (<[l:=s]> h)) n (ValR []%S) σs' (ValR []%S) σt')
r {n,fs,ft}
(Place l (Tagged tg) T <- #[s], σs) (Place l (Tagged tg) T <- #[s], σt) : Φ.
......@@ -35,7 +35,7 @@ Admitted.
Lemma sim_body_copy_unique_r
fs ft (r r': resUR) (h: heaplet) n (l: loc) tg T (s: scalar) es σs σt Φ :
tsize T = 1%nat
tag_on_top σt l tg
tag_on_top σt.(sst) l tg
r r' res_tag tg tkUnique h
h !! l = Some s
(r {n,fs,ft} (es, σs) (#[s], σt) : Φ : Prop)
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