left_step.v 1.25 KB
Newer Older
Hai Dang's avatar
Hai Dang committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
From iris.algebra Require Import local_updates.

From stbor.lang Require Import steps_progress steps_inversion steps_retag.
From stbor.sim Require Export instance.

Set Default Proof Using "Type".

Lemma sim_body_copy_left_1
  fs ft (r: resUR) k (h: heapletR) n l t et σs σt Φ
  (UNIQUE: r.1 !! t  Some (k, h))
  (InD: l  dom (gset loc) h) :
  ( s, σs.(shp) !! l = Some s  r {n,fs,ft} (#[s%S], σs)  (et, σt) : Φ : Prop) 
  r {n,fs,ft} (Copy (Place l (Tagged t) int), σs)  (et, σt) : Φ.
Proof.
  intros COND. pfold. intros NT r_f WSAT.
  edestruct NT as [[]|[es1 [σs1 STEP1]]]; [constructor 1|done|].
  destruct (tstep_copy_inv _ _ _ _ _ _ _ STEP1) as (vs & α' & ? & Eqvs & READ & ?).
  subst es1 σs1. rewrite /= read_mem_equation_1 /= in Eqvs.
  destruct (σs.(shp) !! l) as [s|] eqn:Eqs; [|done]. simpl in Eqvs. simplify_eq.
  specialize (COND _ eq_refl).

  (* we need to invoke WSAT to know that α' = σs.(sst) *)
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).

  (* once we know that the state did not change, we can use COND. *)
  have NT2 := never_stuck_tstep_once _ _ _ _ _ STEP1 NT.
  punfold COND.

  split.
  { (* this comes from COND *) admit. }
  { (* follows COND *) admit. }
  { (* follows COND *) admit. }
Abort.