text:
(*
  Autor(s):
    Andrej Dudenhefner (1)
  Affiliation(s):
    (1) Saarland University, Saarbrücken, Germany
*)

(*
  Reduction(s):
    Halting Problem of One-Counter Machines (CM1_HALT) to
    Uniform Boundedness of Deterministic, Length-preserving Stack Machines
*)

Require Import Relation_Operators Lia PeanoNat List.
Import ListNotations.

Require Undecidability.CounterMachines.CM1.
Module CM := CM1.
Require Undecidability.CounterMachines.Util.CM1_facts.
Module CM_facts := CM1_facts.

Require Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.SMX.

Require Import Undecidability.StackMachines.SMN.

From Undecidability.StackMachines.Util Require Import Facts Nat_facts List_facts Enumerable.
Require Import Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.CM1_to_SMX.

Require Import ssreflect ssrbool ssrfun.

Set Default Proof Using "Type".
Set Default Goal Selector "!".

Module Argument.

Local Instance Prefix_Enumerable : Enumerable Prefix.
Proof.
  exists
    (fun x => if x is Try then 0 else if x is Yes then 1 else 2)
    (fun x => if x is 0 then Try else if x is 1 then Yes else No).
  by case.
Qed.

Local Instance BasicState_Enumerable : Enumerable BasicState.
Proof.
  apply: (enumerableI
    (fun x => match x with
      | is_bounded b => inl b | index p n => inr (inl (p, n)) | increase p n => inr (inr (p, n))
      end)
    (fun x => match x with
      | inl b => is_bounded b | inr (inl (p, n)) => index p n | inr (inr (p, n)) => increase p n
      end)).
   by case.
Qed.

Local Instance State_Enumerable : Enumerable State.
Proof.
  apply: (enumerableI
    (fun x => match x with
      | basic_state X => inl X | goto n X Y => inr (n, X, Y)
      end)
    (fun x =>
      match x with
      | inl X => basic_state X | inr (n, X, Y) => goto n X Y
      end)).
  by case.
Qed.

Section Reduction.
  Variable MX : SMX.SMX (State := State) (Symbol := Symbol).
  Variable deterministic_MX : SMX.deterministic MX.
  Variable length_preserving_MX : forall s t X s' t' Y b,
    In ((s, t, X), (s', t', Y), b) MX -> length (s ++ t) = length (s' ++ t') /\ 1 <= length (s ++ t).
  Variable flip_consistent_MX : forall s1 t1 X c b1 s2 t2 c2 b2,
    In ((s1, t1, X), c, b1) MX -> In ((s2, t2, X), c2, b2) MX -> b1 = b2.

  Local Definition SMX_Instruction := SMX.Instruction (State := State) (Symbol := Symbol).

  Definition encode_Symbol (a: Symbol) : bool := if a is zero then false else true.

  Definition decode_Symbol (a: bool) : Symbol := if a is false then zero else one.

  Definition encode_Stack (s: list Symbol) : list bool := map encode_Symbol s.

  Definition decode_Stack (s: list bool) : list Symbol := map decode_Symbol s.

  Lemma encode_decode_Stack {s: list bool} : encode_Stack (decode_Stack s) = s.
  Proof. rewrite /encode_Stack /decode_Stack map_map. elim: s; [done | by case=> l /= ->]. Qed.

  Lemma decode_encode_Stack {s: list Symbol} : decode_Stack (encode_Stack s) = s.
  Proof. rewrite /encode_Stack /decode_Stack map_map. elim: s; [done | by case=> l /= ->]. Qed.

  Lemma encode_Stack_inj {s t: list Symbol} : encode_Stack s = encode_Stack t -> s = t.
  Proof. move /(f_equal decode_Stack). by rewrite ?decode_encode_Stack. Qed.

  Lemma encode_Stack_app {v w} : encode_Stack (v ++ w) = encode_Stack v ++ encode_Stack w.
  Proof. by rewrite /encode_Stack map_app. Qed.

  (* state (x, true) represents that the next instruction has to be performed mirrored *)
  Definition encode_Instruction : SMX_Instruction -> list Instruction :=
    fun '((r, s, x), (r', s', y), b) => if b is true then
      [
        ((encode_Stack r, encode_Stack s, to_nat (x, false)), (encode_Stack r', encode_Stack s', to_nat (y, true)));
        ((encode_Stack s, encode_Stack r, to_nat (x, true)), (encode_Stack s', encode_Stack r', to_nat (y, false)))
      ] else
      [
        ((encode_Stack r, encode_Stack s, to_nat (x, false)), (encode_Stack r', encode_Stack s', to_nat (y, false)));
        ((encode_Stack s, encode_Stack r, to_nat (x, true)), (encode_Stack s', encode_Stack r', to_nat (y, true)))
      ].

  (* encoding of MX *)
  Definition MN: SMN := flat_map encode_Instruction MX.

  Theorem length_preserving_MN : length_preserving MN.
  Proof using length_preserving_MX.
    move=> s t X s' t' Y. rewrite /MN in_flat_map /encode_Instruction.
    move=> [[[[[? ?] ?] [[? ?] ?]] b]] [/length_preserving_MX [H1 H2]].
    case: b; (case; last (case; last done)).
    all: move=> [] *; subst; move: H1 H2; rewrite /encode_Stack ?app_length ?map_length; by lia.
  Qed.

  Lemma simulation_step_false {l r x l' r' y} :
    SMX.step MX (l, r, x) (l', r', y) ->
    step MN (encode_Stack l, encode_Stack r, to_nat (x, false)) (encode_Stack l', encode_Stack r', to_nat (y, false)) \/
    step MN (encode_Stack l, encode_Stack r, to_nat (x, false)) (encode_Stack r', encode_Stack l', to_nat (y, true)).
  Proof.
    move Hc: (l, r, x) => c. move Hd: (l', r', y) => d Hcd. case: Hcd Hc Hd.
    move=> v w r1 s1 r2 s2 x' y' [|] HMX [] ? ? ? [] ? ? ?; subst.
    - right. rewrite ?encode_Stack_app. apply: transition.
      rewrite in_flat_map. eexists. constructor; first by eassumption.
      by left.
    - left. rewrite ?encode_Stack_app. apply: transition.
      rewrite in_flat_map. eexists. constructor; first by eassumption.
      by left.
  Qed.

  Lemma simulation_step_true {l r x l' r' y} :
    SMX.step MX (l, r, x) (l', r', y) ->
    step MN (encode_Stack r, encode_Stack l, to_nat (x, true)) (encode_Stack r', encode_Stack l', to_nat (y, true)) \/
    step MN (encode_Stack r, encode_Stack l, to_nat (x, true)) (encode_Stack l', encode_Stack r', to_nat (y, false)).
  Proof.
    move Hc: (l, r, x) => c. move Hd: (l', r', y) => d Hcd. case: Hcd Hc Hd.
    move=> v w r1 s1 r2 s2 x' y' [|] HMX [] ? ? ? [] ? ? ?; subst.
    - right. rewrite ?encode_Stack_app. apply: transition.
      rewrite in_flat_map. eexists. constructor; first by eassumption.
      right. by left.
    - left. rewrite ?encode_Stack_app. apply: transition.
      rewrite in_flat_map. eexists. constructor; first by eassumption.
      right. by left.
  Qed.

  Lemma simulation {c d} :
    SMX.reachable MX c d ->
    let '(l, r, x) := c in let '(l', r', y) := d in
    (reachable MN (encode_Stack r, encode_Stack l, to_nat (x, true)) (encode_Stack r', encode_Stack l', to_nat (y, true)) \/
    reachable MN (encode_Stack r, encode_Stack l, to_nat (x, true)) (encode_Stack l', encode_Stack r', to_nat (y, false))) /\
    (reachable MN (encode_Stack l, encode_Stack r, to_nat (x, false)) (encode_Stack l', encode_Stack r', to_nat (y, false)) \/
    reachable MN (encode_Stack l, encode_Stack r, to_nat (x, false)) (encode_Stack r', encode_Stack l', to_nat (y, true))).
  Proof.
    elim.
    - move=> [[l r] x] [[l' r'] y] Hxy. constructor.
      + have [? | ?] := simulation_step_true Hxy; [left | right]; by apply: rt_step.
      + have [? | ?] := simulation_step_false Hxy; [left | right]; by apply: rt_step.
    - move=> [[l r] x]. constructor; left; by apply rt_refl.
    - move=> [[lx rx] x] [[ly ry] y] [[lz rz] z] _ Hxy _ Hyz. constructor.
      + move: Hxy Hyz => [[Hxy|Hxy] _].
        * move=> [[Hyz|Hyz] _]; [left | right]; apply: rt_trans; by eassumption.
        * move=> [_ [Hyz|Hyz]]; [right | left]; apply: rt_trans; by eassumption.
      + move: Hxy Hyz => [_ [Hxy|Hxy]].
        * move=> [_ [Hyz|Hyz]]; [left | right]; apply: rt_trans; by eassumption.
        * move=> [[Hyz|Hyz] _]; [right | left] ; apply: rt_trans; by eassumption.
  Qed.

  Lemma inverse_simulation_step L R X : exists (x: State) (b_x: bool) (l r: list Symbol) (b_y: bool),
    forall L' R' Y, step MN (L, R, X) (L', R', Y) ->
      exists (y: State) (l' r': list Symbol),
      (L, R, X) = (encode_Stack l, encode_Stack r, to_nat (x, b_x)) /\
      (L', R', Y) = (encode_Stack l', encode_Stack r', to_nat (y, b_y)) /\
        match b_x, b_y with
        | false, false => SMX.step MX (l, r, x) (l', r', y)
        | false, true => SMX.step MX (l, r, x) (r', l', y)
        | true, false => SMX.step MX (r, l, x) (l', r', y)
        | true, true => SMX.step MX (r, l, x) (r', l', y)
        end.
  Proof using flip_consistent_MX.
    set x_b_x : State * bool := of_nat X.
    move Hx_b_x: x_b_x => [x b_x]. subst x_b_x. exists x, b_x, (decode_Stack L), (decode_Stack R).
    have := Exists_dec (fun '((_, X), _, b) => X = x) MX.
    move=> /(_ ltac:(move=> [[[? ?] ?] ?]; do 3 (decide equality))). case; first last.
    { move Hx': (L, R, X) => x' HMX. exists false. move=> L' R' Y HXY. exfalso. apply: HMX.
      apply /Exists_exists. case: HXY Hx'. move=> >.
      rewrite /MN in_flat_map. move=> [[[[[? ?] ?] [[? ?] ?]] b]] + [] *. subst.
      move=> [H2MX HX]. eexists. constructor; first by eassumption. move=> /=.
      move: b HX {H2MX} => /= [|].
      { case.
        - move=> [] *. subst. move: Hx_b_x. by rewrite enumP => [[]].
        - case; last done. move=> [] *. subst. move: Hx_b_x. by rewrite enumP => [[]]. }
      case.
        - move=> [] *. subst. move: Hx_b_x. by rewrite enumP => [[]].
        - case; last done. move=> [] *. subst. move: Hx_b_x. by rewrite enumP => [[]]. }
    rewrite Exists_exists. move=> [[[[[? ?] x'] [[? ?] ?]] b'] [H2MX ?]]. subst x'.
    exists (if b' then negb b_x else b_x).
    move=> L' R' Y.
    move Hc: (L, R, X) => c. move Hd: (L', R', Y) => d Hcd. case: Hcd Hc Hd Hx_b_x.
    move=> v w r1 s1 r2 s2 x' y + [] ? ? ? [] ? ? ?; subst.
    rewrite /MN in_flat_map. move=> [[[[[? ?] ?] [[? ?] ?]] b]].
    move=> + Hx_b_x. rewrite ?encode_decode_Stack -Hx_b_x.
    case: b.
    { move=> [HMX] /=. case.
      - move=> [] *. subst. move: Hx_b_x. rewrite ?enumP. move=> [? ?]. subst.
        have ? := flip_consistent_MX _ _ _ _ _ _ _ _ _ HMX H2MX. subst b'.
        rewrite -(@encode_decode_Stack v) -(@encode_decode_Stack w) -?encode_Stack_app. do 3 eexists.
        constructor; first by reflexivity. constructor; first by reflexivity.
        move: HMX => /(SMX.transition MX). rewrite ?decode_encode_Stack. by apply.
      - case; last done.
        move=> [] *. subst. move: Hx_b_x. rewrite ?enumP. move=> [? ?]. subst.
        have ? := flip_consistent_MX _ _ _ _ _ _ _ _ _ HMX H2MX. subst b'.
        rewrite -(@encode_decode_Stack v) -(@encode_decode_Stack w) -?encode_Stack_app. do 3 eexists.
        constructor; first by reflexivity. constructor; first by reflexivity.
        move: HMX => /(SMX.transition MX). rewrite ?decode_encode_Stack. by apply. }
    move=> [HMX] /=. case.
    - move=> [] *. subst. move: Hx_b_x. rewrite ?enumP. move=> [? ?]. subst.
      have ? := flip_consistent_MX _ _ _ _ _ _ _ _ _ HMX H2MX. subst b'.
      rewrite -(@encode_decode_Stack v) -(@encode_decode_Stack w) -?encode_Stack_app. do 3 eexists.
      constructor; first by reflexivity. constructor; first by reflexivity.
      move: HMX => /(SMX.transition MX). rewrite ?decode_encode_Stack. by apply.
    - case; last done.
      move=> [] *. subst. move: Hx_b_x. rewrite ?enumP. move=> [? ?]. subst.
      have ? := flip_consistent_MX _ _ _ _ _ _ _ _ _ HMX H2MX. subst b'.
      rewrite -(@encode_decode_Stack v) -(@encode_decode_Stack w) -?encode_Stack_app. do 3 eexists.
      constructor; first by reflexivity. constructor; first by reflexivity.
      move: HMX => /(SMX.transition MX). rewrite ?decode_encode_Stack. apply.
  Qed.

  Lemma deterministic_MN : deterministic MN.
  Proof using flip_consistent_MX deterministic_MX.
    move=> [[L R] X]. have [x [b_x [l [r [b_y Hx]]]]]:= inverse_simulation_step L R X.
    move=> [[? ?] ?] [[? ?] ?] /Hx + /Hx.
    move=> [y [ly [ry [{}Hx [-> Hy]]]]] [z [lz [rz [_ [-> Hz]]]]].
    move: b_x b_y Hx Hy Hz.
    move=> [|] [|] ?; move /deterministic_MX => H /H; by congruence.
  Qed.

  Lemma inverse_simulation {x y} :
  reachable MN x y -> x = y \/
  let '(L, R, X) := x in let '(L', R', Y) := y in
  exists (x y: State) (b_x b_y: bool) (l r l' r': list Symbol),
    (L, R, X) = (encode_Stack l, encode_Stack r, to_nat (x, b_x)) /\
    (L', R', Y) = (encode_Stack l', encode_Stack r', to_nat (y, b_y)) /\
    match b_x, b_y with
    | false, false => SMX.reachable MX (l, r, x) (l', r', y)
    | false, true => SMX.reachable MX (l, r, x) (r', l', y)
    | true, false => SMX.reachable MX (r, l, x) (l', r', y)
    | true, true => SMX.reachable MX (r, l, x) (r', l', y)
    end.
  Proof using flip_consistent_MX.
    elim.
    - move=> [[L R] X]. have [{}x [b_x [l [r [b_y Hx]]]]] := inverse_simulation_step L R X.
      move=> [[? ?] ?] /Hx{Hx} => [[{}y]] [l'] [r'] [->] [->] Hxy.
      right. do 8 eexists. constructor; first by reflexivity. constructor; first by reflexivity.
      move: b_x b_y Hxy => [|] [|] Hxy; by apply: rt_step.
    - move=> ?. by left.
    - move=> [[L1 R1] X1] [[L2 R2] X2] [[L3 R3] X3].
      move=> _ [[] ? ? ?|IH1]; first by subst.
      move=> _ [[] ? ? ?|IH2]; first by (subst; right).
      move: IH1 => [x1] [y1] [b_x1] [b_y1] [l1] [r1] [l'1] [r'1] [[]] ? ? ? [[]] ? ? ? Hx1y1.
      move: IH2 => [x2] [y2] [b_x2] [b_y2] [l2] [r2] [l'2] [r'2] [[]] ? ? ? [[]] ? ? ? Hx2y2.
      subst. right. exists x1, y2, b_x1, b_y2, l1, r1, l'2, r'2.
      constructor; first done. constructor; first done.
      have [? ?]: (y1, b_y1) = (x2, b_x2) by apply /to_nat_inj.
      have ?: l'1 = l2 by (apply: encode_Stack_inj; congruence).
      have ?: r'1 = r2 by (apply: encode_Stack_inj; congruence).
      subst.
      move: Hx1y1 Hx2y2. clear. move: b_x1 b_x2 b_y2 => [|] [|] [|]; by apply: rt_trans.
  Qed.

  Section Transport.
    Variable NMX : nat.
    Variable bounded_MX : SMX.bounded MX NMX.

    Lemma bounded_MN : bounded MN (1 + 4*NMX).
    Proof using flip_consistent_MX bounded_MX.
      rewrite /bounded. move=> [[L R] X].
      set x_b_x : State * bool := of_nat X.
      move Hx: x_b_x => [x b_x].
      have [T1 [H1T1 H2T1]] := bounded_MX (decode_Stack L, decode_Stack R, x).
      have [T2 [H1T2 H2T2]] := bounded_MX (decode_Stack R, decode_Stack L, x).
      exists ([(L, R, X)] ++
        flat_map (fun '(l, r, x) =>
          [(encode_Stack l, encode_Stack r, to_nat (x, b_x));
          (encode_Stack r, encode_Stack l, to_nat (x, negb b_x))]) T1 ++
        flat_map (fun '(l, r, x) =>
          [(encode_Stack l, encode_Stack r, to_nat (x, negb b_x));
          (encode_Stack r, encode_Stack l, to_nat (x, b_x))]) T2).
      constructor.
      { move=> [[L' R'] Y] /inverse_simulation. case.
        { move=> <-. by left. }
        move=> [x'] [y'] [b_x'] [b_y'] [l] [r] [l'] [r'].
        move=> [[]] ? ? ? [[]] ? ? ?. subst.
        have [? ?] : (x, b_x) = (x', b_x') by rewrite -Hx /x_b_x enumP. subst.
        move Hb_x: (b_x') => b_x. move Hb_y: (b_y') => b_y.
        rewrite ?decode_encode_Stack in H1T1.
        rewrite ?decode_encode_Stack in H1T2.

        move: b_x b_y Hb_x Hb_y => [|] [|] ? ?; subst; rewrite ?in_app_iff ?in_flat_map.
        - move /H1T2 => ?. right. right. eexists.
          constructor; first by eassumption.
          move=> /=. by firstorder done.
        - move /H1T2 => ?. right. right. eexists.
          constructor; first by eassumption.
          move=> /=. by firstorder done.
        - move /H1T1 => ?. right. left. eexists.
          constructor; first by eassumption.
          move=> /=. by firstorder done.
        - move /H1T1 => ?. right. left. eexists.
          constructor; first by eassumption.
          move=> /=. by firstorder done.
      }
      rewrite ?app_length.
      set f1 := (f in (flat_map f T1)). set f2 := (f in (flat_map f T2)).
      have := legnth_flat_map (f := f1) (l := T1) (n := 2).
      apply: unnest.
      { move=> [[? ?] ?]. rewrite /f1 /length. by lia. }
      have := legnth_flat_map (f := f2) (l := T2) (n := 2).
      apply: unnest.
      { move=> [[? ?] ?]. rewrite /f2 /length. by lia. }
      rewrite /length -?/(length _).
      move: H2T1 H2T2. move: (length _) (length _). by lia.
    Qed.

  End Transport.

  Section Reflection.
    Variable NMN : nat.
    Variable bounded_MN : bounded MN NMN.

    Definition encode_State : State * bool -> nat := to_nat.

    Definition decode_State : nat -> State * bool := of_nat.

    Lemma bounded_MX : SMX.bounded MX (2*NMN).
    Proof using bounded_MN.
      rewrite /SMX.bounded. move=> [[l r] x].
      have [T [H1T H2T]]:= bounded_MN (encode_Stack l, encode_Stack r, encode_State (x, false)).
      exists
        ((map (fun '(L, R, X) => (decode_Stack L, decode_Stack R, fst (decode_State X))) T)
        ++ (map (fun '(L, R, X) => (decode_Stack R, decode_Stack L, fst (decode_State X))) T)).
      constructor; first last.
      { rewrite ?app_length ?map_length. move: (length T) H2T. by lia. }
      move=> [[l' r'] y] /simulation /=. rewrite ?in_app_iff ?in_map_iff.
      move=> [] _ [Hxy|Hxy].
      - left. exists (encode_Stack l', encode_Stack r', to_nat (y, false)).
        rewrite ?decode_encode_Stack /decode_State ?enumP /=.
        constructor; first done.
        by apply: H1T.
      - right. exists (encode_Stack r', encode_Stack l', to_nat (y, true)).
        rewrite ?decode_encode_Stack /decode_State ?enumP /=.
        constructor; first done.
        by apply: H1T.
    Qed.

  End Reflection.

End Reduction.
End Argument.

Require Import Undecidability.Synthetic.Definitions.
Require Import Undecidability.CounterMachines.CM1.

(* many-one reduction from counter machine halting to uniform boundedness of stack machines *)
Theorem reduction : CM1_HALT ⪯ SMNdl_UB.
Proof.
  unshelve eexists (fun '(exist _ P HP) => exist _ (Argument.MN (M P)) _).
  (* establish domain properties *)
  - constructor; [apply: Argument.deterministic_MN | apply: Argument.length_preserving_MN].
    + by apply: deterministic_M.
    + by apply: flip_consistent_M.
    + by apply: length_preserving_M.
  - move=> [P HP]. constructor.
    + move=> [nP] /(terminating_P_to_bounded_M P HP).
      move /Argument.bounded_MN => bounded_MN. eexists.
      apply: bounded_MN. by apply: flip_consistent_M.
    + move=> [nMN] /= /Argument.bounded_MX /(bounded_M_to_terminating_P P HP) H'P.
      eexists. by eassumption.
Qed.

author: uds-psl

repo: coq-synthetic-incompleteness


text:
Require Export Induction.

Module NatList.

  Inductive natprod : Type :=
    | pair : nat -> nat -> natprod.

  Check (pair 3 5).

  Definition fst (p : natprod) : nat :=
    match p with
      | pair x y => x
    end.

  Definition snd (p : natprod) : nat :=
    match p with
      | pair x y => y
    end.

  Eval compute in fst (pair 3 5).

  Notation "( x , y )" := (pair x y).
  Eval compute in fst (3, 5).

  Definition fst' (p : natprod) : nat :=
    match p with
      | (x, y) => x
    end.
  Definition snd' (p : natprod) : nat :=
    match p with
      | (x, y) => y
    end.

  Definition swap_pair (p : natprod) : natprod :=
    match p with
      | (x, y) => (y, x)
    end.

  Theorem surjective_pairing' : forall (n m : nat),
                                  (n,m) = (fst (n,m), snd (n,m)).
  Proof.
    reflexivity.
  Qed.

  Theorem surjective_pairing_stuck : forall (p : natprod),
                                       p = (fst p, snd p).
  Proof.
    simpl.
  Abort.

  Theorem surjective_pairing : forall (p : natprod),
                                 p = (fst p, snd p).
  Proof.
    destruct p. reflexivity.
  Qed.

  Theorem snd_fst_is_swap : forall (p : natprod),
                              (snd p, fst p) = swap_pair p.
  Proof.
    destruct p. reflexivity.
  Qed.

  Theorem fst_swap_is_snd : forall (p : natprod),
                              fst (swap_pair p) = snd p.
  Proof.
    destruct p. reflexivity.
  Qed.

  Inductive natlist : Type :=
  | nil : natlist
  | cons : nat -> natlist -> natlist.

  Definition mylist := cons 1 (cons 2 (cons 3 nil)).

  Notation "x :: l" := (cons x l) (at level 60, right associativity).
  Notation "[ ]" := nil.
  Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

  Definition mylist1 := 1 :: (2 :: (3 :: nil)).
  Definition mylist2 := 1 :: 2 :: 3 :: nil.
  Definition mylist3 := [1;2;3].

  Fixpoint repeat (n count : nat) : natlist :=
    match count with
      | O => nil
      | S cnt => n :: repeat n cnt
    end.

  Fixpoint length (l : natlist) : nat :=
    match l with
      | nil => O
      | _ :: l' => S (length l')
    end.

  Fixpoint app (l1 l2 : natlist) : natlist :=
    match l1 with
      | nil => l2
      | h :: t => h :: app t l2
    end.

  Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).

  Example test_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5].
  Proof. reflexivity. Qed.
  Example test_app2: nil ++ [4;5] = [4;5].
  Proof. reflexivity. Qed.
  Example test_app3: [1;2;3] ++ nil = [1;2;3].
  Proof. reflexivity. Qed.

  Definition hd (default : nat) (l : natlist) : nat :=
    match l with
      | nil => default
      | h :: _ => h
    end.

  Definition tl (l : natlist) : natlist :=
    match l with
      | nil => nil
      | h :: t => t
    end.

  Example test_hd1: hd 0 [1;2;3] = 1.
  Proof. reflexivity. Qed.
  Example test_hd2: hd 0 [] = 0.
  Proof. reflexivity. Qed.
  Example test_tl: tl [1;2;3] = [2;3].
  Proof. reflexivity. Qed.

  Fixpoint nonzeros (l : natlist) : natlist :=
    match l with
      | nil => nil
      | O :: t => nonzeros t
      | S n' :: t => S n' :: nonzeros t
    end.

  Example test_nonzeros: nonzeros [0;1;0;2;3;0;0] = [1;2;3].
  Proof. simpl. reflexivity. Qed.

  SearchAbout evenb.

  Fixpoint oddmembers (l : natlist) : natlist :=
    match l with
      | nil => nil
      | h :: t =>
        if negb (evenb h) then h :: oddmembers t
        else oddmembers t
    end.

  Example test_oddmembers: oddmembers [0;1;0;2;3;0;0] = [1;3].
  Proof. simpl. reflexivity. Qed.

  Fixpoint countoddmembers (l : natlist) : nat :=
    match l with
      | nil => O
      | h :: t =>
        if negb (evenb h) then S (countoddmembers t)
        else countoddmembers t
    end.

  Example test_countoddmembers1: countoddmembers [1;0;3;1;4;5] = 4.
  Proof. simpl. reflexivity. Qed.
  Example test_countoddmembers2: countoddmembers [0;2;4] = 0.
  Proof. simpl. reflexivity. Qed.
  Example test_countoddmembers3: countoddmembers nil = 0.
  Proof. simpl. reflexivity. Qed.

  Fixpoint alternate (l1 l2 : natlist) : natlist :=
    match l1, l2 with
      | nil, nil => nil
      | nil, h :: t => h :: t
      | h :: t, nil => h :: t
      | h1 :: t1, h2 :: t2 => h1 :: h2 :: alternate t1 t2
    end.

  Example test_alternate1: alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
  Proof. simpl. reflexivity. Qed.
  Example test_alternate2: alternate [1] [4;5;6] = [1;4;5;6].
  Proof. simpl. reflexivity. Qed.
  Example test_alternate3: alternate [1;2;3] [4] = [1;4;2;3].
  Proof. simpl. reflexivity. Qed.
  Example test_alternate4: alternate [] [20;30] = [20;30].
  Proof. simpl. reflexivity. Qed.

  Definition bag := natlist.

  Fixpoint count (v : nat) (s : bag) : nat :=
    match s with
      | nil => O
      | h :: t =>
        if beq_nat v h then S (count v t)
        else count v t
    end.

  Example test_count1: count 1 [1;2;3;1;4;1] = 3.
  Proof. simpl. reflexivity. Qed.
  Example test_count2: count 6 [1;2;3;1;4;1] = 0.
  Proof. simpl. reflexivity. Qed.

  Definition sum : bag -> bag -> bag := app.
  Example test_sum1: count 1 (sum [1;2;3] [1;4;1]) = 3.
  Proof. simpl. reflexivity. Qed.

  Definition add (v : nat) (s : bag) : bag :=  v :: s.
  Example test_add1: count 1 (add 1 [1;4;1]) = 3.
  Proof. simpl. reflexivity. Qed.
  Example test_add2: count 5 (add 1 [1;4;1]) = 0.
  Proof. simpl. reflexivity. Qed.

  Definition member (v:nat) (s:bag) : bool :=
    negb (beq_nat (count v s) O).

  Example test_member1: member 1 [1;4;1] = true.
  Proof. simpl. reflexivity. Qed.
  Example test_member2: member 2 [1;4;1] = false.
  Proof. simpl. reflexivity. Qed.

  Fixpoint remove_one (v : nat) (s : bag) : bag :=
    match s with
      | nil => nil
      | h :: t =>
        if beq_nat h v then t
        else h :: remove_one v t
    end.

  Example test_remove_one1: count 5 (remove_one 5 [2;1;5;4;1]) = 0.
  Proof. simpl. reflexivity. Qed.
  Example test_remove_one2: count 5 (remove_one 5 [2;1;4;1]) = 0.
  Proof. simpl. reflexivity. Qed.
  Example test_remove_one3: count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
  Proof. simpl. reflexivity. Qed.
  Example test_remove_one4: count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
  Proof. simpl. reflexivity. Qed.

  Fixpoint remove_all (v : nat) (s : bag) : bag :=
    match s with
      | nil => nil
      | h :: t =>
        if beq_nat h v then remove_all v t
        else h :: remove_all v t
    end.

  Example test_remove_all1: count 5 (remove_all 5 [2;1;5;4;1]) = 0.
  Proof. simpl. reflexivity. Qed.
  Example test_remove_all2: count 5 (remove_all 5 [2;1;4;1]) = 0.
  Proof. simpl. reflexivity. Qed.
  Example test_remove_all3: count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
  Proof. simpl. reflexivity. Qed.
  Example test_remove_all4: count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
  Proof. simpl. reflexivity. Qed.

  Fixpoint subset (s1 : bag) (s2 : bag) : bool :=
    match s1 with
      | nil => true
      | h :: t =>
        if member h s2 then subset t (remove_one h s2)
        else false
    end.
  SearchAbout member.

  Example test_subset1: subset [1;2] [2;1;4;1] = true.
  Proof. simpl. reflexivity. Qed.
  Example test_subset2: subset [1;2;2] [2;1;4;1] = false.
  Proof. simpl. reflexivity. Qed.

  Theorem nil_app : forall l : natlist, [] ++ l = l.
  Proof. reflexivity. Qed.

  Theorem nil_app_right : forall l : natlist, l ++ [] = l.
  Proof.
    induction l.
    reflexivity.
    simpl. rewrite IHl. reflexivity.
  Qed.

  Theorem tl_length_pred : forall l:natlist,
                             pred (length l) = length (tl l).
  Proof.
    intros l. destruct l as [ | n l'].
    Case "l = nil". reflexivity.
    Case "l = cons n l'". simpl. reflexivity.
  Qed.

  Theorem app_assoc : forall l1 l2 l3 : natlist,
                        (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
  Proof.
    induction l1 as [ | n l'].
    Case "l1 = nil". reflexivity.
    Case "l1 = cons n l'".
    simpl. intros l2 l3. rewrite IHl'. reflexivity.
  Qed.

  Theorem app_length : forall l1 l2 : natlist,
                         length (l1 ++ l2) = (length l1) + (length l2).
  Proof.
    induction l1 as [ | n l].
    Case "l1 = nil". reflexivity.
    Case "l1 = cons n l".
    intros l2. simpl. rewrite IHl. reflexivity.
  Qed.

  Fixpoint snoc (l : natlist) (v : nat) : natlist :=
    match l with
      | nil => [v]
      | h :: t => h :: (snoc t v)
    end.

  Eval compute in snoc [1; 2; 3] 5.

  Fixpoint rev (l : natlist) : natlist :=
    match l with
      | nil => nil
      | h :: t => snoc (rev t) h
    end.

  Example test_rev1: rev [1;2;3] = [3;2;1].
  Proof. reflexivity. Qed.
  Example test_rev2: rev nil = nil.
  Proof. reflexivity. Qed.

  Theorem rev_length_firsttry : forall l : natlist,
                                  length (rev l) = length l.
  Proof.
    induction l as [ | n' l'].
    Case "l = nil".
    simpl. reflexivity.
    Case "l = cons n' l'".
    simpl. rewrite <- IHl'.
  Abort.

  Theorem length_snoc : forall n : nat, forall l : natlist,
                          length (snoc l n) = S (length l).
  Proof.
    induction l as [ | n' l'].
    Case "l = nil". reflexivity.
    Case "l = cons n' l'".  simpl. rewrite IHl'. reflexivity.
  Qed.

  Theorem rev_length : forall l : natlist, length (rev l) = length l.
  Proof.
    induction l as [ | n' l'].
    Case "l = nil". reflexivity.
    Case "l = cons n' l'". simpl.  rewrite length_snoc. rewrite IHl'.
    reflexivity.
  Qed.

  Theorem app_nil_end : forall l : natlist,
                          l ++ [] = l.
  Proof.
    induction l as [ | n' l'].
    Case "l = nil". reflexivity.
    Case "l = cons n' l'". simpl. rewrite IHl'. reflexivity.
  Qed.

  Lemma snoc_rev : forall ( n : nat ) ( l : natlist ),
    rev ( snoc l n ) = n :: rev l.
  Proof.
  induction l as [ | n' l'].
  Case "l = nil". reflexivity.
  Case "l = cons n' l'". simpl. rewrite IHl'. simpl. reflexivity.
  Qed.

  Theorem rev_involutive : forall l : natlist,
                             rev (rev l) = l.
  Proof.
    induction l.
    Case "l = nil". reflexivity.
    Case "l = cons n l". simpl. rewrite snoc_rev. rewrite IHl. reflexivity.
  Qed.

  Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist,
                         l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
  Proof.
    intros l1 l2 l3 l4. rewrite app_assoc. rewrite app_assoc.
    reflexivity.
  Qed.

  Theorem snoc_append : forall (l:natlist) (n:nat),
                          snoc l n = l ++ [n].
  Proof.
    induction l.
    Case "l = nil". reflexivity.
    Case "l = cons n l". simpl. intros n0. rewrite IHl. reflexivity.
  Qed.

  Theorem distr_rev : forall l1 l2 : natlist,
                        rev (l1 ++ l2) = (rev l2) ++ (rev l1).
  Proof.
    induction l1.
    Case "l1 = nil". simpl. intros l2. rewrite app_nil_end. reflexivity.
    Case "l1 = cons n l".  intros l2. simpl. repeat (rewrite snoc_append).
    rewrite IHl1. rewrite app_assoc. reflexivity.
  Qed.

  Lemma nonzeros_app : forall l1 l2 : natlist,
                         nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
  Proof.
    induction l1.
    Case "l1 = nil". reflexivity.
    Case "l1 = cons n l". intros l2.
    destruct n.
    SCase "n = O". simpl. rewrite IHl1. reflexivity.
    SCase "n = S n". simpl. rewrite IHl1. reflexivity.
  Qed.

  Fixpoint beq_natlist (l1 l2 : natlist) : bool :=
    match l1, l2 with
      | nil, nil => true
      | _ :: _, nil => false
      | nil, _::_ => false
      | h1 :: t1, h2 :: t2 =>
        andb (beq_nat h1 h2) (beq_natlist t1 t2)
    end.

  Example test_beq_natlist1 : beq_natlist nil nil = true.
  Proof. simpl. reflexivity. Qed.
  Example test_beq_natlist2 : beq_natlist [1;2;3] [1;2;3] = true.
  Proof. simpl. reflexivity. Qed.
  Example test_beq_natlist3 : beq_natlist [1;2;3] [1;2;4] = false.
  Proof. simpl. reflexivity. Qed.

  Theorem beq_natlist_refl : forall l : natlist,
                               true = beq_natlist l l.
  Proof.
    induction l.
    Case "l = nil". reflexivity.
    Case "l = cons n l". simpl. rewrite <- beq_nat_refl.
    simpl. rewrite IHl. reflexivity.
  Qed.

  Theorem count_member_nonzero : forall (s : bag),
                                   ble_nat 1 (count 1 (1 :: s)) = true.
  Proof.
    intros s. simpl. reflexivity.
  Qed.

  Theorem ble_n_Sn : forall n,
                       ble_nat n (S n) = true.
  Proof.
    induction n.
    Case "n = O". reflexivity.
    Case "n = S n".  simpl. rewrite IHn. reflexivity.
  Qed.

  Theorem remove_decreases_count: forall (s : bag),
          ble_nat (count 0 (remove_one 0 s)) (count 0 s) = true.
  Proof.
    induction s.
    Case "s = nil". reflexivity.
    Case "s = cons n l".
    destruct n.
    SCase "n = O". simpl.  apply ble_n_Sn.
    SCase "n = S n". simpl. assumption.
  Qed.

  Theorem rev_injective : forall l1 l2 : natlist,
                            rev l1 = rev l2 -> l1 = l2.
  Proof.
    intros l1 l2 H. rewrite <- rev_involutive.
    rewrite <- H. rewrite rev_involutive. reflexivity.
  Qed.

  Fixpoint index_bad (n : nat) (l : natlist) : nat :=
    match l with
      | nil => 42 (* arbitrary! *)
      | a :: l' => match beq_nat n O with
                     | true => a
                     | false => index_bad (pred n) l'
                   end
    end.

  Inductive natoption : Type :=
  | Some : nat -> natoption
  | None : natoption.

  Fixpoint index (n : nat) (l : natlist) : natoption :=
    match l with
      | nil => None
      | a :: l' => match beq_nat n O with
                     | true => Some a
                     | false => index (pred n) l'
                   end
    end.

  Example test_index1 : index 0 [4;5;6;7] = Some 4.
  Proof. reflexivity. Qed.
  Example test_index2 : index 3 [4;5;6;7] = Some 7.
  Proof. reflexivity. Qed.
  Example test_index3 : index 10 [4;5;6;7] = None.
  Proof. reflexivity. Qed.

  Fixpoint index' (n : nat) (l : natlist) : natoption :=
    match l with
      | nil => None
      | a :: l' => if beq_nat n O then Some a else index' (pred n) l'
    end.

  Definition option_elim (d : nat) (o : natoption) : nat :=
    match o with
      | Some n' => n'
      | None => d
    end.

  Definition hd_opt (l : natlist) : natoption :=
    match l with
      | nil => None
      | h :: t => Some h
    end.

  Example test_hd_opt1 : hd_opt [] = None.
  Proof. reflexivity. Qed.
  Example test_hd_opt2 : hd_opt [1] = Some 1.
  Proof. reflexivity. Qed.
  Example test_hd_opt3 : hd_opt [5;6] = Some 5.
  Proof. reflexivity. Qed.

  Theorem option_elim_hd : forall (l : natlist) (default : nat),
       hd default l = option_elim default (hd_opt l).
  Proof.
    induction l.
    Case "l = nil". reflexivity.
    Case "l = cons n l". intros default. simpl. reflexivity.
  Qed.

  Module Dictionary.

    Inductive dictionary : Type :=
    | empty : dictionary
    | record : nat -> nat -> dictionary -> dictionary.

    Eval compute in record 3 2 (record 2 2 empty).

    Definition insert (key value : nat) (d : dictionary) : dictionary :=
      (record key value d).

    Fixpoint find (key : nat) (d : dictionary) : natoption :=
      match d with
        | empty => None
        | record k v d' =>
          if (beq_nat key k) then (Some v)
          else (find key d')
      end.

    Theorem dictionary_invariant1' :
      forall (d : dictionary) (k v: nat), (find k (insert k v d)) = Some v.
    Proof.
      induction d.
      Case "d = empty". simpl. intros k v. rewrite <- beq_nat_refl. reflexivity.
      Case "d = record k v d". intros k v. simpl. rewrite <- beq_nat_refl.
      reflexivity.
    Qed.

    Theorem dictionary_invariant2' :
      forall (d : dictionary) (m n o: nat),
        beq_nat m n = false -> find m d = find m (insert n o d).
    Proof.
      intros d m n o H. simpl. rewrite H. reflexivity.
    Qed.
  End Dictionary.
End NatList.

repo: Coq


text:
From iris.proofmode Require Import tactics.
From iris.algebra Require Import auth.
From iris.base_logic.lib Require Import proph_map.
From iris.program_logic Require Import weakestpre adequacy hoare.
From intensional.heap_lang Require Import lang proofmode notation.
Set Default Proof Using "Type".

Class heapPreG Σ := HeapPreG {
  heap_preG_iris :> invPreG Σ;
  heap_preG_heap :> gen_heapPreG loc val Σ;
  heap_preG_proph :> proph_mapPreG proph_id (val * val) Σ;
  heap_preG_trace :> trace_preG Σ;
}.

Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id (val * val); traceΣ].
Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
Proof. solve_inG. Qed.

Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
  (∀ `{!heapG Σ}, ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
  adequate s e σ (λ v _, φ v).
Proof.
  intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
  iMod (gen_heap_init σ.(heap)) as (?) "Hh".
  iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
  iMod (trace_auth_init σ.(trace)) as (?) "(Ht & _ & _)".
  iModIntro. iExists
    (λ σ κs, (gen_heap_ctx σ.(heap) ∗ trace_auth σ.(trace) ∗ proph_map_ctx κs σ.(used_proph_id))%I),
    (λ _, True%I).
  iFrame. iApply (Hwp (HeapG _ _ _ _ _)).
Qed.

Definition heap_invariance Σ `{!heapPreG Σ} (N: namespace) (I: list val → Prop) s e σ :
  I (trace σ) →
  (∀ `{!heapG Σ}, ⊢ trace_inv N I -∗ trace_is (trace σ) -∗ WP e @ s; ⊤ {{ _, True }}) →
  ∀ σ' t,
    rtc erased_step ([e], σ) (t, σ') →
    I (trace σ').
Proof.
  intros HI Hwp σ' t.
  eapply (wp_invariance Σ _ s _ _ _ _ (I (trace σ'))). iIntros (Hinv κs) "".
  iMod (gen_heap_init σ.(heap)) as (?) "Hh".
  iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
  iMod (trace_auth_init σ.(trace)) as (?) "(Hta & Ht & Hth)".
  iDestruct (inv_alloc N _ (∃ t, trace_half_frag t ∗ ⌜I t⌝) with "[Hth]") as ">#HI".
  { iNext. eauto. }
  iModIntro. iExists
    (λ σ κs _, (gen_heap_ctx σ.(heap) ∗ trace_auth σ.(trace) ∗ proph_map_ctx κs σ.(used_proph_id))%I),
    (λ _, True%I).
  iFrame. iSplitL.
  { iDestruct (Hwp (HeapG _ _ _ _ _)) as "Hwp". iApply ("Hwp" with "HI Ht"). }
  iIntros "(_ & Hta & _)". iExists _.
  iInv "HI" as ">Ht'" "_". iDestruct "Ht'" as (t') "(Ht' & %)".
  iDestruct (trace_auth_half_frag_agree with "Hta Ht'") as %->. iModIntro. eauto.
Qed.

(** Specialized adequacy theorem to establish trace properties as free theorems.
   This corresponds to Theorem 4.1 in the paper.

   Minor remark 1: in the paper, the state of the operational semantics is
   represented as a pair of a heap and a trace. Here, we instead have σ,σ' be
   inhabitants of the [state] record type, and we use the [trace] projection to
   get the trace of a given state.

   Minor remark 2: the following theorem is slightly more general than the one
   from the paper, as we only require the trace property to hold of the trace of
   the initial state σ, while the theorem in the paper is specialized to the
   case where the initial trace is the empty trace. *)
Lemma module_invariance {Σ} `{heapPreG Σ} (N: namespace)
  (Φ: ∀ `{heapG Σ}, iProp Σ → val → iProp Σ)  (* Module specification *)
  (P0: iProp Σ) (* Initial resources required by the module *)
  (e: val → expr) (* Context program, parameterized by the module *)
  (e_init: expr) (* Initialization code, used to allocate resources for P0 *)
  (imimpl: val) (* Implementation of the module (instrumented) *)
  (good_trace: list val → Prop) (* Trace property *)
  (σ: state) (* Initial state *)
:
  (* The initial trace must satisfy the property *)
  good_trace (trace σ) →
  (* The context must be safe, given a module satisfying the specification Φ *)
  (⊢ ∀ `(heapG Σ) P m, Φ P m -∗ {{{ P }}} e m {{{ v, RET v; True }}}) →
  (* The initialization code must provide P0 *)
  (⊢ ∀ `(heapG Σ), {{ True }} e_init {{ _, P0 }}) →
  (* The implementation provided for the module (iops) must satisfy the specification Φ.
     On top of P0 it is given SL resources for the trace. *)
  (⊢ ∀ `(heapG Σ), Φ (P0 ∗ trace_is (trace σ) ∗ trace_inv N good_trace)%I imimpl) →
  (* Then the trace remains good at every step *)
  ∀ σ' e',
    rtc erased_step ([(e_init;; e imimpl)%E], σ) (e', σ') →
    good_trace (trace σ').
Proof.
  intros Htrσ Hctx Hinit Himpl σ' e' Hsteps.
  eapply heap_invariance. done. by apply Htrσ. 2: eapply Hsteps.
  iIntros (?) "HI Htr". wp_bind e_init.
  iApply wp_wand. by iApply Hinit.
  iIntros (v) "H0". wp_pures.
  iApply (Hctx with "[] [H0 Htr HI]").
  - iApply Himpl.
  - iFrame.
  - eauto.
Qed.

author: logsem

repo: free-theorems-sl


text:
Require Import LayerDeps.
Require Import Ident.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import Constants.
Require Import CommonLib.
Require Import AbsAccessor.Spec.
Require Import BaremoreHandler.Spec.
Require Import RmiSMC.Spec.
Require Import PSCIHandler.Spec.
Require Import PendingCheck.Spec.

Local Open Scope Z_scope.

Section Layer.

  Context `{real_params: RealParams}.

  Section InvDef.

    Record high_level_invariant (adt: RData) :=
      mkInvariants { }.

    Global Instance PendingCheck_ops : CompatDataOps RData :=
      {
        empty_data := empty_adt;
        high_level_invariant := high_level_invariant;
        low_level_invariant := fun (b: block) (d: RData) => True;
        kernel_mode adt := True
      }.

  End InvDef.

  Section InvInit.

    Global Instance PendingCheck_prf : CompatData RData.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

  End InvInit.

  Context `{Hstencil: Stencil}.
  Context `{Hmem: Mem.MemoryModelX}.
  Context `{Hmwd: UseMemWithData mem}.

  Section InvProof.

    Global Instance check_pending_ptimers_inv: PreservesInvariants check_pending_ptimers_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance check_pending_vtimers_inv: PreservesInvariants check_pending_vtimers_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance shiftl_inv: PreservesInvariants shiftl_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance addr_to_idx_inv: PreservesInvariants addr_to_idx_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance el3_sync_lel_inv: PreservesInvariants el3_sync_lel_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_sysregs_inv: PreservesInvariants set_rec_sysregs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_forward_psci_call_inv: PreservesInvariants get_psci_result_forward_psci_call_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_refcount_inc_inv: PreservesInvariants granule_refcount_inc_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance ns_buffer_read_rec_run_inv: PreservesInvariants ns_buffer_read_rec_run_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_put_inv: PreservesInvariants granule_put_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance smc_granule_undelegate_inv: PreservesInvariants smc_granule_undelegate_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance entry_is_table_inv: PreservesInvariants entry_is_table_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_pstate_inv: PreservesInvariants get_rec_pstate_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance atomic_granule_put_release_inv: PreservesInvariants atomic_granule_put_release_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance smc_rec_destroy_inv: PreservesInvariants smc_rec_destroy_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_run_gprs_inv: PreservesInvariants get_rec_run_gprs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_ptimer_asserted_inv: PreservesInvariants set_rec_ptimer_asserted_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_run_is_emulated_mmio_inv: PreservesInvariants get_rec_run_is_emulated_mmio_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance read_reg_inv: PreservesInvariants read_reg_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_refcount_dec_inv: PreservesInvariants granule_refcount_dec_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_ptimer_masked_inv: PreservesInvariants get_rec_ptimer_masked_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance measurement_extend_data_header_inv: PreservesInvariants measurement_extend_data_header_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_lock_inv: PreservesInvariants granule_lock_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance ns_buffer_unmap_inv: PreservesInvariants ns_buffer_unmap_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_memzero_mapped_inv: PreservesInvariants granule_memzero_mapped_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_common_sysregs_inv: PreservesInvariants get_rec_common_sysregs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance is_addr_in_par_rec_inv: PreservesInvariants is_addr_in_par_rec_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rd_state_inv: PreservesInvariants get_rd_state_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance esr_sixty_four_inv: PreservesInvariants esr_sixty_four_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance run_realm_inv: PreservesInvariants run_realm_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_g_rtt_refcount_inv: PreservesInvariants get_g_rtt_refcount_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance esr_srt_inv: PreservesInvariants esr_srt_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_pstate_inv: PreservesInvariants set_rec_pstate_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_pc_inv: PreservesInvariants get_rec_pc_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_get_inv: PreservesInvariants granule_get_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance buffer_unmap_inv: PreservesInvariants buffer_unmap_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance access_len_inv: PreservesInvariants access_len_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance enter_rmm_inv: PreservesInvariants enter_rmm_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_ptimer_masked_inv: PreservesInvariants set_rec_ptimer_masked_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance sysreg_read_inv: PreservesInvariants sysreg_read_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_set_state_inv: PreservesInvariants granule_set_state_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance null_ptr_inv: PreservesInvariants null_ptr_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_ns_state_inv: PreservesInvariants get_ns_state_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_vtimer_masked_inv: PreservesInvariants set_rec_vtimer_masked_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_wi_g_llt_inv: PreservesInvariants get_wi_g_llt_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_run_esr_inv: PreservesInvariants set_rec_run_esr_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_map_inv: PreservesInvariants granule_map_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_ns_state_inv: PreservesInvariants set_ns_state_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_run_gprs_inv: PreservesInvariants set_rec_run_gprs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_run_hpfar_inv: PreservesInvariants set_rec_run_hpfar_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_x0_inv: PreservesInvariants get_psci_result_x0_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_x1_inv: PreservesInvariants get_psci_result_x1_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_x2_inv: PreservesInvariants get_psci_result_x2_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance find_lock_granule_inv: PreservesInvariants find_lock_granule_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance psci_rsi_inv: PreservesInvariants psci_rsi_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance is_null_inv: PreservesInvariants is_null_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance assert_cond_inv: PreservesInvariants assert_cond_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance pgte_read_inv: PreservesInvariants pgte_read_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_vtimer_masked_inv: PreservesInvariants get_rec_vtimer_masked_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_wi_g_llt_inv: PreservesInvariants set_wi_g_llt_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_last_run_info_esr_inv: PreservesInvariants get_rec_last_run_info_esr_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance esr_is_write_inv: PreservesInvariants esr_is_write_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_x3_inv: PreservesInvariants get_psci_result_x3_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_wi_index_inv: PreservesInvariants get_wi_index_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_wi_index_inv: PreservesInvariants set_wi_index_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_unlock_inv: PreservesInvariants granule_unlock_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance emulate_timer_ctl_read_inv: PreservesInvariants emulate_timer_ctl_read_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance exit_rmm_inv: PreservesInvariants exit_rmm_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance measurement_extend_data_inv: PreservesInvariants measurement_extend_data_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance ESR_EL2_SYSREG_IS_WRITE_inv: PreservesInvariants ESR_EL2_SYSREG_IS_WRITE_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance barrier_inv: PreservesInvariants barrier_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance access_mask_inv: PreservesInvariants access_mask_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance esr_sign_extend_inv: PreservesInvariants esr_sign_extend_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_dispose_pending_inv: PreservesInvariants set_rec_dispose_pending_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rd_g_rtt_inv: PreservesInvariants get_rd_g_rtt_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_last_run_info_esr_inv: PreservesInvariants set_rec_last_run_info_esr_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_memzero_inv: PreservesInvariants granule_memzero_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_regs_inv: PreservesInvariants get_rec_regs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_forward_x3_inv: PreservesInvariants get_psci_result_forward_x3_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_forward_x2_inv: PreservesInvariants get_psci_result_forward_x2_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_forward_x1_inv: PreservesInvariants get_psci_result_forward_x1_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_run_exit_reason_inv: PreservesInvariants set_rec_run_exit_reason_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance ESR_EL2_SYSREG_ISS_RT_inv: PreservesInvariants ESR_EL2_SYSREG_ISS_RT_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance atomic_granule_put_inv: PreservesInvariants atomic_granule_put_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance read_idreg_inv: PreservesInvariants read_idreg_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_par_end_inv: PreservesInvariants get_rec_par_end_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance smc_realm_activate_inv: PreservesInvariants smc_realm_activate_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_mapping_inv: PreservesInvariants set_mapping_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_pc_inv: PreservesInvariants set_rec_pc_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_regs_inv: PreservesInvariants set_rec_regs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_runnable_inv: PreservesInvariants get_rec_runnable_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance ns_granule_map_inv: PreservesInvariants ns_granule_map_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_sysregs_inv: PreservesInvariants get_rec_sysregs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_vtimer_asserted_inv: PreservesInvariants set_rec_vtimer_asserted_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_run_emulated_write_val_inv: PreservesInvariants set_rec_run_emulated_write_val_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance smc_granule_delegate_inv: PreservesInvariants smc_granule_delegate_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_run_far_inv: PreservesInvariants set_rec_run_far_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_run_emulated_read_val_inv: PreservesInvariants get_rec_run_emulated_read_val_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_vtimer_inv: PreservesInvariants get_rec_vtimer_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_ptimer_inv: PreservesInvariants get_rec_ptimer_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance smc_rec_create_inv: PreservesInvariants smc_rec_create_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_g_rtt_rd_inv: PreservesInvariants set_g_rtt_rd_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance ns_buffer_read_data_inv: PreservesInvariants ns_buffer_read_data_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance pgte_write_inv: PreservesInvariants pgte_write_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance is_addr_in_par_inv: PreservesInvariants is_addr_in_par_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance sysreg_write_inv: PreservesInvariants sysreg_write_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance find_granule_inv: PreservesInvariants find_granule_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_par_base_inv: PreservesInvariants get_rec_par_base_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance smc_realm_create_inv: PreservesInvariants smc_realm_create_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance find_lock_unused_granule_inv: PreservesInvariants find_lock_unused_granule_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance entry_to_phys_inv: PreservesInvariants entry_to_phys_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance stage2_tlbi_ipa_inv: PreservesInvariants stage2_tlbi_ipa_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance atomic_granule_get_inv: PreservesInvariants atomic_granule_get_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance user_step_inv: PreservesInvariants user_step_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance link_table_inv: PreservesInvariants link_table_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance smc_realm_destroy_inv: PreservesInvariants smc_realm_destroy_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance timer_condition_met_inv: PreservesInvariants timer_condition_met_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance addr_is_level_aligned_inv: PreservesInvariants addr_is_level_aligned_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

  End InvProof.

  Section LayerDef.

    Definition PendingCheck_fresh : compatlayer (cdata RData) :=
      _check_pending_ptimers ↦ gensem check_pending_ptimers_spec
        ⊕ _check_pending_vtimers ↦ gensem check_pending_vtimers_spec
      .

    Definition PendingCheck_passthrough : compatlayer (cdata RData) :=
      _shiftl ↦ gensem shiftl_spec
        ⊕ _addr_to_idx ↦ gensem addr_to_idx_spec
        ⊕ _el3_sync_lel ↦ gensem el3_sync_lel_spec
        ⊕ _set_rec_sysregs ↦ gensem set_rec_sysregs_spec
        ⊕ _get_psci_result_forward_psci_call ↦ gensem get_psci_result_forward_psci_call_spec
        ⊕ _granule_refcount_inc ↦ gensem granule_refcount_inc_spec
        ⊕ _ns_buffer_read_rec_run ↦ gensem ns_buffer_read_rec_run_spec
        ⊕ _granule_put ↦ gensem granule_put_spec
        ⊕ _smc_granule_undelegate ↦ gensem smc_granule_undelegate_spec
        ⊕ _entry_is_table ↦ gensem entry_is_table_spec
        ⊕ _get_rec_pstate ↦ gensem get_rec_pstate_spec
        ⊕ _atomic_granule_put_release ↦ gensem atomic_granule_put_release_spec
        ⊕ _smc_rec_destroy ↦ gensem smc_rec_destroy_spec
        ⊕ _get_rec_run_gprs ↦ gensem get_rec_run_gprs_spec
        ⊕ _set_rec_ptimer_asserted ↦ gensem set_rec_ptimer_asserted_spec
        ⊕ _get_rec_run_is_emulated_mmio ↦ gensem get_rec_run_is_emulated_mmio_spec
        ⊕ _read_reg ↦ gensem read_reg_spec
        ⊕ _granule_refcount_dec ↦ gensem granule_refcount_dec_spec
        ⊕ _get_rec_ptimer_masked ↦ gensem get_rec_ptimer_masked_spec
        ⊕ _measurement_extend_data_header ↦ gensem measurement_extend_data_header_spec
        ⊕ _granule_lock ↦ gensem granule_lock_spec
        ⊕ _ns_buffer_unmap ↦ gensem ns_buffer_unmap_spec
        ⊕ _granule_memzero_mapped ↦ gensem granule_memzero_mapped_spec
        ⊕ _get_rec_common_sysregs ↦ gensem get_rec_common_sysregs_spec
        ⊕ _is_addr_in_par_rec ↦ gensem is_addr_in_par_rec_spec
        ⊕ _get_rd_state ↦ gensem get_rd_state_spec
        ⊕ _esr_sixty_four ↦ gensem esr_sixty_four_spec
        ⊕ _run_realm ↦ gensem run_realm_spec
        ⊕ _get_g_rtt_refcount ↦ gensem get_g_rtt_refcount_spec
        ⊕ _esr_srt ↦ gensem esr_srt_spec
        ⊕ _set_rec_pstate ↦ gensem set_rec_pstate_spec
        ⊕ _get_rec_pc ↦ gensem get_rec_pc_spec
        ⊕ _granule_get ↦ gensem granule_get_spec
        ⊕ _buffer_unmap ↦ gensem buffer_unmap_spec
        ⊕ _access_len ↦ gensem access_len_spec
        ⊕ _enter_rmm ↦ gensem enter_rmm_spec
        ⊕ _set_rec_ptimer_masked ↦ gensem set_rec_ptimer_masked_spec
        ⊕ _sysreg_read ↦ gensem sysreg_read_spec
        ⊕ _granule_set_state ↦ gensem granule_set_state_spec
        ⊕ _null_ptr ↦ gensem null_ptr_spec
        ⊕ _get_ns_state ↦ gensem get_ns_state_spec
        ⊕ _set_rec_vtimer_masked ↦ gensem set_rec_vtimer_masked_spec
        ⊕ _get_wi_g_llt ↦ gensem get_wi_g_llt_spec
        ⊕ _set_rec_run_esr ↦ gensem set_rec_run_esr_spec
        ⊕ _granule_map ↦ gensem granule_map_spec
        ⊕ _set_ns_state ↦ gensem set_ns_state_spec
        ⊕ _set_rec_run_gprs ↦ gensem set_rec_run_gprs_spec
        ⊕ _set_rec_run_hpfar ↦ gensem set_rec_run_hpfar_spec
        ⊕ _get_psci_result_x0 ↦ gensem get_psci_result_x0_spec
        ⊕ _get_psci_result_x1 ↦ gensem get_psci_result_x1_spec
        ⊕ _get_psci_result_x2 ↦ gensem get_psci_result_x2_spec
        ⊕ _find_lock_granule ↦ gensem find_lock_granule_spec
        ⊕ _psci_rsi ↦ gensem psci_rsi_spec
        ⊕ _is_null ↦ gensem is_null_spec
        ⊕ _assert_cond ↦ gensem assert_cond_spec
        ⊕ _pgte_read ↦ gensem pgte_read_spec
        ⊕ _get_rec_vtimer_masked ↦ gensem get_rec_vtimer_masked_spec
        ⊕ _set_wi_g_llt ↦ gensem set_wi_g_llt_spec
        ⊕ _get_rec_last_run_info_esr ↦ gensem get_rec_last_run_info_esr_spec
        ⊕ _esr_is_write ↦ gensem esr_is_write_spec
        ⊕ _get_psci_result_x3 ↦ gensem get_psci_result_x3_spec
        ⊕ _get_wi_index ↦ gensem get_wi_index_spec
        ⊕ _set_wi_index ↦ gensem set_wi_index_spec
        ⊕ _granule_unlock ↦ gensem granule_unlock_spec
        ⊕ _emulate_timer_ctl_read ↦ gensem emulate_timer_ctl_read_spec
        ⊕ _exit_rmm ↦ gensem exit_rmm_spec
        ⊕ _measurement_extend_data ↦ gensem measurement_extend_data_spec
        ⊕ _ESR_EL2_SYSREG_IS_WRITE ↦ gensem ESR_EL2_SYSREG_IS_WRITE_spec
        ⊕ _barrier ↦ gensem barrier_spec
        ⊕ _access_mask ↦ gensem access_mask_spec
        ⊕ _esr_sign_extend ↦ gensem esr_sign_extend_spec
        ⊕ _set_rec_dispose_pending ↦ gensem set_rec_dispose_pending_spec
        ⊕ _get_rd_g_rtt ↦ gensem get_rd_g_rtt_spec
        ⊕ _set_rec_last_run_info_esr ↦ gensem set_rec_last_run_info_esr_spec
        ⊕ _granule_memzero ↦ gensem granule_memzero_spec
        ⊕ _get_rec_regs ↦ gensem get_rec_regs_spec
        ⊕ _get_psci_result_forward_x3 ↦ gensem get_psci_result_forward_x3_spec
        ⊕ _get_psci_result_forward_x2 ↦ gensem get_psci_result_forward_x2_spec
        ⊕ _get_psci_result_forward_x1 ↦ gensem get_psci_result_forward_x1_spec
        ⊕ _set_rec_run_exit_reason ↦ gensem set_rec_run_exit_reason_spec
        ⊕ _ESR_EL2_SYSREG_ISS_RT ↦ gensem ESR_EL2_SYSREG_ISS_RT_spec
        ⊕ _atomic_granule_put ↦ gensem atomic_granule_put_spec
        ⊕ _read_idreg ↦ gensem read_idreg_spec
        ⊕ _get_rec_par_end ↦ gensem get_rec_par_end_spec
        ⊕ _smc_realm_activate ↦ gensem smc_realm_activate_spec
        ⊕ _set_mapping ↦ gensem set_mapping_spec
        ⊕ _set_rec_pc ↦ gensem set_rec_pc_spec
        ⊕ _set_rec_regs ↦ gensem set_rec_regs_spec
        ⊕ _get_rec_runnable ↦ gensem get_rec_runnable_spec
        ⊕ _ns_granule_map ↦ gensem ns_granule_map_spec
        ⊕ _get_rec_sysregs ↦ gensem get_rec_sysregs_spec
        ⊕ _set_rec_vtimer_asserted ↦ gensem set_rec_vtimer_asserted_spec
        ⊕ _set_rec_run_emulated_write_val ↦ gensem set_rec_run_emulated_write_val_spec
        ⊕ _smc_granule_delegate ↦ gensem smc_granule_delegate_spec
        ⊕ _set_rec_run_far ↦ gensem set_rec_run_far_spec
        ⊕ _get_rec_run_emulated_read_val ↦ gensem get_rec_run_emulated_read_val_spec
        ⊕ _get_rec_vtimer ↦ gensem get_rec_vtimer_spec
        ⊕ _get_rec_ptimer ↦ gensem get_rec_ptimer_spec
        ⊕ _smc_rec_create ↦ gensem smc_rec_create_spec
        ⊕ _set_g_rtt_rd ↦ gensem set_g_rtt_rd_spec
        ⊕ _ns_buffer_read_data ↦ gensem ns_buffer_read_data_spec
        ⊕ _pgte_write ↦ gensem pgte_write_spec
        ⊕ _is_addr_in_par ↦ gensem is_addr_in_par_spec
        ⊕ _sysreg_write ↦ gensem sysreg_write_spec
        ⊕ _find_granule ↦ gensem find_granule_spec
        ⊕ _get_rec_par_base ↦ gensem get_rec_par_base_spec
        ⊕ _smc_realm_create ↦ gensem smc_realm_create_spec
        ⊕ _find_lock_unused_granule ↦ gensem find_lock_unused_granule_spec
        ⊕ _entry_to_phys ↦ gensem entry_to_phys_spec
        ⊕ _stage2_tlbi_ipa ↦ gensem stage2_tlbi_ipa_spec
        ⊕ _atomic_granule_get ↦ gensem atomic_granule_get_spec
        ⊕ _user_step ↦ gensem user_step_spec
        ⊕ _link_table ↦ gensem link_table_spec
        ⊕ _smc_realm_destroy ↦ gensem smc_realm_destroy_spec
        ⊕ _timer_condition_met ↦ gensem timer_condition_met_spec
        ⊕ _addr_is_level_aligned ↦ gensem addr_is_level_aligned_spec
      .

    Definition PendingCheck := PendingCheck_fresh ⊕ PendingCheck_passthrough.

  End LayerDef.

End Layer.

author: columbia