Ported tactics.v. TODO: handle AppRCtx in reshape_expr.

_CoqProject

 -Q . lrust
 lang.v
 substitution.v
+tactics.v

lang.v

@@ -6,7 +6,8 @@ From iris.prelude Require Import gmap.
 Open Scope Z_scope.
 
 (** Expressions and vals. *)
-Definition loc : Set := positive * Z.
+Definition block : Set := positive.
+Definition loc : Set := block * Z.
 
 Inductive base_lit : Set :=
 | LitUnit | LitLoc (l : loc) | LitInt (n : Z).
@@ -172,7 +173,7 @@ Program Fixpoint wsubst {X Y} (x : string) (es : expr [])
                 | right Hfy => wexpr (wsubst_rec_false_prf H Hfy) e
                 end
   | BinOp op e1 e2 => BinOp op (wsubst x es H e1) (wsubst x es H e2)
-  | App e1 e2 => App (wsubst x es H e1) (List.map (wsubst x es H) e2)
+  | App e el => App (wsubst x es H e) (List.map (wsubst x es H) el)
   | Read o e => Read o (wsubst x es H e)
   | Write o e1 e2 => Write o (wsubst x es H e1) (wsubst x es H e2)
   | CAS e0 e1 e2 => CAS (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
@@ -207,14 +208,14 @@ Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
   | _, _, _ => None
   end.
 
-Fixpoint init_mem (blk:positive) (i:Z) (init:list val) (σ:state) : state :=
+Fixpoint init_mem (blk:block) (i:Z) (init:list val) (σ:state) : state :=
   match init with
   | [] => σ
   | inith :: initq =>
     init_mem blk (Z.succ i) initq (<[(blk, i):=(ReadingSt 0, inith)]>σ)
   end.
 
-Fixpoint free_mem (blk:positive) (n:nat) (i0:Z) (σ:state) : state :=
+Fixpoint free_mem (blk:block) (n:nat) (i0:Z) (σ:state) : state :=
   match n with
   | O => σ
   | S n => free_mem blk n i0 (delete (blk, i0+n) σ)
@@ -449,6 +450,29 @@ Proof.
   destruct (list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2); auto. congruence.
 Qed.
 
+Definition fresh_block (σ : state) : block :=
+  let blocklst := (elements (dom _ σ : gset loc)).*1 in
+  let blockset : gset block := foldr (fun b s => {[b]} ∪ s)%C ∅ blocklst in
+  fresh blockset.
+
+Lemma alloc_fresh n σ :
+  let blk := fresh_block σ in
+  let init := repeat (LitV $ LitInt 0) (Z.to_nat n) in
+  0 < n →
+  head_step (Alloc $ Lit $ LitInt n) σ (Lit $ LitLoc (blk, 0))
+            (init_mem blk 0 init σ)
+            None.
+Proof.
+  intros blk init Hn. apply AllocS, repeat_length. auto.
+  clear init n Hn. unfold blk, fresh_block. intro i.
+  match goal with
+  | |- appcontext [foldr ?f ?e] =>
+    assert (FOLD:∀ l x, (x, i) ∈ l → x ∈ (foldr f e (l.*1)))
+  end.
+  { induction l; simpl; inversion 1; subst; set_solver. }
+  rewrite -not_elem_of_dom -elem_of_elements=>/FOLD. apply is_fresh.
+Qed.
+
 (** Equality and other typeclass stuff *)
 Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
 Proof. solve_decision. Defined.

tactics.v

+From lrust Require Export substitution.
+From iris.prelude Require Import fin_maps.
+
+(** The tactic [inv_head_step] performs inversion on hypotheses of the
+shape [head_step]. The tactic will discharge head-reductions starting
+from values, and simplifies hypothesis related to conversions from and
+to values, and finite map operations. This tactic is slightly ad-hoc
+and tuned for proving our lifting lemmas. *)
+Ltac inv_head_step :=
+  repeat match goal with
+  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
+  | H : to_val _ = Some _ |- _ => apply of_to_val in H
+  | H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
+  | H : head_step ?e _ _ _ _ |- _ =>
+     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
+     and can thus better be avoided. *)
+     inversion H; subst; clear H
+  end.
+
+(** The tactic [reshape_expr e tac] decomposes the expression [e] into an
+evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
+for each possible decomposition until [tac] succeeds. *)
+Ltac reshape_val e tac :=
+  let rec go e :=
+  match e with
+  | of_val ?v => v
+  | wexpr' ?e => reshape_val e tac
+  | Lit ?l => constr:(LitV l)
+  | Rec ?f ?xl ?e => constr:(RecV f xl e)
+  end in let v := go e in first [tac v | fail 2].
+
+Ltac reshape_expr e tac :=
+  let rec go K e :=
+  match e with
+  | _ => tac (reverse K) e
+  | BinOp ?op ?e1 ?e2 =>
+     reshape_val e1 ltac:(fun v1 => go (BinOpRCtx op v1 :: K) e2)
+  | BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
+  (* TODO *)
+  (* | App ?e ?el => *)
+  (*   reshape_val e ltac:(fun v => go (AppRCtx v :: K) el) *)
+  | App ?e ?el => go (AppLCtx el :: K) e
+  | Read ?o ?e => go (ReadCtx o :: K) e
+  | Write ?o ?e1 ?e2 =>
+    reshape_val e1 ltac:(fun v1 => go (WriteRCtx o v1 :: K) e2)
+  | Write ?o ?e1 ?e2 => go (WriteLCtx o e2 :: K) e1
+  | CAS ?e0 ?e1 ?e2 => reshape_val e0 ltac:(fun v0 => first
+     [ reshape_val e1 ltac:(fun v1 => go (CasRCtx v0 v1 :: K) e2)
+     | go (CasMCtx v0 e2 :: K) e1 ])
+  | CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
+  | Alloc ?e => go (AllocCtx :: K) e
+  | Free ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (FreeRCtx v1 :: K) e2)
+  | Free ?e1 ?e2 => go (FreeLCtx e2 :: K) e1
+  | Case ?e ?el => go (CaseCtx el :: K) e
+  end in go (@nil ectx_item) e.
+
+(** The tactic [do_head_step tac] solves goals of the shape [head_reducible] and
+[head_step] by performing a reduction step and uses [tac] to solve any
+side-conditions generated by individual steps. *)
+Tactic Notation "do_head_step" tactic3(tac) :=
+  try match goal with |- head_reducible _ _ => eexists _, _, _ end;
+  simpl;
+  match goal with
+  | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
+     first [apply alloc_fresh|econstructor];
+       (* solve [to_val] side-conditions *)
+       first [rewrite ?to_of_val; reflexivity|simpl_subst; tac; fast_done]
+  end.