From Coq Require Export
  Arith.PeanoNat
  ZArith
  Lia
  Lists.List
  Strings.String.

From ExtLib Require Export
  Data.List
  Data.String
  Data.Map.FMapAList
  Structures.Maps
  Core.RelDec.

From HyPre Require Export MultiStep Semantics.

Definition var : Set := string.

Definition value : Type := Z.

Definition varmap := alist var value.
Definition heap := alist value value.

(*required for alist*)
Definition decZ : @RelDec value (eq) := RelDec_from_dec eq Z.eq_dec.

Inductive expr : Type :=
  | Var (_ : var)
  | Lit (_ : value)
  | Plus (_ _ : expr)
  | Minus (_ _ : expr)
  | Mult (_ _ : expr)
  | Less (_ _ : expr)
  | Equal (_ _ : expr)
  | Not (_ : expr).

Definition dec_expr : forall (a b : expr), {a = b} + {a <> b}.
Proof.
  intros.
  induction a in b|-*; destruct b; try (now right).
  1: { destruct (string_eqdec v v0).
    + left. now rewrite e.
    + right. now inversion 1. }
  1: { destruct (Z.eq_dec v v0).
    + left. now rewrite e.
    + right. now inversion 1. }
  1-5: specialize (IHa1 b1); specialize (IHa2 b2); destruct IHa1, IHa2; try (right; now inversion 1); left; subst; reflexivity.
  1: { destruct (IHa b). left. now subst. right. now inversion 1. }
Defined.

Local Notation "i [[ x ]]" := (alist_find _ x i) (at level 40).

Inductive eval_expr: varmap -> expr -> value -> Prop
  := EVar x Gamma v : Gamma[[x]] = Some v -> eval_expr Gamma (Var x) v
  | EVarUnassigned x Gamma : Gamma[[x]] = None -> eval_expr Gamma (Var x) 0%Z
  | ELit v Gamma : eval_expr Gamma (Lit v) v
  | EPlus e1 e2 Gamma v1 v2 : eval_expr Gamma e1 v1 -> eval_expr Gamma e2 v2 -> eval_expr Gamma (Plus e1 e2) (v1+v2)%Z
  | EMinus e1 e2 Gamma v1 v2 : eval_expr Gamma e1 v1 -> eval_expr Gamma e2 v2 -> eval_expr Gamma (Minus e1 e2) (v1-v2)%Z
  | EMult e1 e2 Gamma v1 v2 : eval_expr Gamma e1 v1 -> eval_expr Gamma e2 v2 -> eval_expr Gamma (Mult e1 e2) (v1*v2)%Z
  | ELessTrue e1 e2 Gamma v1 v2 : eval_expr Gamma e1 v1 -> eval_expr Gamma e2 v2 -> (v1 < v2)%Z -> eval_expr Gamma (Less e1 e2) (1%Z)
  | ELessFalse e1 e2 Gamma v1 v2 : eval_expr Gamma e1 v1 -> eval_expr Gamma e2 v2 -> not (v1 < v2)%Z -> eval_expr Gamma (Less e1 e2) (0%Z)
  | EEqualTrue e1 e2 Gamma v1 v2 : eval_expr Gamma e1 v1 -> eval_expr Gamma e2 v2 -> v1 = v2 -> eval_expr Gamma (Equal e1 e2) (1%Z)
  | EEqualFalse e1 e2 Gamma v1 v2 : eval_expr Gamma e1 v1 -> eval_expr Gamma e2 v2 -> not (v1 = v2) -> eval_expr Gamma (Equal e1 e2) (0%Z)
  | ENotTrue e Gamma v : eval_expr Gamma e v -> v = 0%Z -> eval_expr Gamma (Not e) (1%Z)
  | ENotFalse e Gamma v : eval_expr Gamma e v -> not (v = 0%Z) -> eval_expr Gamma (Not e) (0%Z).

Lemma eval_expr_complete e Gamma:
  { v | eval_expr Gamma e v }.
Proof.
  induction e; try destruct IHe1 as [v1 Hv1]; try destruct IHe2 as [v2 Hv2].
  - destruct (Gamma[[v]]) eqn:H.
    + exists v0. now constructor.
    + exists 0%Z. now constructor.
  - exists v. now constructor.
  - exists (v1+v2)%Z. now constructor.
  - exists (v1-v2)%Z. now constructor.
  - exists (v1*v2)%Z. now constructor.
  - assert ((v1 < v2)%Z + not (v1 < v2)%Z) as [H | H]. { destruct (Z_lt_dec v1 v2). now left. now right. }
    + exists 1%Z. now eapply (ELessTrue _ _ _ v1 v2).
    + exists 0%Z. now eapply (ELessFalse _ _ _ v1 v2).
  - assert ({v1 = v2} + {v1 <> v2}) as [H | H] by now apply (Z.eq_dec v1 v2).
    + exists 1%Z. now eapply (EEqualTrue _ _ _ v1 v2).
    + exists 0%Z. now eapply (EEqualFalse _ _ _ v1 v2).
  - destruct IHe as [v Hv].
    assert ({v = 0%Z} + {v <> 0%Z}) as [H | H] by now apply (Z.eq_dec v 0).
    + exists 1%Z. now eapply (ENotTrue _ _ v).
    + exists 0%Z. now eapply (ENotFalse _ _ v).
Defined.

Lemma eval_expr_det e Gamma v1 v2:
  eval_expr Gamma e v1 -> eval_expr Gamma e v2 -> v1 = v2.
Proof.
  revert v1 v2.
  induction e; intros v1 v2 d1 d2.
  - inversion d1; inversion d2; subst; rewrite H5 in H1; try congruence.
  - inversion d1; inversion d2; now subst.
  - inversion d1; inversion d2; subst.
    specialize (IHe1 v0 v4 H2 H8).
    specialize (IHe2 v3 v5 H4 H10). now subst.
  - inversion d1; inversion d2; subst.
    specialize (IHe1 v0 v4 H2 H8).
    specialize (IHe2 v3 v5 H4 H10). now subst.
  - inversion d1; inversion d2; subst.
    specialize (IHe1 v0 v4 H2 H8).
    specialize (IHe2 v3 v5 H4 H10). now subst.
  - inversion d1; inversion d2; subst; try reflexivity.
    all: specialize (IHe1 v0 v4 H1 H8); subst.
    all: specialize (IHe2 v3 v5 H3 H10); subst.
    all: contradiction.
  - inversion d1; inversion d2; subst; try reflexivity.
    all: specialize (IHe1 _ _ H1 H8); subst.
    all: specialize (IHe2 _ _ H3 H10); subst.
    all: contradiction.
  - inversion d1; inversion d2; subst; try reflexivity.
    all: specialize (IHe _ _ H0 H5); subst; contradiction.
Qed.

Definition eval_expr_fun e V : value := match (eval_expr_complete e V) with exist _ v P => v end.

Lemma eval_expr_agree e V:
  eval_expr V e (eval_expr_fun e V).
Proof.
  unfold eval_expr_fun.
  now destruct (eval_expr_complete e V).
Qed.

Hint Immediate eval_expr_agree : core.

Ltac expr_det := repeat multimatch goal with
                        | H1 : context [ eval_expr_fun ?e ?V ] |- _ => lazymatch goal with
                                                                       | _ : eval_expr V e (eval_expr_fun e V) |- _ => fail
                                                                       | _ => pose proof (eval_expr_agree e V)
                                                                       end
                        | |- context [ eval_expr_fun ?e ?V ] => lazymatch goal with
                                                                | _ : eval_expr V e (eval_expr_fun e V) |- _ => fail
                                                                | _ => pose proof (eval_expr_agree e V)
                                                                end
                        end;
                        repeat multimatch goal with
                               | H1 : eval_expr ?V ?e ?a, H2 : eval_expr ?V ?e ?b |- _ => lazymatch goal with
                                                                                          | H : a = b |- _ => fail
                                                                                          | H : b = a |- _ => fail
                                                                                          | _ => pose proof (eval_expr_det _ _ _ _ H1 H2)
                                                                                          end
                               end.

Inductive stmt : Type :=
  | Assign (x : var) (e : expr)
  | Read (x : var) (a : expr)
  | Write (x : var) (a : expr)
  | If (c : expr) (s1 s2 : list stmt)
  | While (c : expr) (s1 s2 : list stmt)
  | Skip
  | Fence.

Fixpoint stmt_depth (s : stmt) : nat
  := let f := fix aux (sl : list stmt)
         := match sl with
            | x :: xs => S (stmt_depth x) + aux xs
            | nil => 0
            end in
     match s with
     | If _ s1 s2 => S (Nat.max (f s1) (f s2))
     | While _ s1 s2 => S (Nat.max (f s1) (f s2))
     | _ => 0
     end.

Fixpoint stmt_depth_list (sl : list stmt) : nat
  := match sl with
     | x :: xs => S (stmt_depth x) + stmt_depth_list xs
     | nil => 0
     end.

Lemma stmt_depth_list_app a b:
  stmt_depth_list (a ++ b) = stmt_depth_list a + stmt_depth_list b.
Proof.
  induction a.
  - reflexivity.
  - rewrite <- app_comm_cons. simpl.
    rewrite IHa. lia.
Qed.

Lemma stmt_depth_S x xs n: stmt_depth_list (x :: xs) < S n -> stmt_depth_list xs < n.
Proof.
  simpl. lia.
Qed.

Lemma string_dec (x y : string): {x = y} + {x <> y}.
Proof.
  destruct (string_eqdec x y). now left. now right.
Qed.

Lemma prog_dec' (x y: list stmt) n:
  stmt_depth_list x < n ->
  stmt_depth_list y < n ->
  {x = y} + {x <> y}.
Proof.
  induction n in x, y |-*.
  - intros. lia.
  - intros.
    destruct x, y. 1: now left. 1,2: now right.
    destruct (IHn x y). 1: eapply stmt_depth_S; exact H. 1: eapply stmt_depth_S; exact H0.
    2: right; inversion 1; congruence.
    subst.
    assert ({s = s0} + {s <> s0}). (* equality for statements, Inlined, as it needs the induction hypothesis*)
    + destruct s, s0; try (right; congruence); try now left.
      * destruct (string_dec x x0). 2: right; inversion 1; congruence.
        destruct (dec_expr e e0). 2: right; inversion 1; congruence.
        subst. now left.
      * destruct (string_dec x x0). 2: right; inversion 1; congruence.
        destruct (dec_expr a a0). 2: right; inversion 1; congruence.
        subst. now left.
      * destruct (string_dec x x0). 2: right; inversion 1; congruence.
        destruct (dec_expr a a0). 2: right; inversion 1; congruence.
        subst. now left.
      * (*equality decider for If needs equality decider for programs*)
        destruct (dec_expr c c0). 2: right; inversion 1; congruence. subst.
        destruct (IHn s1 s0). 4: right; inversion 1; congruence.
        { simpl in H, H0.
          replace ((fix aux (sl : list stmt) : nat :=
                   match sl with
                   | nil => 0
                   | x :: xs => S (stmt_depth x + aux xs)
                   end)) with (stmt_depth_list) in H , H0 by reflexivity.
          lia.
        }
        { simpl in H, H0.
          replace ((fix aux (sl : list stmt) : nat :=
                   match sl with
                   | nil => 0
                   | x :: xs => S (stmt_depth x + aux xs)
                   end)) with (stmt_depth_list) in H , H0 by reflexivity.
          lia.
        }
        subst.
        destruct (IHn s2 s3). 4: right; inversion 1; congruence.
        { simpl in H, H0.
          replace ((fix aux (sl : list stmt) : nat :=
                   match sl with
                   | nil => 0
                   | x :: xs => S (stmt_depth x + aux xs)
                   end)) with (stmt_depth_list) in H , H0 by reflexivity.
          lia.
        }
        { simpl in H, H0.
          replace ((fix aux (sl : list stmt) : nat :=
                   match sl with
                   | nil => 0
                   | x :: xs => S (stmt_depth x + aux xs)
                   end)) with (stmt_depth_list) in H , H0 by reflexivity.
          lia.
        }
        subst. now left.
      * (*exactly the same as for If*)
        destruct (dec_expr c c0). 2: right; inversion 1; congruence. subst.
        destruct (IHn s1 s0). 4: right; inversion 1; congruence.
        { simpl in H, H0.
          replace ((fix aux (sl : list stmt) : nat :=
                   match sl with
                   | nil => 0
                   | x :: xs => S (stmt_depth x + aux xs)
                   end)) with (stmt_depth_list) in H , H0 by reflexivity.
          lia.
        }
        { simpl in H, H0.
          replace ((fix aux (sl : list stmt) : nat :=
                   match sl with
                   | nil => 0
                   | x :: xs => S (stmt_depth x + aux xs)
                   end)) with (stmt_depth_list) in H , H0 by reflexivity.
          lia.
        }
        subst.
        destruct (IHn s2 s3). 4: right; inversion 1; congruence.
        { simpl in H, H0.
          replace ((fix aux (sl : list stmt) : nat :=
                   match sl with
                   | nil => 0
                   | x :: xs => S (stmt_depth x + aux xs)
                   end)) with (stmt_depth_list) in H , H0 by reflexivity.
          lia.
        }
        { simpl in H, H0.
          replace ((fix aux (sl : list stmt) : nat :=
                   match sl with
                   | nil => 0
                   | x :: xs => S (stmt_depth x + aux xs)
                   end)) with (stmt_depth_list) in H , H0 by reflexivity.
          lia.
        }
        subst. now left.

    + destruct H1. subst. now left. right. inversion 1. congruence.
Qed.

Lemma prog_dec (x y : list stmt): {x = y} + {x <> y}.
Proof.
  eapply (prog_dec' x y (S (Nat.max (stmt_depth_list x) (stmt_depth_list y)))).
  all: lia.
Qed.

Definition state : Type := (varmap * heap * list stmt).

Lemma state_dec (x y : state): {x = y} + {x <> y}.
Proof.
  destruct x as [ [V H] p].
  destruct y as [ [V' H'] p'].
  assert ({V = V'} + {V <> V'}). (* equality of the underlying lists, *not* equivalence of the maps!*)
  (*This is fine, however, as this decider is only needed to determine if a state is exactly equal to the one that would be produced by the semantics, which fixes the order of operations. We do not care about states obtained in other ways where the mapping would be equivalent*)
  {
    induction V in V' |-*; destruct V'. 1: now left. 1,2: now right.
    destruct (IHV V').
    + assert ({a = p0} + {a <> p0}).
      * destruct a as [ak av]. destruct p0 as [pk pv].
        destruct (string_dec ak pk). 2: right; inversion 1; congruence.
        destruct (Z.eq_dec av pv). 2: right; inversion 1; congruence.
        subst. now left.
      * destruct H0.
        subst. now left.
        right. inversion 1. congruence.
    + right. inversion 1. congruence.
  }
  assert ({H = H'} + {H <> H'}). (*again, equality of the underlying lists, not equivalence.*)
  {
    induction H in H' |-*; destruct H'. 2,3: now right. 1: now left.
    destruct (IHlist H'). 2: right; inversion 1; congruence.
    assert ({a = p0} + {a <> p0}).
    - destruct a as [ak av]. destruct p0 as [pk pv].
      destruct (Z.eq_dec ak pk). 2: right; inversion 1; congruence.
      destruct (Z.eq_dec av pv). 2: right; inversion 1; congruence.
      subst. now left.
    - destruct H1. 2: right; inversion 1; congruence.
      subst. now left.
  }
  destruct H0. 2: right; inversion 1; congruence.
  destruct H1. 2: right; inversion 1; congruence.
  destruct (prog_dec p p'). 2: right; inversion 1; congruence.
  subst. now left.
Qed.

Inductive smallstep_nonspec:
  state -> state -> Prop
  := NSkip V H l: smallstep_nonspec (V, H, Skip :: l) (V, H, l)
  | NFence V H l: smallstep_nonspec (V, H, Fence :: l) (V, H, l)
  | NAssign V H x e v l: eval_expr V e v -> smallstep_nonspec(V, H, (Assign x e) :: l) ((alist_add _ x v V), H, l)
  | NRead V H x e a v l: eval_expr V e a -> alist_find decZ a H = Some v -> smallstep_nonspec(V, H, (Read x e) :: l) ((alist_add _ x v V), H, l)
  | NReadUninitialized V H x e a l: eval_expr V e a -> alist_find decZ a H = None -> smallstep_nonspec(V, H, (Read x e) :: l) ((alist_add _ x 0%Z V), H, l)
  | NWrite V H x e a v l: eval_expr V e a -> alist_find _ x V = Some v -> smallstep_nonspec(V, H, (Write x e) :: l) (V, (alist_add decZ a v H), l)
  | NWriteUndefined V H x e a l: eval_expr V e a -> alist_find _ x V = None -> smallstep_nonspec(V, H, (Write x e) :: l) (V, (alist_add decZ a 0%Z H), l)
  | NIfTrue V H e v s1 s2 l: eval_expr V e v -> v <> 0%Z -> smallstep_nonspec (V, H, (If e s1 s2) :: l) (V, H, s1 ++ l)
  | NIfFalse V H e v s1 s2 l: eval_expr V e v -> v = 0%Z -> smallstep_nonspec (V, H, (If e s1 s2) :: l) (V, H, s2 ++ l)
  | NWhile V H e s1 s2 l: smallstep_nonspec (V, H, (While e s1 s2) :: l) (V, H, (If e (s1 :r: (While e s1 s2)) s2) :: l)
  | NTerm V H: smallstep_nonspec (V, H, nil) (V, H, nil).

Lemma smallstep_nonspec_det V H s r1 r2:
  smallstep_nonspec (V, H, s) r1 -> smallstep_nonspec (V, H, s) r2 -> r1 = r2.
Proof.
  intros H1 H2.
  destruct s.
  - inversion H1. inversion H2. subst. reflexivity.
  - destruct s; inversion H1; inversion H2; subst; expr_det; subst; congruence.
Qed.

Definition nonspec_step_fun (s : state) := match s with
                                           | (V, H, nil) => (V, H, nil)
                                           | (V, H, s :: l) => match s with
                                                               | Skip => (V, H, l)
                                                               | Fence => (V, H, l)
                                                               | Assign x e => (alist_add _ x (eval_expr_fun e V) V, H, l)
                                                               | Read x a => match (alist_find decZ (eval_expr_fun a V) H) with
                                                                             | Some v => (alist_add _ x v V, H, l)
                                                                             | None => (alist_add _ x 0%Z V, H, l)
                                                                             end
                                                               | Write x a => let a' := eval_expr_fun a V in
                                                                   match (V[[x]]) with
                                                                   | Some v => (V, alist_add decZ a' v H, l)
                                                                   | None => (V, alist_add decZ a' 0%Z H, l)
                                                                   end
                                                               | If c s1 s2 => match (Z.eq_dec (eval_expr_fun c V) 0%Z) with
                                                                               | left _ => (V, H, s2 ++ l)
                                                                               | right _ => (V, H, s1 ++ l)
                                                                               end
                                                               | While c s1 s2 => (V, H, (If c (s1 :r: (While c s1 s2)) s2) :: l)
                                                               end
                                           end.

Lemma nonspec_step_agree (s : state) :
  smallstep_nonspec s (nonspec_step_fun s).
Proof.
  destruct s as [ [V H] s].
  destruct s.
  - simpl. constructor.
  - destruct s; simpl; try constructor.
    + now expr_det.
    + destruct (H [[ eval_expr_fun a V]]) eqn: Ha; expr_det.
      * eapply NRead; eauto.
      * eapply NReadUninitialized; eauto.
    + destruct (V [[ x ]]) eqn:Hv.
      * eapply NWrite. 2: eauto. apply eval_expr_agree.
      * eapply NWriteUndefined. 2: eauto. apply eval_expr_agree.
    + destruct (Z.eq_dec (eval_expr_fun c V) 0).
      * eapply NIfFalse. expr_det. eauto. eauto.
      * eapply NIfTrue. expr_det. eauto. eauto.
Qed.

Definition specstate : Type := (option nat * varmap * heap * list stmt).

Definition valid n := match n with Some v => v > 0 | None => True end.
Definition decr n := match n with Some v => Some (v - 1) | None => None end.
Definition zero_out (n: option nat) := match n with Some v => Some 0 | None => None end.
Definition wndw n := match n with Some v => Some (v - 1) | None => Some 16 end.

Inductive smallstep_spec_am:
  list specstate -> list specstate -> Prop
  := AMSkip n V H l t: valid n -> smallstep_spec_am ((n, V, H, Skip :: l) :: t) ((decr n, V, H, l) :: t)
  | AMFence n V H l t: valid n -> smallstep_spec_am ((n, V, H, Fence :: l) :: t) ((zero_out n, V, H, l) :: t)
  | AMAssign n V H x e v l t: valid n -> eval_expr V e v -> smallstep_spec_am ((n, V, H, (Assign x e) :: l) :: t) ((decr n, (alist_add _ x v V), H, l) :: t)
  | AMRead n V H x e a v l t: valid n -> eval_expr V e a -> alist_find decZ a H = Some v -> smallstep_spec_am ((n, V, H, (Read x e) :: l) :: t) ((decr n, (alist_add _ x v V), H, l) :: t)
  | AMReadUninitialized n V H x e a l t: valid n -> eval_expr V e a -> alist_find decZ a H = None -> smallstep_spec_am ((n, V, H, (Read x e) :: l) :: t) ((decr n, (alist_add _ x 0%Z V), H, l) :: t)
  | AMWrite n V H x e a v l t: valid n -> eval_expr V e a -> alist_find _ x V = Some v -> smallstep_spec_am ((n, V, H, (Write x e) :: l) :: t) ((decr n, V, (alist_add decZ a v H), l) :: t)
  | AMWriteUndefined n V H x e a l t: valid n -> eval_expr V e a -> alist_find _ x V = None -> smallstep_spec_am ((n, V, H, (Write x e) :: l) :: t) ((decr n, V, (alist_add decZ a 0%Z H), l) :: t)
  | AMIfTrue n V H b v s1 s2 l t: valid n -> eval_expr V b v -> v <> 0%Z -> smallstep_spec_am ((n, V, H, (If b s1 s2) :: l) :: t) ((wndw n, V, H, s2 ++ l) :: (decr n, V, H, s1 ++ l) :: t)
  | AMIfFalse n V H b v s1 s2 l t: valid n -> eval_expr V b v -> v = 0%Z -> smallstep_spec_am ((n, V, H, (If b s1 s2) :: l) :: t) ((wndw n, V, H, s1 ++ l) :: (decr n, V, H, s2 ++ l) :: t)
  | AMWhile n V H e s1 s2 l t: valid n -> smallstep_spec_am ((n, V, H, (While e s1 s2) :: l) :: t) ((decr n, V, H, (If e (s1 :r: (While e s1 s2)) s2 ) :: l) :: t)
  | AMRollback n V H l t: not (valid n) -> smallstep_spec_am ((n, V, H, l) :: t) t
  | AMRollbackT n n' V H t: n = Some (S n') -> smallstep_spec_am ((n, V, H, nil) :: t) t
  | AMTerm V H l: smallstep_spec_am ((None, V, H, nil) :: l) ((None, V, H, nil) :: l)
  | AMTerm': smallstep_spec_am nil nil.

Lemma list_cons_neq A (t: list A) (a: A):
  t <> a :: t.
Proof.
  revert a.
  induction t.
  - congruence.
  - intros b H.
    inversion H.
    now apply (IHt b).
Qed.

Hint Immediate list_cons_neq : core.

Lemma smallstep_spec_am_det t t1 t2:
  smallstep_spec_am t t1 -> smallstep_spec_am t t2 -> t1 = t2.
Proof.
  intros H1 H2.
  inversion H1; subst; inversion H2; subst; expr_det; try congruence.
  + simpl in H0. contradiction.
  + simpl in H9. contradiction.
Qed.

Definition spec_step_fun (sl : list specstate) : list specstate :=
  match sl with
  | nil => nil
  | (None, V, H, nil) :: t => (None, V, H, nil) :: t
  | (Some 0, V, H, s) :: t => t
  | (Some _, V, H, nil) :: t => t
  | (n, V, H, s :: l) :: t => match s with
                              | Skip => (decr n, V, H, l) :: t
                              | Fence => (zero_out n, V, H, l) :: t
                              | Assign x e => (decr n, alist_add _ x (eval_expr_fun e V) V, H, l) :: t
                              | Read x a => match (alist_find decZ (eval_expr_fun a V) H) with
                                            | Some v => (decr n, alist_add _ x v V, H, l) :: t
                                            | None => (decr n, alist_add _ x 0%Z V, H, l) :: t
                                            end
                              | Write x a => let a' := eval_expr_fun a V in
                                  match (V[[x]]) with
                                  | Some v => (decr n, V, alist_add decZ a' v H, l) :: t
                                  | None => (decr n, V, alist_add decZ a' 0%Z H, l) :: t
                                  end
                              | If c s1 s2 => match (Z.eq_dec (eval_expr_fun c V) 0%Z) with
                                              | left _ => (wndw n, V, H, s1 ++ l) :: (decr n, V, H, s2 ++ l) :: t
                                              | right _ => (wndw n, V, H, s2 ++ l) :: (decr n, V, H, s1 ++ l) :: t
                                              end
                              | While c s1 s2 => (decr n, V, H, (If c (s1 :r: (While c s1 s2)) s2) :: l) :: t
                              end
  end.

Lemma spec_step_agree sl :
  smallstep_spec_am sl (spec_step_fun sl).
Proof.
  destruct sl.
  - simpl. constructor.
  - destruct s as [ [ [n V] H] s].
    destruct s.
    + destruct n. destruct n.
      * now constructor.
      * now eapply AMRollbackT.
      * now eapply AMTerm.
    + destruct n. destruct n.
      * now constructor.
      * assert (valid (Some (S n))) as Hvalid by (unfold valid; lia).
        destruct s; simpl; try now econstructor.
        -- econstructor. unfold valid. lia. apply eval_expr_agree.
        -- expr_det. destruct (H [[eval_expr_fun a V]]) eqn:Ha; [eapply AMRead | eapply AMReadUninitialized]; eauto.
        -- expr_det. destruct (V [[x]]) eqn:Hv; [eapply AMWrite | eapply AMWriteUndefined]; eauto.
        -- expr_det. destruct (Z.eq_dec (eval_expr_fun c V) 0); [eapply AMIfFalse | eapply AMIfTrue]; eauto.
      * assert (valid None) by easy.
        destruct s; simpl; try now econstructor.
        -- econstructor. unfold valid. lia. apply eval_expr_agree.
        -- expr_det. destruct (H [[eval_expr_fun a V]]) eqn:Ha; [eapply AMRead | eapply AMReadUninitialized]; eauto.
        -- expr_det. destruct (V [[x]]) eqn:Hv; [eapply AMWrite | eapply AMWriteUndefined]; eauto.
        -- expr_det. destruct (Z.eq_dec (eval_expr_fun c V) 0); [eapply AMIfFalse | eapply AMIfTrue]; eauto.
Qed.

Definition multi_nonspec := multi_step' nonspec_step_fun.
Definition multi_spec_am := multi_step' spec_step_fun.

Definition nonspec_trace (s : list stmt) (H : heap) : list state -> Prop
  := fun sl => multi_nonspec (nil, H, s) (length sl) = sl.

Definition spec_am_trace (s : list stmt) (H : heap) : list (list specstate) -> Prop
  := fun sl => multi_spec_am ((None, nil, H, s)::nil) (length sl) = sl.

Lemma nonspec_trace_linear_semantics:
  forall p, rad_semantics (nonspec_trace p).
Proof.
  intros. unfold nonspec_trace.
  econstructor; intros.
  - unfold multi_nonspec. now cbn.
  - destruct sl.
    + exists (nil, i, p).
      unfold multi_nonspec. unfold multi_step'. easy.
    + exists (nonspec_step_fun s).
      rewrite length_cons. rewrite length_cons.
      unfold multi_nonspec, multi_step'.
      rewrite multi_step_S2.
      f_equal; eauto.
      unfold multi_step_hd.
      unfold multi_nonspec, multi_step' in H. cbn in H. rewrite H.
      reflexivity.
  - cbn in H0, H1. rewrite H0 in H1. now inversion H1.
  - destruct sl; cbn.
    easy.
    rewrite length_cons in H. rewrite length_cons in H.
    unfold multi_nonspec, multi_step' in H.
    rewrite multi_step_S2 in H.
    now inversion H.
Qed.

Lemma spec_am_trace_linear_semantics:
  forall p, rad_semantics (spec_am_trace p).
Proof.
  intros. unfold spec_am_trace.
  econstructor; intros.
  - now unfold multi_spec_am.
  - destruct sl.
    + eexists. unfold multi_spec_am, multi_step'. easy.
    + exists (spec_step_fun l).
      rewrite! length_cons.
      unfold multi_spec_am, multi_step'.
      rewrite multi_step_S2.
      f_equal; eauto.
      unfold multi_step_hd.
      unfold multi_spec_am, multi_step' in H. cbn in H. rewrite H.
      reflexivity.
  - cbn in H0, H1. rewrite H0 in H1. now inversion H1.
  - destruct sl; cbn.
    easy.
    rewrite! length_cons in H.
    unfold multi_spec_am, multi_step' in H.
    rewrite multi_step_S2 in H.
    now inversion H.
Qed.

Lemma multi_step'_S St (step : St -> St) (x : St) n:
  multi_step' step x (S n) = multi_step' step (step x) n :r: x.
Proof.
  unfold multi_step'.
  destruct n.
  - reflexivity.
  - now rewrite multi_step_S.
Qed.

Lemma multi_step_split {St} {step : St -> St} {s} {b a: list St}:
  multi_step' step s (|b ++ a|) = b ++ a ->
      multi_step' step (multi_step_hd step s (|a|)) (|b|) = b /\ multi_step' step s (|a|) = a.
Proof.
  unfold multi_step'.
  destruct b.
  - simpl. tauto.
  - rewrite <- app_comm_cons. rewrite! length_cons.
    destruct a.
    + unfold multi_step_hd. rewrite! app_nil_r. simpl. easy.
    + rewrite app_length. rewrite length_cons.
      assert (| b | + S (| a |) = S (| b |) + | a |) as -> by lia.
      rewrite multi_step_app.
      intros.
      rewrite multi_step_hd_step.
      enough (forall {a b c d : list St}, a ++ b = c ++ d /\ |a| = |c| -> a = c /\ b = d).
      * eapply H0. split. exact H. rewrite length_cons. rewrite multi_step_len. easy.
      * clear.
        induction a; destruct 1; destruct c.
        -- easy.
        -- rewrite length_cons in H0. simpl in H0. congruence.
        -- rewrite length_cons in H0. simpl in H0. congruence.
        -- rewrite <-! app_comm_cons in H. inversion H; subst.
           rewrite! length_cons in H0. inversion H0.
           destruct (IHa b c d). easy. subst. easy.
Qed.