Gible

These instructions are used for RTLBlock and RTLPar, so that they have consistent instructions, which greatly simplifies the proofs, as they will by default have the same instruction syntax and semantics. The only changes are therefore at the top-level of the instructions.

Instruction Definition

First, we define the instructions that can be placed into a basic block, meaning they won’t branch. The main changes to how instructions are defined in RTL, is that these instructions don’t have a next node, as they will be in a basic block, and they also have an optional predicate (pred_op).

Control-Flow Instruction Definition

These are the instructions that count as control-flow, and will be placed at the end of the basic blocks.

Variant cf_instr : Type :=
| RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr
| RBtailcall : signature -> reg + ident -> list reg -> cf_instr
| RBbuiltin : external_function -> list (builtin_arg reg) ->
              builtin_res reg -> node -> cf_instr
| RBcond : condition -> list reg -> node -> node -> cf_instr
| RBjumptable : reg -> list node -> cf_instr
| RBreturn : option reg -> cf_instr
| RBgoto : node -> cf_instr.

Variant instr : Type :=
| RBnop : instr
| RBop :
  option pred_op -> operation -> list reg -> reg -> instr
| RBload :
  option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
| RBstore :
  option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
| RBsetpred :
  option pred_op -> condition -> list reg -> predicate -> instr
| RBexit : option pred_op -> cf_instr -> instr.

Helper Functions

Definition successors_instr (i : cf_instr) : list node :=
  match i with
  | RBcall sig ros args res s => s :: nil
  | RBtailcall sig ros args => nil
  | RBbuiltin ef args res s => s :: nil
  | RBcond cond args ifso ifnot => ifso :: ifnot :: nil
  | RBjumptable arg tbl => tbl
  | RBreturn optarg => nil
  | RBgoto n => n :: nil
  end.

Definition max_reg_cfi (m : positive) (i : cf_instr) :=
  match i with
  | RBcall sig (inl r) args res s =>
      fold_left Pos.max args (Pos.max r (Pos.max res m))
  | RBcall sig (inr id) args res s =>
      fold_left Pos.max args (Pos.max res m)
  | RBtailcall sig (inl r) args =>
      fold_left Pos.max args (Pos.max r m)
  | RBtailcall sig (inr id) args =>
      fold_left Pos.max args m
  | RBbuiltin ef args res s =>
      fold_left Pos.max (params_of_builtin_args args)
                (fold_left Pos.max (params_of_builtin_res res) m)
  | RBcond cond args ifso ifnot => fold_left Pos.max args m
  | RBjumptable arg tbl => Pos.max arg m
  | RBreturn None => m
  | RBreturn (Some arg) => Pos.max arg m
  | RBgoto n => m
  end.

Definition max_reg_instr (m: positive) (i: instr) :=
  match i with
  | RBnop => m
  | RBop p op args res =>
      fold_left Pos.max args (Pos.max res m)
  | RBload p chunk addr args dst =>
      fold_left Pos.max args (Pos.max dst m)
  | RBstore p chunk addr args src =>
      fold_left Pos.max args (Pos.max src m)
  | RBsetpred p' c args p =>
      fold_left Pos.max args m
  | RBexit _ c => max_reg_cfi m c
  end.

Definition max_pred_instr (m: positive) (i: instr) :=
  match i with
  | RBop (Some p) op args res => Pos.max m (max_predicate p)
  | RBload (Some p) chunk addr args dst => Pos.max m (max_predicate p)
  | RBstore (Some p) chunk addr args src => Pos.max m (max_predicate p)
  | RBsetpred (Some p') c args p => Pos.max m (Pos.max p (max_predicate p'))
  | RBsetpred None c args p => Pos.max m p
  | RBexit (Some p) c => Pos.max m (max_predicate p)
  | _ => m
  end.

Definition regset := Regmap.t val.
Definition predset := PMap.t bool.

Definition eval_predf (pr: predset) (p: pred_op) :=
  sat_predicate p (fun x => pr !! x).

Lemma sat_pred_agree0 :
  forall a b p,
    (forall x, a x = b x) ->
    sat_predicate p a = sat_predicate p b.
forall (a b : Sat.var -> bool) (p : Predicate.pred_op),
(forall x : Sat.var, a x = b x) ->
sat_predicate p a = sat_predicate p b
Proof.
forall (a b : Sat.var -> bool) (p : Predicate.pred_op),
(forall x : Sat.var, a x = b x) ->
sat_predicate p a = sat_predicate p b
  induction p; auto; intros.
a, b: Sat.var -> bool
p: (bool * Predicate.predicate)%type
H: forall x : Sat.var, a x = b x
sat_predicate (Plit p) a = sat_predicate (Plit p) b
a, b: Sat.var -> bool
p1, p2: Predicate.pred_op
IHp1: (forall x : Sat.var, a x = b x) ->
sat_predicate p1 a = sat_predicate p1 b
IHp2: (forall x : Sat.var, a x = b x) ->
sat_predicate p2 a = sat_predicate p2 b
H: forall x : Sat.var, a x = b x
sat_predicate (Pand p1 p2) a =
sat_predicate (Pand p1 p2) b
a, b: Sat.var -> bool
p1, p2: Predicate.pred_op
IHp1: (forall x : Sat.var, a x = b x) ->
sat_predicate p1 a = sat_predicate p1 b
IHp2: (forall x : Sat.var, a x = b x) ->
sat_predicate p2 a = sat_predicate p2 b
H: forall x : Sat.var, a x = b x
sat_predicate (Por p1 p2) a =
sat_predicate (Por p1 p2) b
  -
a, b: Sat.var -> bool
p: (bool * Predicate.predicate)%type
H: forall x : Sat.var, a x = b x
sat_predicate (Plit p) a = sat_predicate (Plit p) b destruct p.
a, b: Sat.var -> bool
b0: bool
p: Predicate.predicate
H: forall x : Sat.var, a x = b x
sat_predicate (Plit (b0, p)) a =
sat_predicate (Plit (b0, p)) b cbn.
a, b: Sat.var -> bool
b0: bool
p: Predicate.predicate
H: forall x : Sat.var, a x = b x
(if b0 then a p else negb (a p)) =
(if b0 then b p else negb (b p))
    now rewrite H.
  -
a, b: Sat.var -> bool
p1, p2: Predicate.pred_op
IHp1: (forall x : Sat.var, a x = b x) ->
sat_predicate p1 a = sat_predicate p1 b
IHp2: (forall x : Sat.var, a x = b x) ->
sat_predicate p2 a = sat_predicate p2 b
H: forall x : Sat.var, a x = b x
sat_predicate (Pand p1 p2) a =
sat_predicate (Pand p1 p2) b specialize (IHp1 H).
a, b: Sat.var -> bool
p1, p2: Predicate.pred_op
IHp1: sat_predicate p1 a = sat_predicate p1 b
IHp2: (forall x : Sat.var, a x = b x) ->
sat_predicate p2 a = sat_predicate p2 b
H: forall x : Sat.var, a x = b x
sat_predicate (Pand p1 p2) a =
sat_predicate (Pand p1 p2) b specialize (IHp2 H).
a, b: Sat.var -> bool
p1, p2: Predicate.pred_op
IHp1: sat_predicate p1 a = sat_predicate p1 b
IHp2: sat_predicate p2 a = sat_predicate p2 b
H: forall x : Sat.var, a x = b x
sat_predicate (Pand p1 p2) a =
sat_predicate (Pand p1 p2) b
    cbn.
a, b: Sat.var -> bool
p1, p2: Predicate.pred_op
IHp1: sat_predicate p1 a = sat_predicate p1 b
IHp2: sat_predicate p2 a = sat_predicate p2 b
H: forall x : Sat.var, a x = b x
sat_predicate p1 a && sat_predicate p2 a =
sat_predicate p1 b && sat_predicate p2 b rewrite IHp1.
a, b: Sat.var -> bool
p1, p2: Predicate.pred_op
IHp1: sat_predicate p1 a = sat_predicate p1 b
IHp2: sat_predicate p2 a = sat_predicate p2 b
H: forall x : Sat.var, a x = b x
sat_predicate p1 b && sat_predicate p2 a =
sat_predicate p1 b && sat_predicate p2 b rewrite IHp2.
a, b: Sat.var -> bool
p1, p2: Predicate.pred_op
IHp1: sat_predicate p1 a = sat_predicate p1 b
IHp2: sat_predicate p2 a = sat_predicate p2 b
H: forall x : Sat.var, a x = b x
sat_predicate p1 b && sat_predicate p2 b =
sat_predicate p1 b && sat_predicate p2 b auto.
  -
a, b: Sat.var -> bool
p1, p2: Predicate.pred_op
IHp1: (forall x : Sat.var, a x = b x) ->
sat_predicate p1 a = sat_predicate p1 b
IHp2: (forall x : Sat.var, a x = b x) ->
sat_predicate p2 a = sat_predicate p2 b
H: forall x : Sat.var, a x = b x
sat_predicate (Por p1 p2) a =
sat_predicate (Por p1 p2) b specialize (IHp1 H).
a, b: Sat.var -> bool
p1, p2: Predicate.pred_op
IHp1: sat_predicate p1 a = sat_predicate p1 b
IHp2: (forall x : Sat.var, a x = b x) ->
sat_predicate p2 a = sat_predicate p2 b
H: forall x : Sat.var, a x = b x
sat_predicate (Por p1 p2) a =
sat_predicate (Por p1 p2) b specialize (IHp2 H).
a, b: Sat.var -> bool
p1, p2: Predicate.pred_op
IHp1: sat_predicate p1 a = sat_predicate p1 b
IHp2: sat_predicate p2 a = sat_predicate p2 b
H: forall x : Sat.var, a x = b x
sat_predicate (Por p1 p2) a =
sat_predicate (Por p1 p2) b
    cbn.
a, b: Sat.var -> bool
p1, p2: Predicate.pred_op
IHp1: sat_predicate p1 a = sat_predicate p1 b
IHp2: sat_predicate p2 a = sat_predicate p2 b
H: forall x : Sat.var, a x = b x
sat_predicate p1 a || sat_predicate p2 a =
sat_predicate p1 b || sat_predicate p2 b rewrite IHp1.
a, b: Sat.var -> bool
p1, p2: Predicate.pred_op
IHp1: sat_predicate p1 a = sat_predicate p1 b
IHp2: sat_predicate p2 a = sat_predicate p2 b
H: forall x : Sat.var, a x = b x
sat_predicate p1 b || sat_predicate p2 a =
sat_predicate p1 b || sat_predicate p2 b rewrite IHp2.
a, b: Sat.var -> bool
p1, p2: Predicate.pred_op
IHp1: sat_predicate p1 a = sat_predicate p1 b
IHp2: sat_predicate p2 a = sat_predicate p2 b
H: forall x : Sat.var, a x = b x
sat_predicate p1 b || sat_predicate p2 b =
sat_predicate p1 b || sat_predicate p2 b auto.
Qed.

#[global]
 Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf.
Proper (eq ==> equiv ==> eq) eval_predf
Proof.
Proper (eq ==> equiv ==> eq) eval_predf
  unfold Proper.
(eq ==> equiv ==> eq)%signature eval_predf eval_predf simplify.
(eq ==> sat_equiv ==> eq)%signature eval_predf
  eval_predf unfold "==>".
forall x y : predset,
x = y ->
forall x0 y0 : pred_op,
sat_equiv x0 y0 -> eval_predf x x0 = eval_predf y y0
  intros.
x, y: predset
H: x = y
x0, y0: pred_op
H0: sat_equiv x0 y0
eval_predf x x0 = eval_predf y y0
  unfold sat_equiv in *.
x, y: predset
H: x = y
x0, y0: pred_op
H0: forall c : Sat.asgn,
sat_predicate x0 c = sat_predicate y0 c
eval_predf x x0 = eval_predf y y0 intros.
x, y: predset
H: x = y
x0, y0: pred_op
H0: forall c : Sat.asgn,
sat_predicate x0 c = sat_predicate y0 c
eval_predf x x0 = eval_predf y y0 unfold eval_predf.
x, y: predset
H: x = y
x0, y0: pred_op
H0: forall c : Sat.asgn,
sat_predicate x0 c = sat_predicate y0 c
sat_predicate x0 (fun x0 : Sat.var => x !! x0) =
sat_predicate y0 (fun x : Sat.var => y !! x) subst.
y: predset
x0, y0: pred_op
H0: forall c : Sat.asgn,
sat_predicate x0 c = sat_predicate y0 c
sat_predicate x0 (fun x : Sat.var => y !! x) =
sat_predicate y0 (fun x : Sat.var => y !! x) apply H0.
Qed.

#[local] Open Scope pred_op.

Lemma eval_predf_Pand :
  forall ps p p',
    eval_predf ps (p ∧ p') = eval_predf ps p && eval_predf ps p'.
forall (ps : predset) (p p' : Predicate.pred_op),
eval_predf ps (p ∧ p') =
eval_predf ps p && eval_predf ps p'
Proof.
forall (ps : predset) (p p' : Predicate.pred_op),
eval_predf ps (p ∧ p') =
eval_predf ps p && eval_predf ps p' unfold eval_predf; split; simplify; auto with bool. Qed.

Lemma eval_predf_Por :
  forall ps p p',
    eval_predf ps (p ∨ p') = eval_predf ps p || eval_predf ps p'.
forall (ps : predset) (p p' : Predicate.pred_op),
eval_predf ps (p ∨ p') =
eval_predf ps p || eval_predf ps p'
Proof.
forall (ps : predset) (p p' : Predicate.pred_op),
eval_predf ps (p ∨ p') =
eval_predf ps p || eval_predf ps p' unfold eval_predf; split; simplify; auto with bool. Qed.

Lemma eval_predf_simplify :
  forall ps p,
    eval_predf ps (simplify p) = eval_predf ps p.
forall (ps : predset) (p : Predicate.pred_op),
eval_predf ps (simplify p) = eval_predf ps p
Proof.
forall (ps : predset) (p : Predicate.pred_op),
eval_predf ps (simplify p) = eval_predf ps p unfold eval_predf; intros.
ps: predset
p: Predicate.pred_op
sat_predicate (simplify p)
  (fun x : Sat.var => ps !! x) =
sat_predicate p (fun x : Sat.var => ps !! x) now rewrite simplify_correct. Qed.

Lemma eval_predf_deep_simplify :
  forall peq ps p,
    eval_predf ps (deep_simplify peq p) = eval_predf ps p.
forall
  (peq : forall a b : predicate, {a = b} + {a <> b})
  (ps : predset) (p : Predicate.pred_op),
eval_predf ps (deep_simplify peq p) = eval_predf ps p
Proof.
forall
  (peq : forall a b : predicate, {a = b} + {a <> b})
  (ps : predset) (p : Predicate.pred_op),
eval_predf ps (deep_simplify peq p) = eval_predf ps p unfold eval_predf; intros.
peq: forall a b : predicate, {a = b} + {a <> b}
ps: predset
p: Predicate.pred_op
sat_predicate (deep_simplify peq p)
  (fun x : Sat.var => ps !! x) =
sat_predicate p (fun x : Sat.var => ps !! x) now rewrite deep_simplify_correct. Qed.

Lemma eval_predf_pr_equiv :
  forall p ps ps',
    (forall x, ps !! x = ps' !! x) ->
    eval_predf ps p = eval_predf ps' p.
forall (p : pred_op) (ps ps' : PMap.t bool),
(forall x : positive, ps !! x = ps' !! x) ->
eval_predf ps p = eval_predf ps' p
Proof.
forall (p : pred_op) (ps ps' : PMap.t bool),
(forall x : positive, ps !! x = ps' !! x) ->
eval_predf ps p = eval_predf ps' p
  induction p; simplify; auto;
    try (unfold eval_predf; simplify;
         repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto);
    [repeat rewrite eval_predf_Pand|repeat rewrite eval_predf_Por];
    erewrite IHp1; try eassumption; erewrite IHp2; eauto.
Qed.

Lemma eval_predf_not_PredIn :
  forall ps p b op,
    ~ PredIn p op ->
    eval_predf (ps # p <- b) op = eval_predf ps op.
forall (ps : Regmap.t bool) (p : Predicate.predicate)
  (b : bool) (op : Predicate.pred_op),
~ PredIn p op ->
eval_predf ps # p <- b op = eval_predf ps op
Proof.
forall (ps : Regmap.t bool) (p : Predicate.predicate)
  (b : bool) (op : Predicate.pred_op),
~ PredIn p op ->
eval_predf ps # p <- b op = eval_predf ps op
  induction op; auto.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
p0: (bool * Predicate.predicate)%type
~ PredIn p (Plit p0) ->
eval_predf ps # p <- b (Plit p0) =
eval_predf ps (Plit p0)
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
eval_predf ps # p <- b op1 = eval_predf ps op1
IHop2: ~ PredIn p op2 ->
eval_predf ps # p <- b op2 = eval_predf ps op2
~ PredIn p (op1 ∧ op2) ->
eval_predf ps # p <- b (op1 ∧ op2) =
eval_predf ps (op1 ∧ op2)
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
eval_predf ps # p <- b op1 = eval_predf ps op1
IHop2: ~ PredIn p op2 ->
eval_predf ps # p <- b op2 = eval_predf ps op2
~ PredIn p (op1 ∨ op2) ->
eval_predf ps # p <- b (op1 ∨ op2) =
eval_predf ps (op1 ∨ op2)
  -
ps: Regmap.t bool
p: Predicate.predicate
b: bool
p0: (bool * Predicate.predicate)%type
~ PredIn p (Plit p0) ->
eval_predf ps # p <- b (Plit p0) =
eval_predf ps (Plit p0) intros.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
p0: (bool * Predicate.predicate)%type
H: ~ PredIn p (Plit p0)
eval_predf ps # p <- b (Plit p0) =
eval_predf ps (Plit p0) destruct p0.
ps: Regmap.t bool
p: Predicate.predicate
b, b0: bool
p0: Predicate.predicate
H: ~ PredIn p (Plit (b0, p0))
eval_predf ps # p <- b (Plit (b0, p0)) =
eval_predf ps (Plit (b0, p0)) cbn.
ps: Regmap.t bool
p: Predicate.predicate
b, b0: bool
p0: Predicate.predicate
H: ~ PredIn p (Plit (b0, p0))
(if b0
 then (ps # p <- b) !! p0
 else negb (ps # p <- b) !! p0) =
(if b0 then ps !! p0 else negb ps !! p0)
    destruct (peq p p0); subst.
ps: Regmap.t bool
b, b0: bool
p0: Predicate.predicate
H: ~ PredIn p0 (Plit (b0, p0))
(if b0
 then (ps # p0 <- b) !! p0
 else negb (ps # p0 <- b) !! p0) =
(if b0 then ps !! p0 else negb ps !! p0)
ps: Regmap.t bool
p: Predicate.predicate
b, b0: bool
p0: Predicate.predicate
H: ~ PredIn p (Plit (b0, p0))
n: p <> p0
(if b0
 then (ps # p <- b) !! p0
 else negb (ps # p <- b) !! p0) =
(if b0 then ps !! p0 else negb ps !! p0)
      {
ps: Regmap.t bool
b, b0: bool
p0: Predicate.predicate
H: ~ PredIn p0 (Plit (b0, p0))
(if b0
 then (ps # p0 <- b) !! p0
 else negb (ps # p0 <- b) !! p0) =
(if b0 then ps !! p0 else negb ps !! p0) exfalso; apply H; constructor. }
ps: Regmap.t bool
p: Predicate.predicate
b, b0: bool
p0: Predicate.predicate
H: ~ PredIn p (Plit (b0, p0))
n: p <> p0
(if b0
 then (ps # p <- b) !! p0
 else negb (ps # p <- b) !! p0) =
(if b0 then ps !! p0 else negb ps !! p0)
    rewrite Regmap.gso; auto.
  -
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
eval_predf ps # p <- b op1 = eval_predf ps op1
IHop2: ~ PredIn p op2 ->
eval_predf ps # p <- b op2 = eval_predf ps op2
~ PredIn p (op1 ∧ op2) ->
eval_predf ps # p <- b (op1 ∧ op2) =
eval_predf ps (op1 ∧ op2) intros.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
eval_predf ps # p <- b op1 = eval_predf ps op1
IHop2: ~ PredIn p op2 ->
eval_predf ps # p <- b op2 = eval_predf ps op2
H: ~ PredIn p (op1 ∧ op2)
eval_predf ps # p <- b (op1 ∧ op2) =
eval_predf ps (op1 ∧ op2) cbn.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
eval_predf ps # p <- b op1 = eval_predf ps op1
IHop2: ~ PredIn p op2 ->
eval_predf ps # p <- b op2 = eval_predf ps op2
H: ~ PredIn p (op1 ∧ op2)
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) &&
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x) &&
sat_predicate op2 (fun x : Sat.var => ps !! x) unfold eval_predf in *.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∧ op2)
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) &&
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x) &&
sat_predicate op2 (fun x : Sat.var => ps !! x) rewrite IHop1.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∧ op2)
sat_predicate op1 (fun x : Sat.var => ps !! x) &&
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x) &&
sat_predicate op2 (fun x : Sat.var => ps !! x)
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∧ op2)
~ PredIn p op1
    rewrite IHop2.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∧ op2)
sat_predicate op1 (fun x : Sat.var => ps !! x) &&
sat_predicate op2 (fun x : Sat.var => ps !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x) &&
sat_predicate op2 (fun x : Sat.var => ps !! x)
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∧ op2)
~ PredIn p op2
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∧ op2)
~ PredIn p op1 auto.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∧ op2)
~ PredIn p op2
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∧ op2)
~ PredIn p op1
    unfold not; intros; apply H; constructor; tauto.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∧ op2)
~ PredIn p op1
    unfold not; intros; apply H; constructor; tauto.
  -
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
eval_predf ps # p <- b op1 = eval_predf ps op1
IHop2: ~ PredIn p op2 ->
eval_predf ps # p <- b op2 = eval_predf ps op2
~ PredIn p (op1 ∨ op2) ->
eval_predf ps # p <- b (op1 ∨ op2) =
eval_predf ps (op1 ∨ op2) intros.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
eval_predf ps # p <- b op1 = eval_predf ps op1
IHop2: ~ PredIn p op2 ->
eval_predf ps # p <- b op2 = eval_predf ps op2
H: ~ PredIn p (op1 ∨ op2)
eval_predf ps # p <- b (op1 ∨ op2) =
eval_predf ps (op1 ∨ op2) cbn.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
eval_predf ps # p <- b op1 = eval_predf ps op1
IHop2: ~ PredIn p op2 ->
eval_predf ps # p <- b op2 = eval_predf ps op2
H: ~ PredIn p (op1 ∨ op2)
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x)
|| sat_predicate op2
     (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
|| sat_predicate op2 (fun x : Sat.var => ps !! x) unfold eval_predf in *.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∨ op2)
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x)
|| sat_predicate op2
     (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
|| sat_predicate op2 (fun x : Sat.var => ps !! x) rewrite IHop1.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∨ op2)
sat_predicate op1 (fun x : Sat.var => ps !! x)
|| sat_predicate op2
     (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
|| sat_predicate op2 (fun x : Sat.var => ps !! x)
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∨ op2)
~ PredIn p op1
    rewrite IHop2.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∨ op2)
sat_predicate op1 (fun x : Sat.var => ps !! x)
|| sat_predicate op2 (fun x : Sat.var => ps !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
|| sat_predicate op2 (fun x : Sat.var => ps !! x)
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∨ op2)
~ PredIn p op2
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∨ op2)
~ PredIn p op1 auto.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∨ op2)
~ PredIn p op2
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∨ op2)
~ PredIn p op1
    unfold not; intros; apply H; constructor; tauto.
ps: Regmap.t bool
p: Predicate.predicate
b: bool
op1, op2: Predicate.pred_op
IHop1: ~ PredIn p op1 ->
sat_predicate op1
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op1 (fun x : Sat.var => ps !! x)
IHop2: ~ PredIn p op2 ->
sat_predicate op2
  (fun x : Sat.var => (ps # p <- b) !! x) =
sat_predicate op2 (fun x : Sat.var => ps !! x)
H: ~ PredIn p (op1 ∨ op2)
~ PredIn p op1
    unfold not; intros; apply H; constructor; tauto.
Qed.

Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
  match rl, vl with
  | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs)
  | _, _ => Regmap.init Vundef
  end.

Instruction State

Definition of the instruction state, which contains the following:

is_rs:

This is the current state of the registers.

is_ps:

This is the current state of the predicate registers, which is in a separate namespace and area compared to the standard registers in [is_rs].

is_mem:

The current state of the memory.

Record instr_state := mk_instr_state {
                         is_rs: regset;
                         is_ps: predset;
                         is_mem: mem;
                       }.

Variant istate : Type :=
  | Iexec : instr_state -> istate
  | Iterm : instr_state -> cf_instr -> istate.

Inductive eval_pred:
  option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
| eval_pred_true:
  forall i i' p,
    eval_predf (is_ps i) p = true ->
    eval_pred (Some p) i i' i'
| eval_pred_false:
  forall i i' p,
    eval_predf (is_ps i) p = false ->
    eval_pred (Some p) i i' i
| eval_pred_none:
  forall i i', eval_pred None i i' i'.

Definition truthyb (ps: predset) (p: option pred_op) :=
  match p with
  | None => true
  | Some p' => eval_predf ps p'
  end.

Variant truthy (ps: predset): option pred_op -> Prop :=
  | truthy_None: truthy ps None
  | truthy_Some: forall p, eval_predf ps p = true -> truthy ps (Some p).

Variant falsy (ps: predset): option pred_op -> Prop :=
  | falsy_Some: forall p, eval_predf ps p = false -> falsy ps (Some p).

Variant instr_falsy (ps: predset): instr -> Prop :=
  | RBop_falsy :
    forall p op args res,
      eval_predf ps p = false ->
      instr_falsy ps (RBop (Some p) op args res)
  | RBload_falsy:
    forall p chunk addr args dst,
      eval_predf ps p = false ->
      instr_falsy ps (RBload (Some p) chunk addr args dst)
  | RBstore_falsy:
    forall p chunk addr args src,
      eval_predf ps p = false ->
      instr_falsy ps (RBstore (Some p) chunk addr args src)
  | RBsetpred_falsy:
    forall p c args pred,
      eval_predf ps p = false ->
      instr_falsy ps (RBsetpred (Some p) c args pred)
  | RBexit_falsy:
    forall p cf,
      eval_predf ps p = false ->
      instr_falsy ps (RBexit (Some p) cf)
  .

Inductive state_equiv : instr_state -> instr_state -> Prop :=
| match_states_intro:
  forall ps ps' rs rs' m m',
    (forall x, rs !! x = rs' !! x) ->
    (forall x, ps !! x = ps' !! x) ->
    m = m' ->
    state_equiv (mk_instr_state rs ps  m) (mk_instr_state rs' ps' m').

Lemma state_equiv_refl x : state_equiv x x.
x: instr_state
state_equiv x x
Proof.
x: instr_state
state_equiv x x destruct x; constructor; crush. Qed.

Lemma state_equiv_commut x y : state_equiv x y -> state_equiv y x.
x, y: instr_state
state_equiv x y -> state_equiv y x
Proof.
x, y: instr_state
state_equiv x y -> state_equiv y x inversion 1; constructor; crush. Qed.

Lemma state_equiv_trans x y z :
  state_equiv x y -> state_equiv y z -> state_equiv x z.
x, y, z: instr_state
state_equiv x y -> state_equiv y z -> state_equiv x z
Proof.
x, y, z: instr_state
state_equiv x y -> state_equiv y z -> state_equiv x z repeat inversion 1; constructor; crush. Qed.

#[global] Instance state_equiv_Equivalence : Equivalence state_equiv :=
  { Equivalence_Reflexive := state_equiv_refl ;
    Equivalence_Symmetric := state_equiv_commut ;
    Equivalence_Transitive := state_equiv_trans ; }.

Lemma match_states_list :
  forall A (rs: Regmap.t A) rs',
  (forall r, rs !! r = rs' !! r) ->
  forall l, rs ## l = rs' ## l.
forall (A : Type) (rs : Regmap.t A) (rs' : PMap.t A),
(forall r : positive, rs !! r = rs' !! r) ->
forall l : list positive, rs ## l = rs' ## l
Proof.
forall (A : Type) (rs : Regmap.t A) (rs' : PMap.t A),
(forall r : positive, rs !! r = rs' !! r) ->
forall l : list positive, rs ## l = rs' ## l induction l; crush. Qed.

Lemma truthy_match_state :
  forall ps ps' p,
    (forall x, ps !! x = ps' !! x) ->
    truthy ps p ->
    truthy ps' p.
forall (ps ps' : PMap.t bool) (p : option pred_op),
(forall x : positive, ps !! x = ps' !! x) ->
truthy ps p -> truthy ps' p
Proof.
forall (ps ps' : PMap.t bool) (p : option pred_op),
(forall x : positive, ps !! x = ps' !! x) ->
truthy ps p -> truthy ps' p
  intros; destruct p; inv H0; constructor; auto.
ps, ps': PMap.t bool
p: pred_op
H: forall x : positive, ps !! x = ps' !! x
H2: eval_predf ps p = true
eval_predf ps' p = true
  erewrite eval_predf_pr_equiv; eauto.
Qed.

Lemma falsy_match_state :
  forall ps ps' p,
    (forall x, ps !! x = ps' !! x) ->
    falsy ps p ->
    falsy ps' p.
forall (ps ps' : PMap.t bool) (p : option pred_op),
(forall x : positive, ps !! x = ps' !! x) ->
falsy ps p -> falsy ps' p
Proof.
forall (ps ps' : PMap.t bool) (p : option pred_op),
(forall x : positive, ps !! x = ps' !! x) ->
falsy ps p -> falsy ps' p
  intros; destruct p; inv H0; constructor; auto.
ps, ps': PMap.t bool
p: pred_op
H: forall x : positive, ps !! x = ps' !! x
H2: eval_predf ps p = false
eval_predf ps' p = false
  erewrite eval_predf_pr_equiv; eauto.
Qed.

Lemma PTree_matches :
  forall A (v: A) res rs rs',
  (forall r, rs !! r = rs' !! r) ->
  forall x, (Regmap.set res v rs) !! x = (Regmap.set res v rs') !! x.
forall (A : Type) (v : A) (res : positive)
  (rs rs' : PMap.t A),
(forall r : positive, rs !! r = rs' !! r) ->
forall x : positive,
(rs # res <- v) !! x = (rs' # res <- v) !! x
Proof.
forall (A : Type) (v : A) (res : positive)
  (rs rs' : PMap.t A),
(forall r : positive, rs !! r = rs' !! r) ->
forall x : positive,
(rs # res <- v) !! x = (rs' # res <- v) !! x
  intros; destruct (Pos.eq_dec x res); subst;
  [ repeat rewrite Regmap.gss by auto
  | repeat rewrite Regmap.gso by auto ]; auto.
Qed.

Section RELABSTR.

  Context {A B : Type} (ge : Genv.t A B).

Step Instruction

Variant step_instr: val -> istate -> instr -> istate -> Prop :=
  | exec_RBnop:
    forall sp ist,
      step_instr sp (Iexec ist) RBnop (Iexec ist)
  | exec_RBop:
    forall op v res args rs m sp p pr,
      eval_operation ge sp op rs##args m = Some v ->
      truthy pr p ->
      step_instr sp (Iexec (mk_instr_state rs pr m)) (RBop p op args res)
                 (Iexec (mk_instr_state (rs#res <- v) pr m))
  | exec_RBload:
    forall addr rs args a chunk m v dst sp p pr,
      eval_addressing ge sp addr rs##args = Some a ->
      Mem.loadv chunk m a = Some v ->
      truthy pr p ->
      step_instr sp (Iexec (mk_instr_state rs pr m))
                 (RBload p chunk addr args dst) (Iexec (mk_instr_state (rs#dst <- v) pr m))
  | exec_RBstore:
    forall addr rs args a chunk m src m' sp p pr,
      eval_addressing ge sp addr rs##args = Some a ->
      Mem.storev chunk m a rs#src = Some m' ->
      truthy pr p ->
      step_instr sp (Iexec (mk_instr_state rs pr m))
                 (RBstore p chunk addr args src) (Iexec (mk_instr_state rs pr m'))
  | exec_RBsetpred:
    forall sp rs pr m p c b args p',
      Op.eval_condition c rs##args m = Some b ->
      truthy pr p' ->
      step_instr sp (Iexec (mk_instr_state rs pr m))
                 (RBsetpred p' c args p) (Iexec (mk_instr_state rs (pr#p <- b) m))
  | exec_RBexit:
    forall p c sp i,
      truthy (is_ps i) p ->
      step_instr sp (Iexec i) (RBexit p c) (Iterm i c)
  | exec_RB_falsy :
    forall sp st i,
      instr_falsy (is_ps st) i ->
      step_instr sp (Iexec st) i (Iexec st)
.

Lemma step_exists:
  forall sp i instr i' ti,
    step_instr sp (Iexec i) instr (Iexec i') ->
    state_equiv i ti ->
    exists ti',
      step_instr sp (Iexec ti) instr (Iexec ti')
      /\ state_equiv i' ti'.
A, B: Type
ge: Genv.t A B
forall (sp : val) (i : instr_state) (instr : instr)
  (i' ti : instr_state),
step_instr sp (Iexec i) instr (Iexec i') ->
state_equiv i ti ->
exists ti' : instr_state,
  step_instr sp (Iexec ti) instr (Iexec ti') /\
  state_equiv i' ti'
Proof.
A, B: Type
ge: Genv.t A B
forall (sp : val) (i : instr_state) (instr : instr)
  (i' ti : instr_state),
step_instr sp (Iexec i) instr (Iexec i') ->
state_equiv i ti ->
exists ti' : instr_state,
  step_instr sp (Iexec ti) instr (Iexec ti') /\
  state_equiv i' ti'
  inversion_clear 1; subst; intros.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i', ti: instr_state
H: state_equiv i' ti
exists ti' : instr_state,
  step_instr sp (Iexec ti) RBnop (Iexec ti') /\
  state_equiv i' ti'
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i', ti: instr_state
op: operation
v: val
res: reg
args: list positive
rs: Regmap.t val
m: mem
p: option pred_op
pr: predset
H0: eval_operation ge sp op rs ## args m = Some v
H1: truthy pr p
H: state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m |} ti
exists ti' : instr_state,
  step_instr sp (Iexec ti) 
    (RBop p op args res) 
    (Iexec ti') /\
  state_equiv
    {|
      is_rs := rs # res <- v; is_ps := pr; is_mem := m
    |} ti'
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i', ti: instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
m: mem
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
H1: Mem.loadv chunk m a = Some v
H2: truthy pr p
H: state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m |} ti
exists ti' : instr_state,
  step_instr sp (Iexec ti)
    (RBload p chunk addr args dst) 
    (Iexec ti') /\
  state_equiv
    {|
      is_rs := rs # dst <- v; is_ps := pr; is_mem := m
    |} ti'
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i', ti: instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
m: mem
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
H1: Mem.storev chunk m a rs !! src = Some m'
H2: truthy pr p
H: state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m |} ti
exists ti' : instr_state,
  step_instr sp (Iexec ti)
    (RBstore p chunk addr args src) 
    (Iexec ti') /\
  state_equiv
    {| is_rs := rs; is_ps := pr; is_mem := m' |} ti'
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i', ti: instr_state
rs: Regmap.t val
pr: predset
m: mem
p: predicate
c: condition
b: bool
args: list positive
p': option pred_op
H0: eval_condition c rs ## args m = Some b
H1: truthy pr p'
H: state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m |} ti
exists ti' : instr_state,
  step_instr sp (Iexec ti) 
    (RBsetpred p' c args p) 
    (Iexec ti') /\
  state_equiv
    {|
      is_rs := rs; is_ps := pr # p <- b; is_mem := m
    |} ti'
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i', ti: instr_state
H0: instr_falsy (is_ps i') instr0
H: state_equiv i' ti
exists ti' : instr_state,
  step_instr sp (Iexec ti) instr0 (Iexec ti') /\
  state_equiv i' ti'
  -
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i', ti: instr_state
H: state_equiv i' ti
exists ti' : instr_state,
  step_instr sp (Iexec ti) RBnop (Iexec ti') /\
  state_equiv i' ti' econstructor; split; eauto.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i', ti: instr_state
H: state_equiv i' ti
step_instr sp (Iexec ti) RBnop (Iexec ti) constructor.
  -
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i', ti: instr_state
op: operation
v: val
res: reg
args: list positive
rs: Regmap.t val
m: mem
p: option pred_op
pr: predset
H0: eval_operation ge sp op rs ## args m = Some v
H1: truthy pr p
H: state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m |} ti
exists ti' : instr_state,
  step_instr sp (Iexec ti) (RBop p op args res)
    (Iexec ti') /\
  state_equiv
    {|
      is_rs := rs # res <- v; is_ps := pr; is_mem := m
    |} ti' destruct ti; cbn in *.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
is_rs0: regset
is_ps0: predset
is_mem0: mem
op: operation
v: val
res: reg
args: list positive
rs: Regmap.t val
m: mem
p: option pred_op
pr: predset
H0: eval_operation ge sp op rs ## args m = Some v
H1: truthy pr p
H: state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m |}
  {|
    is_rs := is_rs0;
    is_ps := is_ps0;
    is_mem := is_mem0
  |}
exists ti' : instr_state,
  step_instr sp
    (Iexec
       {|
         is_rs := is_rs0;
         is_ps := is_ps0;
         is_mem := is_mem0
       |}) (RBop p op args res) (Iexec ti') /\
  state_equiv
    {|
      is_rs := rs # res <- v; is_ps := pr; is_mem := m
    |} ti' inv H.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
is_rs0: regset
is_ps0: predset
is_mem0: mem
op: operation
v: val
res: reg
args: list positive
rs: Regmap.t val
p: option pred_op
pr: predset
H0: eval_operation ge sp op rs ## args is_mem0 =
Some v
H1: truthy pr p
H6: forall x : positive, rs !! x = is_rs0 !! x
H9: forall x : positive, pr !! x = is_ps0 !! x
exists ti' : instr_state,
  step_instr sp
    (Iexec
       {|
         is_rs := is_rs0;
         is_ps := is_ps0;
         is_mem := is_mem0
       |}) (RBop p op args res) (Iexec ti') /\
  state_equiv
    {|
      is_rs := rs # res <- v;
      is_ps := pr;
      is_mem := is_mem0
    |} ti' econstructor.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
is_rs0: regset
is_ps0: predset
is_mem0: mem
op: operation
v: val
res: reg
args: list positive
rs: Regmap.t val
p: option pred_op
pr: predset
H0: eval_operation ge sp op rs ## args is_mem0 =
Some v
H1: truthy pr p
H6: forall x : positive, rs !! x = is_rs0 !! x
H9: forall x : positive, pr !! x = is_ps0 !! x
step_instr sp
  (Iexec
     {|
       is_rs := is_rs0;
       is_ps := is_ps0;
       is_mem := is_mem0
     |}) (RBop p op args res) (Iexec ?ti') /\
state_equiv
  {|
    is_rs := rs # res <- v;
    is_ps := pr;
    is_mem := is_mem0
  |} ?ti' split.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
is_rs0: regset
is_ps0: predset
is_mem0: mem
op: operation
v: val
res: reg
args: list positive
rs: Regmap.t val
p: option pred_op
pr: predset
H0: eval_operation ge sp op rs ## args is_mem0 =
Some v
H1: truthy pr p
H6: forall x : positive, rs !! x = is_rs0 !! x
H9: forall x : positive, pr !! x = is_ps0 !! x
step_instr sp
  (Iexec
     {|
       is_rs := is_rs0;
       is_ps := is_ps0;
       is_mem := is_mem0
     |}) (RBop p op args res) (Iexec ?ti')
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
is_rs0: regset
is_ps0: predset
is_mem0: mem
op: operation
v: val
res: reg
args: list positive
rs: Regmap.t val
p: option pred_op
pr: predset
H0: eval_operation ge sp op rs ## args is_mem0 =
Some v
H1: truthy pr p
H6: forall x : positive, rs !! x = is_rs0 !! x
H9: forall x : positive, pr !! x = is_ps0 !! x
state_equiv
  {|
    is_rs := rs # res <- v;
    is_ps := pr;
    is_mem := is_mem0
  |} ?ti'
    econstructor.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
is_rs0: regset
is_ps0: predset
is_mem0: mem
op: operation
v: val
res: reg
args: list positive
rs: Regmap.t val
p: option pred_op
pr: predset
H0: eval_operation ge sp op rs ## args is_mem0 =
Some v
H1: truthy pr p
H6: forall x : positive, rs !! x = is_rs0 !! x
H9: forall x : positive, pr !! x = is_ps0 !! x
eval_operation ge sp op is_rs0 ## args is_mem0 =
Some ?v
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
is_rs0: regset
is_ps0: predset
is_mem0: mem
op: operation
v: val
res: reg
args: list positive
rs: Regmap.t val
p: option pred_op
pr: predset
H0: eval_operation ge sp op rs ## args is_mem0 =
Some v
H1: truthy pr p
H6: forall x : positive, rs !! x = is_rs0 !! x
H9: forall x : positive, pr !! x = is_ps0 !! x
truthy is_ps0 p
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
is_rs0: regset
is_ps0: predset
is_mem0: mem
op: operation
v: val
res: reg
args: list positive
rs: Regmap.t val
p: option pred_op
pr: predset
H0: eval_operation ge sp op rs ## args is_mem0 =
Some v
H1: truthy pr p
H6: forall x : positive, rs !! x = is_rs0 !! x
H9: forall x : positive, pr !! x = is_ps0 !! x
state_equiv
  {|
    is_rs := rs # res <- v;
    is_ps := pr;
    is_mem := is_mem0
  |}
  {|
    is_rs := is_rs0 # res <- ?v;
    is_ps := is_ps0;
    is_mem := is_mem0
  |} erewrite match_states_list; eauto.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
is_rs0: regset
is_ps0: predset
is_mem0: mem
op: operation
v: val
res: reg
args: list positive
rs: Regmap.t val
p: option pred_op
pr: predset
H0: eval_operation ge sp op rs ## args is_mem0 =
Some v
H1: truthy pr p
H6: forall x : positive, rs !! x = is_rs0 !! x
H9: forall x : positive, pr !! x = is_ps0 !! x
truthy is_ps0 p
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
is_rs0: regset
is_ps0: predset
is_mem0: mem
op: operation
v: val
res: reg
args: list positive
rs: Regmap.t val
p: option pred_op
pr: predset
H0: eval_operation ge sp op rs ## args is_mem0 =
Some v
H1: truthy pr p
H6: forall x : positive, rs !! x = is_rs0 !! x
H9: forall x : positive, pr !! x = is_ps0 !! x
state_equiv
  {|
    is_rs := rs # res <- v;
    is_ps := pr;
    is_mem := is_mem0
  |}
  {|
    is_rs := is_rs0 # res <- v;
    is_ps := is_ps0;
    is_mem := is_mem0
  |}
    eapply truthy_match_state; eauto.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
is_rs0: regset
is_ps0: predset
is_mem0: mem
op: operation
v: val
res: reg
args: list positive
rs: Regmap.t val
p: option pred_op
pr: predset
H0: eval_operation ge sp op rs ## args is_mem0 =
Some v
H1: truthy pr p
H6: forall x : positive, rs !! x = is_rs0 !! x
H9: forall x : positive, pr !! x = is_ps0 !! x
state_equiv
  {|
    is_rs := rs # res <- v;
    is_ps := pr;
    is_mem := is_mem0
  |}
  {|
    is_rs := is_rs0 # res <- v;
    is_ps := is_ps0;
    is_mem := is_mem0
  |} constructor; auto.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
is_rs0: regset
is_ps0: predset
is_mem0: mem
op: operation
v: val
res: reg
args: list positive
rs: Regmap.t val
p: option pred_op
pr: predset
H0: eval_operation ge sp op rs ## args is_mem0 =
Some v
H1: truthy pr p
H6: forall x : positive, rs !! x = is_rs0 !! x
H9: forall x : positive, pr !! x = is_ps0 !! x
forall x : positive,
(rs # res <- v) !! x = (is_rs0 # res <- v) !! x
    eapply PTree_matches; auto.
  -
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i', ti: instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
m: mem
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
H1: Mem.loadv chunk m a = Some v
H2: truthy pr p
H: state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m |} ti
exists ti' : instr_state,
  step_instr sp (Iexec ti)
    (RBload p chunk addr args dst) (Iexec ti') /\
  state_equiv
    {|
      is_rs := rs # dst <- v; is_ps := pr; is_mem := m
    |} ti' inv H; cbn in *.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m': mem
H1: Mem.loadv chunk m' a = Some v
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
exists ti' : instr_state,
  step_instr sp
    (Iexec
       {| is_rs := rs'; is_ps := ps'; is_mem := m' |})
    (RBload p chunk addr args dst) (Iexec ti') /\
  state_equiv
    {|
      is_rs := rs # dst <- v;
      is_ps := pr;
      is_mem := m'
    |} ti' eexists; split.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m': mem
H1: Mem.loadv chunk m' a = Some v
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
step_instr sp
  (Iexec
     {| is_rs := rs'; is_ps := ps'; is_mem := m' |})
  (RBload p chunk addr args dst) (Iexec ?ti')
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m': mem
H1: Mem.loadv chunk m' a = Some v
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
state_equiv
  {|
    is_rs := rs # dst <- v; is_ps := pr; is_mem := m'
  |} ?ti' econstructor.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m': mem
H1: Mem.loadv chunk m' a = Some v
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
eval_addressing ge sp addr rs' ## args = Some ?a
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m': mem
H1: Mem.loadv chunk m' a = Some v
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
Mem.loadv chunk m' ?a = Some ?v
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m': mem
H1: Mem.loadv chunk m' a = Some v
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
truthy ps' p
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m': mem
H1: Mem.loadv chunk m' a = Some v
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
state_equiv
  {|
    is_rs := rs # dst <- v; is_ps := pr; is_mem := m'
  |}
  {|
    is_rs := rs' # dst <- ?v;
    is_ps := ps';
    is_mem := m'
  |}
    erewrite match_states_list; eauto.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m': mem
H1: Mem.loadv chunk m' a = Some v
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
Mem.loadv chunk m' a = Some ?v
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m': mem
H1: Mem.loadv chunk m' a = Some v
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
truthy ps' p
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m': mem
H1: Mem.loadv chunk m' a = Some v
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
state_equiv
  {|
    is_rs := rs # dst <- v; is_ps := pr; is_mem := m'
  |}
  {|
    is_rs := rs' # dst <- ?v;
    is_ps := ps';
    is_mem := m'
  |} eauto.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m': mem
H1: Mem.loadv chunk m' a = Some v
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
truthy ps' p
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m': mem
H1: Mem.loadv chunk m' a = Some v
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
state_equiv
  {|
    is_rs := rs # dst <- v; is_ps := pr; is_mem := m'
  |}
  {|
    is_rs := rs' # dst <- v;
    is_ps := ps';
    is_mem := m'
  |}
    eapply truthy_match_state; eauto.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m': mem
H1: Mem.loadv chunk m' a = Some v
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
state_equiv
  {|
    is_rs := rs # dst <- v; is_ps := pr; is_mem := m'
  |}
  {|
    is_rs := rs' # dst <- v;
    is_ps := ps';
    is_mem := m'
  |} constructor; auto.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
v: val
dst: reg
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m': mem
H1: Mem.loadv chunk m' a = Some v
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
forall x : positive,
(rs # dst <- v) !! x = (rs' # dst <- v) !! x
    eapply PTree_matches; auto.
  -
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i', ti: instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
m: mem
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
H1: Mem.storev chunk m a rs !! src = Some m'
H2: truthy pr p
H: state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m |} ti
exists ti' : instr_state,
  step_instr sp (Iexec ti)
    (RBstore p chunk addr args src) (Iexec ti') /\
  state_equiv
    {| is_rs := rs; is_ps := pr; is_mem := m' |} ti' inv H; cbn in *.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
exists ti' : instr_state,
  step_instr sp
    (Iexec
       {| is_rs := rs'; is_ps := ps'; is_mem := m'0 |})
    (RBstore p chunk addr args src) (Iexec ti') /\
  state_equiv
    {| is_rs := rs; is_ps := pr; is_mem := m' |} ti' eexists; split.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
step_instr sp
  (Iexec
     {| is_rs := rs'; is_ps := ps'; is_mem := m'0 |})
  (RBstore p chunk addr args src) (Iexec ?ti')
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m' |} 
  ?ti' econstructor.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
eval_addressing ge sp addr rs' ## args = Some ?a
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
Mem.storev chunk m'0 ?a rs' !! src = Some ?m'
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
truthy ps' p
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m' |}
  {| is_rs := rs'; is_ps := ps'; is_mem := ?m' |}
    erewrite match_states_list; eauto.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
Mem.storev chunk m'0 a rs' !! src = Some ?m'
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
truthy ps' p
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m' |}
  {| is_rs := rs'; is_ps := ps'; is_mem := ?m' |} rewrite <- H6.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
Mem.storev chunk m'0 a rs !! src = Some ?m'
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
truthy ps' p
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m' |}
  {| is_rs := rs'; is_ps := ps'; is_mem := ?m' |} eauto.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
truthy ps' p
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m' |}
  {| is_rs := rs'; is_ps := ps'; is_mem := m' |}
    eapply truthy_match_state; eauto.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
addr: addressing
rs: Regmap.t val
args: list positive
a: val
chunk: memory_chunk
src: positive
m': mem
p: option pred_op
pr: predset
H0: eval_addressing ge sp addr rs ## args = Some a
m'0: mem
H1: Mem.storev chunk m'0 a rs !! src = Some m'
H2: truthy pr p
ps': PMap.t bool
rs': PMap.t val
H6: forall x : positive, rs !! x = rs' !! x
H8: forall x : positive, pr !! x = ps' !! x
state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m' |}
  {| is_rs := rs'; is_ps := ps'; is_mem := m' |} constructor; auto.
  -
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i', ti: instr_state
rs: Regmap.t val
pr: predset
m: mem
p: predicate
c: condition
b: bool
args: list positive
p': option pred_op
H0: eval_condition c rs ## args m = Some b
H1: truthy pr p'
H: state_equiv
  {| is_rs := rs; is_ps := pr; is_mem := m |} ti
exists ti' : instr_state,
  step_instr sp (Iexec ti) (RBsetpred p' c args p)
    (Iexec ti') /\
  state_equiv
    {|
      is_rs := rs; is_ps := pr # p <- b; is_mem := m
    |} ti' inv H.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
rs: Regmap.t val
pr: predset
p: predicate
c: condition
b: bool
args: list positive
p': option pred_op
m': mem
H0: eval_condition c rs ## args m' = Some b
H1: truthy pr p'
ps': PMap.t bool
rs': PMap.t val
H5: forall x : positive, rs !! x = rs' !! x
H7: forall x : positive, pr !! x = ps' !! x
exists ti' : instr_state,
  step_instr sp
    (Iexec
       {| is_rs := rs'; is_ps := ps'; is_mem := m' |})
    (RBsetpred p' c args p) (Iexec ti') /\
  state_equiv
    {|
      is_rs := rs; is_ps := pr # p <- b; is_mem := m'
    |} ti' econstructor.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
rs: Regmap.t val
pr: predset
p: predicate
c: condition
b: bool
args: list positive
p': option pred_op
m': mem
H0: eval_condition c rs ## args m' = Some b
H1: truthy pr p'
ps': PMap.t bool
rs': PMap.t val
H5: forall x : positive, rs !! x = rs' !! x
H7: forall x : positive, pr !! x = ps' !! x
step_instr sp
  (Iexec
     {| is_rs := rs'; is_ps := ps'; is_mem := m' |})
  (RBsetpred p' c args p) (Iexec ?ti') /\
state_equiv
  {|
    is_rs := rs; is_ps := pr # p <- b; is_mem := m'
  |} ?ti' split.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
rs: Regmap.t val
pr: predset
p: predicate
c: condition
b: bool
args: list positive
p': option pred_op
m': mem
H0: eval_condition c rs ## args m' = Some b
H1: truthy pr p'
ps': PMap.t bool
rs': PMap.t val
H5: forall x : positive, rs !! x = rs' !! x
H7: forall x : positive, pr !! x = ps' !! x
step_instr sp
  (Iexec
     {| is_rs := rs'; is_ps := ps'; is_mem := m' |})
  (RBsetpred p' c args p) (Iexec ?ti')
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
rs: Regmap.t val
pr: predset
p: predicate
c: condition
b: bool
args: list positive
p': option pred_op
m': mem
H0: eval_condition c rs ## args m' = Some b
H1: truthy pr p'
ps': PMap.t bool
rs': PMap.t val
H5: forall x : positive, rs !! x = rs' !! x
H7: forall x : positive, pr !! x = ps' !! x
state_equiv
  {|
    is_rs := rs; is_ps := pr # p <- b; is_mem := m'
  |} ?ti' econstructor.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
rs: Regmap.t val
pr: predset
p: predicate
c: condition
b: bool
args: list positive
p': option pred_op
m': mem
H0: eval_condition c rs ## args m' = Some b
H1: truthy pr p'
ps': PMap.t bool
rs': PMap.t val
H5: forall x : positive, rs !! x = rs' !! x
H7: forall x : positive, pr !! x = ps' !! x
eval_condition c rs' ## args m' = Some ?b
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
rs: Regmap.t val
pr: predset
p: predicate
c: condition
b: bool
args: list positive
p': option pred_op
m': mem
H0: eval_condition c rs ## args m' = Some b
H1: truthy pr p'
ps': PMap.t bool
rs': PMap.t val
H5: forall x : positive, rs !! x = rs' !! x
H7: forall x : positive, pr !! x = ps' !! x
truthy ps' p'
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
rs: Regmap.t val
pr: predset
p: predicate
c: condition
b: bool
args: list positive
p': option pred_op
m': mem
H0: eval_condition c rs ## args m' = Some b
H1: truthy pr p'
ps': PMap.t bool
rs': PMap.t val
H5: forall x : positive, rs !! x = rs' !! x
H7: forall x : positive, pr !! x = ps' !! x
state_equiv
  {|
    is_rs := rs; is_ps := pr # p <- b; is_mem := m'
  |}
  {|
    is_rs := rs'; is_ps := ps' # p <- ?b; is_mem := m'
  |} erewrite match_states_list; eauto.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
rs: Regmap.t val
pr: predset
p: predicate
c: condition
b: bool
args: list positive
p': option pred_op
m': mem
H0: eval_condition c rs ## args m' = Some b
H1: truthy pr p'
ps': PMap.t bool
rs': PMap.t val
H5: forall x : positive, rs !! x = rs' !! x
H7: forall x : positive, pr !! x = ps' !! x
truthy ps' p'
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
rs: Regmap.t val
pr: predset
p: predicate
c: condition
b: bool
args: list positive
p': option pred_op
m': mem
H0: eval_condition c rs ## args m' = Some b
H1: truthy pr p'
ps': PMap.t bool
rs': PMap.t val
H5: forall x : positive, rs !! x = rs' !! x
H7: forall x : positive, pr !! x = ps' !! x
state_equiv
  {|
    is_rs := rs; is_ps := pr # p <- b; is_mem := m'
  |}
  {|
    is_rs := rs'; is_ps := ps' # p <- b; is_mem := m'
  |}
    eapply truthy_match_state; eauto.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
rs: Regmap.t val
pr: predset
p: predicate
c: condition
b: bool
args: list positive
p': option pred_op
m': mem
H0: eval_condition c rs ## args m' = Some b
H1: truthy pr p'
ps': PMap.t bool
rs': PMap.t val
H5: forall x : positive, rs !! x = rs' !! x
H7: forall x : positive, pr !! x = ps' !! x
state_equiv
  {|
    is_rs := rs; is_ps := pr # p <- b; is_mem := m'
  |}
  {|
    is_rs := rs'; is_ps := ps' # p <- b; is_mem := m'
  |} constructor; auto.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i': instr_state
rs: Regmap.t val
pr: predset
p: predicate
c: condition
b: bool
args: list positive
p': option pred_op
m': mem
H0: eval_condition c rs ## args m' = Some b
H1: truthy pr p'
ps': PMap.t bool
rs': PMap.t val
H5: forall x : positive, rs !! x = rs' !! x
H7: forall x : positive, pr !! x = ps' !! x
forall x : positive,
(pr # p <- b) !! x = (ps' # p <- b) !! x
    eapply PTree_matches; auto.
  -
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
i', ti: instr_state
H0: instr_falsy (is_ps i') instr0
H: state_equiv i' ti
exists ti' : instr_state,
  step_instr sp (Iexec ti) instr0 (Iexec ti') /\
  state_equiv i' ti' inv H0; exists ti; split; auto;
      repeat constructor; inv H; erewrite eval_predf_pr_equiv; eauto.
Qed.

Lemma step_exists_Iterm:
  forall sp i instr ti cf,
    step_instr sp (Iexec i) instr (Iterm i cf) ->
    state_equiv i ti ->
    step_instr sp (Iexec ti) instr (Iterm ti cf).
A, B: Type
ge: Genv.t A B
forall (sp : val) (i : instr_state) (instr : instr)
  (ti : instr_state) (cf : cf_instr),
step_instr sp (Iexec i) instr (Iterm i cf) ->
state_equiv i ti ->
step_instr sp (Iexec ti) instr (Iterm ti cf)
Proof.
A, B: Type
ge: Genv.t A B
forall (sp : val) (i : instr_state) (instr : instr)
  (ti : instr_state) (cf : cf_instr),
step_instr sp (Iexec i) instr (Iterm i cf) ->
state_equiv i ti ->
step_instr sp (Iexec ti) instr (Iterm ti cf)
  inversion_clear 1; subst; intros.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
ti: instr_state
cf: cf_instr
p: option pred_op
H0: truthy (is_ps i) p
H: state_equiv i ti
step_instr sp (Iexec ti) (RBexit p cf) (Iterm ti cf)
  econstructor.
A, B: Type
ge: Genv.t A B
sp: val
i: instr_state
instr0: instr
ti: instr_state
cf: cf_instr
p: option pred_op
H0: truthy (is_ps i) p
H: state_equiv i ti
truthy (is_ps ti) p
  inv H.
A, B: Type
ge: Genv.t A B
sp: val
instr0: instr
cf: cf_instr
p: option pred_op
ps: PMap.t bool
rs: PMap.t val
m': mem
H0: truthy
  (is_ps
     {| is_rs := rs; is_ps := ps; is_mem := m' |})
  p
ps': PMap.t bool
rs': PMap.t val
H1: forall x : positive, rs !! x = rs' !! x
H2: forall x : positive, ps !! x = ps' !! x
truthy
  (is_ps
     {| is_rs := rs'; is_ps := ps'; is_mem := m' |}) p eapply truthy_match_state; eauto.
Qed.

End RELABSTR.

A big-step semantics describing the execution of a list of instructions. This uses a higher-order function step_i, so that this Inductive can be nested to describe the execution of nested lists.

Inductive step_list {A} (step_i: val -> istate -> A -> istate -> Prop):
  val -> istate -> list A -> istate -> Prop :=
| exec_RBcons :
  forall state i state' state'' instrs sp cf,
    step_i sp (Iexec state) i (Iexec state') ->
    step_list step_i sp (Iexec state') instrs (Iterm state'' cf) ->
    step_list step_i sp (Iexec state) (i :: instrs) (Iterm state'' cf)
| exec_RBterm :
  forall state sp i state' cf instrs,
    step_i sp (Iexec state) i (Iterm state' cf) ->
    step_list step_i sp (Iexec state) (i :: instrs) (Iterm state' cf).

Inductive step_list_nth {A} (step_i: val -> istate -> A -> istate -> Prop):
  val -> nat -> istate -> list A -> nat -> istate -> Prop :=
| exec_RBnth_refl :
  forall out n instrs sp,
    step_list_nth step_i sp n out instrs n out
| exec_RBnth_star :
  forall state i n out instrs sp m out',
    nth_error instrs n = Some i ->
    step_i sp state i out ->
    step_list_nth step_i sp (S n) out instrs m out' ->
    (n < m)%nat ->
    step_list_nth step_i sp n state instrs m out'.

Lemma list_drop_nil :
  forall A n, @list_drop A n nil = nil.
forall (A : Type) (n : nat), list_drop n nil = nil
Proof.
forall (A : Type) (n : nat), list_drop n nil = nil intros.
A: Type
n: nat
list_drop n nil = nil destruct n; auto. Qed.

Lemma list_drop_length :
  forall A n (l: list A), (length l <= n)%nat -> @list_drop A n l = nil.
forall (A : Type) (n : nat) (l : list A),
(Datatypes.length l <= n)%nat -> list_drop n l = nil
Proof.
forall (A : Type) (n : nat) (l : list A),
(Datatypes.length l <= n)%nat -> list_drop n l = nil 
  induction n; intros.
A: Type
l: list A
H: (Datatypes.length l <= 0)%nat
list_drop 0 l = nil
A: Type
n: nat
IHn: forall l : list A, (Datatypes.length l <= n)%nat -> list_drop n l = nil
l: list A
H: (Datatypes.length l <= S n)%nat
list_drop (S n) l = nil
  -
A: Type
l: list A
H: (Datatypes.length l <= 0)%nat
list_drop 0 l = nil destruct l; cbn in *; auto.
A: Type
a: A
l: list A
H: (S (Datatypes.length l) <= 0)%nat
a :: l = nil lia.
  -
A: Type
n: nat
IHn: forall l : list A, (Datatypes.length l <= n)%nat -> list_drop n l = nil
l: list A
H: (Datatypes.length l <= S n)%nat
list_drop (S n) l = nil destruct l; cbn; auto.
A: Type
n: nat
IHn: forall l : list A, (Datatypes.length l <= n)%nat -> list_drop n l = nil
a: A
l: list A
H: (Datatypes.length (a :: l) <= S n)%nat
list_drop n l = nil
    rewrite IHn; eauto.
A: Type
n: nat
IHn: forall l : list A, (Datatypes.length l <= n)%nat -> list_drop n l = nil
a: A
l: list A
H: (Datatypes.length (a :: l) <= S n)%nat
(Datatypes.length l <= n)%nat cbn in *.
A: Type
n: nat
IHn: forall l : list A, (Datatypes.length l <= n)%nat -> list_drop n l = nil
a: A
l: list A
H: (S (Datatypes.length l) <= S n)%nat
(Datatypes.length l <= n)%nat lia.
Qed.

Lemma step_list_equiv_nth:
  forall A (step_i: val -> istate -> A -> istate -> Prop) sp l n m st1 st2,
    step_list_nth step_i sp n st1 l m st2 ->
    forall offs l',
    (forall x e, (n <= x < m)%nat -> nth_error l x = Some e -> nth_error l' (x+offs) = Some e) ->
    step_list_nth step_i sp (n+offs) st1 l' (m+offs) st2.
forall (A : Type)
  (step_i : val -> istate -> A -> istate -> Prop)
  (sp : val) (l : list A) (n m : nat)
  (st1 st2 : istate),
step_list_nth step_i sp n st1 l m st2 ->
forall (offs : nat) (l' : list A),
(forall (x : nat) (e : A),
 (n <= x < m)%nat ->
 nth_error l x = Some e ->
 nth_error l' (x + offs) = Some e) ->
step_list_nth step_i sp (n + offs) st1 l' (m + offs)
  st2
Proof.
forall (A : Type)
  (step_i : val -> istate -> A -> istate -> Prop)
  (sp : val) (l : list A) (n m : nat)
  (st1 st2 : istate),
step_list_nth step_i sp n st1 l m st2 ->
forall (offs : nat) (l' : list A),
(forall (x : nat) (e : A),
 (n <= x < m)%nat ->
 nth_error l x = Some e ->
 nth_error l' (x + offs) = Some e) ->
step_list_nth step_i sp (n + offs) st1 l' (m + offs)
  st2
  induction 1.
A: Type
step_i: val -> istate -> A -> istate -> Prop
out: istate
n: nat
instrs: list A
sp: val
forall (offs : nat) (l' : list A),
(forall (x : nat) (e : A),
 (n <= x < n)%nat ->
 nth_error instrs x = Some e ->
 nth_error l' (x + offs) = Some e) ->
step_list_nth step_i sp (n + offs) out l' (n + offs)
  out
A: Type
step_i: val -> istate -> A -> istate -> Prop
state: istate
i: A
n: nat
out: istate
instrs: list A
sp: val
m: nat
out': istate
H: nth_error instrs n = Some i
H0: step_i sp state i out
H1: step_list_nth step_i sp (S n) out instrs m out'
H2: (n < m)%nat
IHstep_list_nth: forall (offs : nat) (l' : list A),
(forall (x : nat) (e : A),
 (S n <= x < m)%nat ->
 nth_error instrs x = Some e ->
 nth_error l' (x + offs) = Some e) ->
step_list_nth step_i sp 
  (S n + offs) out l' (m + offs)
  out'
forall (offs : nat) (l' : list A),
(forall (x : nat) (e : A),
 (n <= x < m)%nat ->
 nth_error instrs x = Some e ->
 nth_error l' (x + offs) = Some e) ->
step_list_nth step_i sp 
  (n + offs) state l' (m + offs) out' intros.
A: Type
step_i: val -> istate -> A -> istate -> Prop
out: istate
n: nat
instrs: list A
sp: val
offs: nat
l': list A
H: forall (x : nat) (e : A),
(n <= x < n)%nat ->
nth_error instrs x = Some e ->
nth_error l' (x + offs) = Some e
step_list_nth step_i sp 
  (n + offs) out l' (n + offs) out
A: Type
step_i: val -> istate -> A -> istate -> Prop
state: istate
i: A
n: nat
out: istate
instrs: list A
sp: val
m: nat
out': istate
H: nth_error instrs n = Some i
H0: step_i sp state i out
H1: step_list_nth step_i sp (S n) out instrs m out'
H2: (n < m)%nat
IHstep_list_nth: forall (offs : nat) (l' : list A),
(forall (x : nat) (e : A),
 (S n <= x < m)%nat ->
 nth_error instrs x = Some e ->
 nth_error l' (x + offs) = Some e) ->
step_list_nth step_i sp 
  (S n + offs) out l' (m + offs)
  out'
forall (offs : nat) (l' : list A),
(forall (x : nat) (e : A),
 (n <= x < m)%nat ->
 nth_error instrs x = Some e ->
 nth_error l' (x + offs) = Some e) ->
step_list_nth step_i sp 
  (n + offs) state l' (m + offs) out' constructor.
A: Type
step_i: val -> istate -> A -> istate -> Prop
state: istate
i: A
n: nat
out: istate
instrs: list A
sp: val
m: nat
out': istate
H: nth_error instrs n = Some i
H0: step_i sp state i out
H1: step_list_nth step_i sp (S n) out instrs m out'
H2: (n < m)%nat
IHstep_list_nth: forall (offs : nat) (l' : list A),
(forall (x : nat) (e : A),
 (S n <= x < m)%nat ->
 nth_error instrs x = Some e ->
 nth_error l' (x + offs) = Some e) ->
step_list_nth step_i sp 
  (S n + offs) out l' (m + offs)
  out'
forall (offs : nat) (l' : list A),
(forall (x : nat) (e : A),
 (n <= x < m)%nat ->
 nth_error instrs x = Some e ->
 nth_error l' (x + offs) = Some e) ->
step_list_nth step_i sp 
  (n + offs) state l' (m + offs) out'
  intros.
A: Type
step_i: val -> istate -> A -> istate -> Prop
state: istate
i: A
n: nat
out: istate
instrs: list A
sp: val
m: nat
out': istate
H: nth_error instrs n = Some i
H0: step_i sp state i out
H1: step_list_nth step_i sp (S n) out instrs m out'
H2: (n < m)%nat
IHstep_list_nth: forall (offs : nat) (l' : list A),
(forall (x : nat) (e : A),
 (S n <= x < m)%nat ->
 nth_error instrs x = Some e ->
 nth_error l' (x + offs) = Some e) ->
step_list_nth step_i sp 
  (S n + offs) out l' (m + offs)
  out'
offs: nat
l': list A
H3: forall (x : nat) (e : A),
(n <= x < m)%nat ->
nth_error instrs x = Some e ->
nth_error l' (x + offs) = Some e
step_list_nth step_i sp 
  (n + offs) state l' (m + offs) out' econstructor; eauto; [|lia].
A: Type
step_i: val -> istate -> A -> istate -> Prop
state: istate
i: A
n: nat
out: istate
instrs: list A
sp: val
m: nat
out': istate
H: nth_error instrs n = Some i
H0: step_i sp state i out
H1: step_list_nth step_i sp (S n) out instrs m out'
H2: (n < m)%nat
IHstep_list_nth: forall (offs : nat) (l' : list A),
(forall (x : nat) (e : A),
 (S n <= x < m)%nat ->
 nth_error instrs x = Some e ->
 nth_error l' (x + offs) = Some e) ->
step_list_nth step_i sp 
  (S n + offs) out l' (m + offs)
  out'
offs: nat
l': list A
H3: forall (x : nat) (e : A),
(n <= x < m)%nat ->
nth_error instrs x = Some e ->
nth_error l' (x + offs) = Some e
step_list_nth step_i sp 
  (S (n + offs)) out l' 
  (m + offs) out'
  eapply IHstep_list_nth; eauto.
A: Type
step_i: val -> istate -> A -> istate -> Prop
state: istate
i: A
n: nat
out: istate
instrs: list A
sp: val
m: nat
out': istate
H: nth_error instrs n = Some i
H0: step_i sp state i out
H1: step_list_nth step_i sp (S n) out instrs m out'
H2: (n < m)%nat
IHstep_list_nth: forall (offs : nat) (l' : list A),
(forall (x : nat) (e : A),
 (S n <= x < m)%nat ->
 nth_error instrs x = Some e ->
 nth_error l' (x + offs) = Some e) ->
step_list_nth step_i sp 
  (S n + offs) out l' (m + offs)
  out'
offs: nat
l': list A
H3: forall (x : nat) (e : A),
(n <= x < m)%nat ->
nth_error instrs x = Some e ->
nth_error l' (x + offs) = Some e
forall (x : nat) (e : A),
(S n <= x < m)%nat ->
nth_error instrs x = Some e ->
nth_error l' (x + offs) = Some e
  intros.
A: Type
step_i: val -> istate -> A -> istate -> Prop
state: istate
i: A
n: nat
out: istate
instrs: list A
sp: val
m: nat
out': istate
H: nth_error instrs n = Some i
H0: step_i sp state i out
H1: step_list_nth step_i sp (S n) out instrs m out'
H2: (n < m)%nat
IHstep_list_nth: forall (offs : nat) (l' : list A),
(forall (x : nat) (e : A),
 (S n <= x < m)%nat ->
 nth_error instrs x = Some e ->
 nth_error l' (x + offs) = Some e) ->
step_list_nth step_i sp 
  (S n + offs) out l' (m + offs)
  out'
offs: nat
l': list A
H3: forall (x : nat) (e : A),
(n <= x < m)%nat ->
nth_error instrs x = Some e ->
nth_error l' (x + offs) = Some e
x: nat
e: A
H4: (S n <= x < m)%nat
H5: nth_error instrs x = Some e
nth_error l' (x + offs) = Some e eapply H3; auto; lia.
Qed.

Lemma step_list_nth_cons':
  forall A (step_i: val -> istate -> A -> istate -> Prop) sp 
      n m (l: list A) a st1 st2,
    step_list_nth step_i sp n st1 l m st2 ->
    step_list_nth step_i sp (S n) st1 (a :: l) (S m) st2.
forall (A : Type)
  (step_i : val -> istate -> A -> istate -> Prop)
  (sp : val) (n m : nat) (l : list A) (a : A)
  (st1 st2 : istate),
step_list_nth step_i sp n st1 l m st2 ->
step_list_nth step_i sp (S n) st1 (a :: l) (S m) st2
Proof.
forall (A : Type)
  (step_i : val -> istate -> A -> istate -> Prop)
  (sp : val) (n m : nat) (l : list A) (a : A)
  (st1 st2 : istate),
step_list_nth step_i sp n st1 l m st2 ->
step_list_nth step_i sp (S n) st1 (a :: l) (S m) st2
  intros * Hstep.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
n, m: nat
l: list A
a: A
st1, st2: istate
Hstep: step_list_nth step_i sp n st1 l m st2
step_list_nth step_i sp (S n) st1 (a :: l) (S m) st2
  assert (Hequiv: forall x e, (n <= x < m)%nat -> nth_error l x = Some e -> nth_error (a :: l) (x+1) = Some e).
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
n, m: nat
l: list A
a: A
st1, st2: istate
Hstep: step_list_nth step_i sp n st1 l m st2
forall (x : nat) (e : A),
(n <= x < m)%nat ->
nth_error l x = Some e ->
nth_error (a :: l) (x + 1) = Some e
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
n, m: nat
l: list A
a: A
st1, st2: istate
Hstep: step_list_nth step_i sp n st1 l m st2
Hequiv: forall (x : nat) (e : A),
(n <= x < m)%nat ->
nth_error l x = Some e ->
nth_error (a :: l) (x + 1) = Some e
step_list_nth step_i sp (S n) st1 (a :: l) (S m) st2
  {
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
n, m: nat
l: list A
a: A
st1, st2: istate
Hstep: step_list_nth step_i sp n st1 l m st2
forall (x : nat) (e : A),
(n <= x < m)%nat ->
nth_error l x = Some e ->
nth_error (a :: l) (x + 1) = Some e intros.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
n, m: nat
l: list A
a: A
st1, st2: istate
Hstep: step_list_nth step_i sp n st1 l m st2
x: nat
e: A
H: (n <= x < m)%nat
H0: nth_error l x = Some e
nth_error (a :: l) (x + 1) = Some e replace (a :: l) with ((a :: nil) ++ l) by auto.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
n, m: nat
l: list A
a: A
st1, st2: istate
Hstep: step_list_nth step_i sp n st1 l m st2
x: nat
e: A
H: (n <= x < m)%nat
H0: nth_error l x = Some e
nth_error ((a :: nil) ++ l) (x + 1) = Some e
    rewrite nth_error_app2 by (cbn; lia).
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
n, m: nat
l: list A
a: A
st1, st2: istate
Hstep: step_list_nth step_i sp n st1 l m st2
x: nat
e: A
H: (n <= x < m)%nat
H0: nth_error l x = Some e
nth_error l (x + 1 - Datatypes.length (a :: nil)) =
Some e
    cbn.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
n, m: nat
l: list A
a: A
st1, st2: istate
Hstep: step_list_nth step_i sp n st1 l m st2
x: nat
e: A
H: (n <= x < m)%nat
H0: nth_error l x = Some e
nth_error l (x + 1 - 1) = Some e now replace ((x + 1 - 1)%nat) with x by lia.
  }
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
n, m: nat
l: list A
a: A
st1, st2: istate
Hstep: step_list_nth step_i sp n st1 l m st2
Hequiv: forall (x : nat) (e : A),
(n <= x < m)%nat ->
nth_error l x = Some e ->
nth_error (a :: l) (x + 1) = Some e
step_list_nth step_i sp (S n) st1 (a :: l) (S m) st2
  replace (S n) with (n + 1)%nat by lia.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
n, m: nat
l: list A
a: A
st1, st2: istate
Hstep: step_list_nth step_i sp n st1 l m st2
Hequiv: forall (x : nat) (e : A),
(n <= x < m)%nat ->
nth_error l x = Some e ->
nth_error (a :: l) (x + 1) = Some e
step_list_nth step_i sp (n + 1) st1 (a :: l) (S m) st2
  replace (S m) with (m + 1)%nat by lia.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
n, m: nat
l: list A
a: A
st1, st2: istate
Hstep: step_list_nth step_i sp n st1 l m st2
Hequiv: forall (x : nat) (e : A),
(n <= x < m)%nat ->
nth_error l x = Some e ->
nth_error (a :: l) (x + 1) = Some e
step_list_nth step_i sp 
  (n + 1) st1 (a :: l) (m + 1) st2
  eapply step_list_equiv_nth; eauto.
Qed.

Lemma step_list_nth_cons :
  forall A (step_i: val -> istate -> A -> istate -> Prop) sp 
      (instrs: list A) (a: A) l st1 st2 st3,
    step_i sp st1 a st2 ->
    step_list_nth step_i sp 0 st2 instrs l st3 ->
    step_list_nth step_i sp 0 st1 (a :: instrs) (S l) st3.
forall (A : Type)
  (step_i : val -> istate -> A -> istate -> Prop)
  (sp : val) (instrs : list A) (a : A) (l : nat)
  (st1 st2 st3 : istate),
step_i sp st1 a st2 ->
step_list_nth step_i sp 0 st2 instrs l st3 ->
step_list_nth step_i sp 0 st1 (a :: instrs) (S l) st3
Proof.
forall (A : Type)
  (step_i : val -> istate -> A -> istate -> Prop)
  (sp : val) (instrs : list A) (a : A) (l : nat)
  (st1 st2 st3 : istate),
step_i sp st1 a st2 ->
step_list_nth step_i sp 0 st2 instrs l st3 ->
step_list_nth step_i sp 0 st1 (a :: instrs) (S l) st3
  intros.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
instrs: list A
a: A
l: nat
st1, st2, st3: istate
H: step_i sp st1 a st2
H0: step_list_nth step_i sp 0 st2 instrs l st3
step_list_nth step_i sp 0 st1 (a :: instrs) (S l) st3 econstructor; cbn; eauto; [|lia].
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
instrs: list A
a: A
l: nat
st1, st2, st3: istate
H: step_i sp st1 a st2
H0: step_list_nth step_i sp 0 st2 instrs l st3
step_list_nth step_i sp 1 st2 (a :: instrs) (S l) st3
  replace 1%nat with (0 + 1)%nat at 1 by lia.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
instrs: list A
a: A
l: nat
st1, st2, st3: istate
H: step_i sp st1 a st2
H0: step_list_nth step_i sp 0 st2 instrs l st3
step_list_nth step_i sp 
  (0 + 1) st2 (a :: instrs) 
  (S l) st3 
  now apply step_list_nth_cons'.
Qed.

Lemma step_list_equiv :
  forall A step_i sp (instrs: list A) st1 st2,
    step_list step_i sp st1 instrs st2 ->
    exists l, step_list_nth step_i sp 0 st1 instrs l st2 
      /\ (l <= length instrs)%nat.
forall (A : Type)
  (step_i : val -> istate -> A -> istate -> Prop)
  (sp : val) (instrs : list A) (st1 st2 : istate),
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l st2 /\
  (l <= Datatypes.length instrs)%nat
Proof.
forall (A : Type)
  (step_i : val -> istate -> A -> istate -> Prop)
  (sp : val) (instrs : list A) (st1 st2 : istate),
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l st2 /\
  (l <= Datatypes.length instrs)%nat
  induction instrs.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
forall st1 st2 : istate,
step_list step_i sp st1 nil st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 nil l st2 /\
  (l <= Datatypes.length nil)%nat
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
forall st1 st2 : istate,
step_list step_i sp st1 (a :: instrs) st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 (a :: instrs) l st2 /\
  (l <= Datatypes.length (a :: instrs))%nat
  -
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
forall st1 st2 : istate,
step_list step_i sp st1 nil st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 nil l st2 /\
  (l <= Datatypes.length nil)%nat cbn; intros.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
st1, st2: istate
H: step_list step_i sp st1 nil st2
exists l : nat,
  step_list_nth step_i sp 0 st1 nil l st2 /\
  (l <= 0)%nat inv H.
  -
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
forall st1 st2 : istate,
step_list step_i sp st1 (a :: instrs) st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 (a :: instrs) l st2 /\
  (l <= Datatypes.length (a :: instrs))%nat cbn; intros.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
st1, st2: istate
H: step_list step_i sp st1 (a :: instrs) st2
exists l : nat,
  step_list_nth step_i sp 0 st1 (a :: instrs) l st2 /\
  (l <= S (Datatypes.length instrs))%nat inv H.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
state, state', state'': instr_state
cf: cf_instr
H4: step_i sp (Iexec state) a (Iexec state')
H6: step_list step_i sp (Iexec state') instrs
  (Iterm state'' cf)
exists l : nat,
  step_list_nth step_i sp 0 
    (Iexec state) (a :: instrs) l 
    (Iterm state'' cf) /\
  (l <= S (Datatypes.length instrs))%nat
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
state, state': instr_state
cf: cf_instr
H5: step_i sp (Iexec state) a (Iterm state' cf)
exists l : nat,
  step_list_nth step_i sp 0 
    (Iexec state) (a :: instrs) l 
    (Iterm state' cf) /\
  (l <= S (Datatypes.length instrs))%nat
    +
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
state, state', state'': instr_state
cf: cf_instr
H4: step_i sp (Iexec state) a (Iexec state')
H6: step_list step_i sp (Iexec state') instrs
  (Iterm state'' cf)
exists l : nat,
  step_list_nth step_i sp 0 
    (Iexec state) (a :: instrs) l 
    (Iterm state'' cf) /\
  (l <= S (Datatypes.length instrs))%nat exploit IHinstrs.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
state, state', state'': instr_state
cf: cf_instr
H4: step_i sp (Iexec state) a (Iexec state')
H6: step_list step_i sp (Iexec state') instrs
  (Iterm state'' cf)
step_list step_i sp ?Goal0 instrs ?Goal1
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
state, state', state'': instr_state
cf: cf_instr
H4: step_i sp (Iexec state) a (Iexec state')
H6: step_list step_i sp (Iexec state') instrs
  (Iterm state'' cf)
(exists l : nat,
   step_list_nth step_i sp 0 ?Goal0 instrs l ?Goal1 /\
   (l <= Datatypes.length instrs)%nat) ->
exists l : nat,
  step_list_nth step_i sp 0 
    (Iexec state) (a :: instrs) l 
    (Iterm state'' cf) /\
  (l <= S (Datatypes.length instrs))%nat eauto.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
state, state', state'': instr_state
cf: cf_instr
H4: step_i sp (Iexec state) a (Iexec state')
H6: step_list step_i sp (Iexec state') instrs
  (Iterm state'' cf)
(exists l : nat,
   step_list_nth step_i sp 0 
     (Iexec state') instrs l 
     (Iterm state'' cf) /\
   (l <= Datatypes.length instrs)%nat) ->
exists l : nat,
  step_list_nth step_i sp 0 
    (Iexec state) (a :: instrs) l 
    (Iterm state'' cf) /\
  (l <= S (Datatypes.length instrs))%nat simplify.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
state, state', state'': instr_state
cf: cf_instr
H4: step_i sp (Iexec state) a (Iexec state')
H6: step_list step_i sp (Iexec state') instrs
  (Iterm state'' cf)
x: nat
H: step_list_nth step_i sp 0 
  (Iexec state') instrs x 
  (Iterm state'' cf)
H1: (x <= Datatypes.length instrs)%nat
exists l : nat,
  step_list_nth step_i sp 0 
    (Iexec state) (a :: instrs) l 
    (Iterm state'' cf) /\
  (l <= S (Datatypes.length instrs))%nat
      exists (S x).
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
state, state', state'': instr_state
cf: cf_instr
H4: step_i sp (Iexec state) a (Iexec state')
H6: step_list step_i sp (Iexec state') instrs
  (Iterm state'' cf)
x: nat
H: step_list_nth step_i sp 0 
  (Iexec state') instrs x 
  (Iterm state'' cf)
H1: (x <= Datatypes.length instrs)%nat
step_list_nth step_i sp 0 
  (Iexec state) (a :: instrs) 
  (S x) (Iterm state'' cf) /\
(S x <= S (Datatypes.length instrs))%nat split; [|lia].
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
state, state', state'': instr_state
cf: cf_instr
H4: step_i sp (Iexec state) a (Iexec state')
H6: step_list step_i sp (Iexec state') instrs
  (Iterm state'' cf)
x: nat
H: step_list_nth step_i sp 0 
  (Iexec state') instrs x 
  (Iterm state'' cf)
H1: (x <= Datatypes.length instrs)%nat
step_list_nth step_i sp 0 
  (Iexec state) (a :: instrs) 
  (S x) (Iterm state'' cf)
      eapply step_list_nth_cons; eauto.
    +
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
state, state': instr_state
cf: cf_instr
H5: step_i sp (Iexec state) a (Iterm state' cf)
exists l : nat,
  step_list_nth step_i sp 0 
    (Iexec state) (a :: instrs) l 
    (Iterm state' cf) /\
  (l <= S (Datatypes.length instrs))%nat exists 1%nat.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
state, state': instr_state
cf: cf_instr
H5: step_i sp (Iexec state) a (Iterm state' cf)
step_list_nth step_i sp 0 
  (Iexec state) (a :: instrs) 1 
  (Iterm state' cf) /\
(1 <= S (Datatypes.length instrs))%nat split; [|lia].
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
state, state': instr_state
cf: cf_instr
H5: step_i sp (Iexec state) a (Iterm state' cf)
step_list_nth step_i sp 0 
  (Iexec state) (a :: instrs) 1 
  (Iterm state' cf)
      econstructor; cbn; eauto.
A: Type
step_i: val -> istate -> A -> istate -> Prop
sp: val
a: A
instrs: list A
IHinstrs: forall st1 st2 : istate,
step_list step_i sp st1 instrs st2 ->
exists l : nat,
  step_list_nth step_i sp 0 st1 instrs l
    st2 /\
  (l <= Datatypes.length instrs)%nat
state, state': instr_state
cf: cf_instr
H5: step_i sp (Iexec state) a (Iterm state' cf)
step_list_nth step_i sp 1 
  (Iterm state' cf) (a :: instrs) 1 
  (Iterm state' cf) constructor.
Qed.

Inductive step_list2 {A} (step_i: val -> istate -> A -> istate -> Prop):
  val -> istate -> list A -> istate -> Prop :=
| exec_RBcons2 :
  forall i0 i1 i2 i instrs sp,
    step_i sp i0 i i1 ->
    step_list2 step_i sp i1 instrs i2 ->
    step_list2 step_i sp i0 (i :: instrs) i2
| exec_RBnil2 :
  forall sp i, step_list2 step_i sp i nil i.

Inductive step_list_inter {A} (step_i: val -> istate -> A -> istate -> Prop):
  val -> istate -> list A -> istate -> Prop :=
| exec_term_RBcons :
  forall i0 i1 i2 i instrs sp,
    step_i sp (Iexec i0) i i1 ->
    step_list_inter step_i sp i1 instrs i2 ->
    step_list_inter step_i sp (Iexec i0) (i :: instrs) i2
| exec_term_RBnil :
  forall sp i, step_list_inter step_i sp i nil i
| exec_term_RBcons_term :
  forall i cf l sp,
    step_list_inter step_i sp (Iterm i cf) l (Iterm i cf).

Inductive step_list_inter_strict {A} (step_i: val -> istate -> A -> istate -> Prop):
  val -> istate -> list A -> istate -> Prop :=
| exec_term_strict_RBcons :
  forall i0 i1 i2 i instrs sp,
    step_i sp (Iexec i0) i i1 ->
    step_list_inter_strict step_i sp i1 instrs i2 ->
    step_list_inter_strict step_i sp (Iexec i0) (i :: instrs) i2
| exec_term_strict_RBnil :
  forall sp i, step_list_inter_strict step_i sp i nil i
| exec_term_strict_RBcons_term :
  forall i cf instr instrs sp,
    step_i sp (Iexec i) instr (Iexec i) ->
    step_list_inter_strict step_i sp (Iexec i) instrs (Iexec i) ->
    step_list_inter_strict step_i sp (Iterm i cf) (instr :: instrs) (Iterm i cf).

Top-Level Type Definitions

Module Type BlockType.

  Parameter t: Type.
  Parameter foldl : forall A, (A -> instr -> A) -> t -> A -> A.
  Parameter length : t -> nat.
  Parameter step: forall A B, Genv.t A B -> val -> istate -> t -> istate -> Prop.

  Arguments step [A B].
  Arguments foldl [A].

End BlockType.

Module Gible(B : BlockType).

  Definition code: Type := PTree.t B.t.

  Record function: Type := mkfunction {
                              fn_sig: signature;
                              fn_params: list reg;
                              fn_stacksize: Z;
                              fn_code: code;
                              fn_entrypoint: node
                            }.

  Definition fundef := AST.fundef function.

  Definition program := AST.program fundef unit.

  Definition funsig (fd: fundef) :=
    match fd with
    | Internal f => fn_sig f
    | External ef => ef_sig ef
    end.

  Inductive stackframe : Type :=
  | Stackframe:
    forall (res: reg)            (**r where to store the result *)
           (f: function)         (**r calling function *)
           (sp: val)             (**r stack pointer in calling function *)
           (pc: node)            (**r program point in calling function *)
           (rs: regset)          (**r register state in calling function *)
           (pr: predset),        (**r predicate state of the calling
                                        function *)
      stackframe.

State Definition

The definition of state is normal now, and is directly the same as in other intermediate languages. The main difference in the execution of the semantics, though is that executing basic blocks uses big-step semantics.

  Variant state : Type :=
    | State:
      forall (stack: list stackframe) (**r call stack *)
             (f: function)            (**r current function *)
             (sp: val)                (**r stack pointer *)
             (pc: node)               (**r current program point in [c] *)
             (rs: regset)             (**r register state *)
             (pr: predset)            (**r predicate register state *)
             (m: mem),                (**r memory state *)
        state
    | Callstate:
      forall (stack: list stackframe) (**r call stack *)
             (f: fundef)              (**r function to call *)
             (args: list val)         (**r arguments to the call *)
             (m: mem),                (**r memory state *)
        state
    | Returnstate:
      forall (stack: list stackframe) (**r call stack *)
             (v: val)                 (**r return value for the call *)
             (m: mem),                (**r memory state *)
        state.

Old version of state

The definition of state used to be a bit strange when compared to other state definitions in CompCert. The main reason for that is the inclusion of list bblock_body, even though theoretically this is not necessary as one can use the program counter pc to index the current function and find the whole basic block that needs to be executed.

However, the state definition needs to be viable for a translation from RTL into RTLBlock, as well as larger grained optimisations such as scheduling. The proof of semantic correctness of the first translation requires that the instructions are executed one after another. As it is not possible to perform multiple steps in the input language for one step in the output language, without showing that the state is reduced by some measure, the current basic block needs to be present inside of the state.

The ideal solution to this would be to have two indices, one which finds the current basic block to execute, and another which keeps track of the offset. This would make the basic block generation proof much simpler, because there is a direct correlation between the program counter in RTL and the program counter in addition to the offset in RTLBlock.

On the other hand, the best solution for proving scheduling correct would be a pure big step style semantics for executing the basic block. This would not need to include anything relating to the basic block in the state, as it would execute each basic block at a time. Referring to each instruction individually becomes impossible then, because the state transition skips over it directly.

Finally, the way the state is actually implemented is using a mixture of the two methods above. Instead of having two indices, the internal index is instead a list of remaining instructions to executed in the current block. In case of transformations that need to reason about each instruction individually, the list of instructions will be reduced one instruction at a time. However, in the case of transformations that only need to reason about basic blocks at a time will only use the fact that one can transform a list of instructions into a next state transition (JumpState).

Semantics

  Section RELSEM.

    Definition genv := Genv.t fundef unit.

    Context (ge: genv).

    Definition find_function
               (ros: reg + ident) (rs: regset) : option fundef :=
      match ros with
      | inl r => Genv.find_funct ge rs#r
      | inr symb =>
          match Genv.find_symbol ge symb with
          | None => None
          | Some b => Genv.find_funct_ptr ge b
          end
      end.

Step Control-Flow Instruction

These control-flow instruction semantics are essentially the same as in RTL, with the addition of a recursive conditional instruction, which is used to support if-conversion.

    Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop :=
    | exec_RBcall:
      forall s f sp rs m res fd ros sig args pc pc' pr,
        find_function ros rs = Some fd ->
        funsig fd = sig ->
        step_cf_instr
          (State s f sp pc rs pr m) (RBcall sig ros args res pc')
          E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m)
    | exec_RBtailcall:
      forall s f stk rs m sig ros args fd m' pc pr,
        find_function ros rs = Some fd ->
        funsig fd = sig ->
        Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
        step_cf_instr
          (State s f (Vptr stk Ptrofs.zero) pc rs pr m)
          (RBtailcall sig ros args)
          E0 (Callstate s fd rs##args m')
    | exec_RBbuiltin:
      forall s f sp rs m ef args res pc' vargs t vres m' pc pr,
        eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
        external_call ef ge vargs m t vres m' ->
        step_cf_instr
          (State s f sp pc rs pr m) (RBbuiltin ef args res pc')
          t (State s f sp pc' (regmap_setres res vres rs) pr m')
    | exec_RBcond:
      forall s f sp rs m cond args ifso ifnot b pc pc' pr,
        eval_condition cond rs##args m = Some b ->
        pc' = (if b then ifso else ifnot) ->
        step_cf_instr
          (State s f sp pc rs pr m)
          (RBcond cond args ifso ifnot)
          E0 (State s f sp pc' rs pr m)
    | exec_RBjumptable:
      forall s f sp rs m arg tbl n pc pc' pr,
        rs#arg = Vint n ->
        list_nth_z tbl (Int.unsigned n) = Some pc' ->
        step_cf_instr
          (State s f sp pc rs pr m)
          (RBjumptable arg tbl)
          E0 (State s f sp pc' rs pr m)
    | exec_RBreturn:
      forall s f stk rs m or pc m' pr,
        Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
        step_cf_instr
          (State s f (Vptr stk Ptrofs.zero) pc rs pr m)
          (RBreturn or)
          E0 (Returnstate s (regmap_optget or Vundef rs) m')
    | exec_RBgoto:
      forall s f sp pc rs pr m pc',
        step_cf_instr (State s f sp pc rs pr m)
                      (RBgoto pc') E0 (State s f sp pc' rs pr m).

    Lemma step_cf_instr_det :
      forall st cf t st1 st2,
        step_cf_instr st cf t st1 ->
        step_cf_instr st cf t st2 ->
        st1 = st2.
ge: genv
forall (st : state) (cf : cf_instr) (t : trace)
  (st1 st2 : state),
step_cf_instr st cf t st1 ->
step_cf_instr st cf t st2 -> st1 = st2
    Proof using.
ge: genv
forall (st : state) (cf : cf_instr) (t : trace)
  (st1 st2 : state),
step_cf_instr st cf t st1 ->
step_cf_instr st cf t st2 -> st1 = st2
      inversion 1; subst; simplify; clear H;
        match goal with H: context[step_cf_instr] |- _ => inv H end; crush;
        assert (vargs0 = vargs) by eauto using eval_builtin_args_determ; subst;
        assert (vres = vres0 /\ m' = m'0) by eauto using external_call_deterministic; crush.
    Qed.

Top-level step

The step function itself then uses this big step of the list of instructions to then show a transition from basic block to basic block. The one particular aspect of this is that the basic block is also part of the state, which has to be correctly set during the execution of the function. Function calls and function returns then also need to set the basic block properly. This means that the basic block of the returning function also needs to be stored in the stackframe, as that is the only assumption one can make when returning from a function.

    Variant step: state -> trace -> state -> Prop :=
      | exec_bblock:
        forall s f sp pc rs rs' m m' bb pr pr' t state cf,
          f.(fn_code) ! pc = Some bb ->
          B.step ge sp (Iexec (mk_instr_state rs pr m)) bb (Iterm (mk_instr_state rs' pr' m') cf) ->
          step_cf_instr (State s f sp pc rs' pr' m') cf t state ->
          step (State s f sp pc rs pr m) t state
      | exec_function_internal:
        forall s f args m m' stk,
          Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
          step (Callstate s (Internal f) args m)
               E0 (State s f
                         (Vptr stk Ptrofs.zero)
                         f.(fn_entrypoint)
                         (init_regs args f.(fn_params))
                         (PMap.init false)
                         m')
      | exec_function_external:
        forall s ef args res t m m',
          external_call ef ge args m t res m' ->
          step (Callstate s (External ef) args m)
               t (Returnstate s res m')
      | exec_return:
        forall res f sp pc rs s vres m pr,
          step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m)
               E0 (State s f sp pc (rs#res <- vres) pr m).

  End RELSEM.

  Inductive initial_state (p: program): state -> Prop :=
  | initial_state_intro: forall b f m0,
      let ge := Genv.globalenv p in
      Genv.init_mem p = Some m0 ->
      Genv.find_symbol ge p.(prog_main) = Some b ->
      Genv.find_funct_ptr ge b = Some f ->
      funsig f = signature_main ->
      initial_state p (Callstate nil f nil m0).

  Inductive final_state: state -> int -> Prop :=
  | final_state_intro: forall r m,
      final_state (Returnstate nil (Vint r) m) r.

Semantics

We first describe the semantics by assuming a global program environment with type ~genv~ which was declared earlier.

  Definition semantics (p: program) :=
    Semantics step (initial_state p) final_state (Genv.globalenv p).

  Definition max_reg_block (m: positive) (n: node) (i: B.t) := B.foldl max_reg_instr i m.

  Definition max_pred_block (m: positive) (n: node) (i: B.t) := B.foldl max_pred_instr i m.

  Definition max_reg_function (f: function) :=
    Pos.max
      (PTree.fold max_reg_block f.(fn_code) 1%positive)
      (fold_left Pos.max f.(fn_params) 1%positive).

  Definition max_pred_function (f: function) :=
    PTree.fold max_pred_block f.(fn_code) 1%positive.

  Definition max_pc_function (f: function) : positive :=
    PTree.fold
      (fun m pc i =>
         (Pos.max m
                  (pc + match Z.of_nat (B.length i)
                        with Z.pos p => p | _ => 1 end))%positive)
      f.(fn_code) 1%positive.

  Definition all_successors (b: B.t) : list node :=
    B.foldl (fun ns i =>
               match i with
               | RBexit _ cf => successors_instr cf ++ ns
               | _ => ns
               end
            ) b nil.

    Definition pred_uses i :=
      match i with
      | RBop (Some p) _ _ _
      | RBload (Some p) _ _ _ _
      | RBstore (Some p) _ _ _ _
      | RBexit (Some p) _ => predicate_use p
      | RBsetpred (Some p) _ _ p' => p' :: predicate_use p
      | RBsetpred None _ _ p' => p' :: nil
      | _ => nil
      end.

End Gible.