text:
(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Instruction selection for operators *)

(** The instruction selection pass recognizes opportunities for using
  combined arithmetic and logical operations and addressing modes
  offered by the target processor.  For instance, the expression [x + 1]
  can take advantage of the "immediate add" instruction of the processor,
  and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned
  into a "rotate and mask" instruction.

  This file defines functions for building CminorSel expressions and
  statements, especially expressions consisting of operator
  applications.  These functions examine their arguments to choose
  cheaper forms of operators whenever possible.

  For instance, [add e1 e2] will return a CminorSel expression semantically
  equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a
  [Oaddimm] operator if one of the arguments is an integer constant,
  or suppress the addition altogether if one of the arguments is the
  null integer.  In passing, we perform operator reassociation
  ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount
  of constant propagation.

  On top of the "smart constructor" functions defined below,
  module [Selection] implements the actual instruction selection pass.
*)

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import CminorSel.

Open Local Scope cminorsel_scope.

(** ** Constants **)

(** External oracle to determine whether a symbol is external and must
  be addressed through [Oaddrsymbol], or is local and can be addressed
  through [Olea Aglobal].  This is to accommodate MacOS X's limitations
  on references to data symbols imported from shared libraries. *)

Parameter symbol_is_external: ident -> bool.

Definition addrsymbol (id: ident) (ofs: int) :=
  if symbol_is_external id then
    if Int.eq ofs Int.zero
    then Eop (Oindirectsymbol id) Enil
    else Eop (Olea (Aindexed ofs)) (Eop (Oindirectsymbol id) Enil ::: Enil)
  else
    Eop (Olea (Aglobal id ofs)) Enil.

Definition addrstack (ofs: int) :=
  Eop (Olea (Ainstack ofs)) Enil.

(** ** Integer logical negation *)

Definition notint (e: expr) := Eop (Oxorimm Int.mone) (e ::: Enil).

(** ** Integer addition and pointer addition *)

Definition offset_addressing (a: addressing) (ofs: int) : addressing :=
  match a with
  | Aindexed n => Aindexed (Int.add n ofs)
  | Aindexed2 n => Aindexed2 (Int.add n ofs)
  | Ascaled sc n => Ascaled sc (Int.add n ofs)
  | Aindexed2scaled sc n => Aindexed2scaled sc (Int.add n ofs)
  | Aglobal id n => Aglobal id (Int.add n ofs)
  | Abased id n => Abased id (Int.add n ofs)
  | Abasedscaled sc id n => Abasedscaled sc id (Int.add n ofs)
  | Ainstack n => Ainstack (Int.add n ofs)
  end.

(** Original definition:
<<
Nondetfunction addimm (n: int) (e: expr) :=
  if Int.eq n Int.zero then e else
  match e with
  | Eop (Ointconst m) Enil       => Eop (Ointconst(Int.add n m)) Enil
  | Eop (Olea addr) args         => Eop (Olea (offset_addressing addr n)) args
  | _                            => Eop (Olea (Aindexed n)) (e ::: Enil)
  end.
>>
*)

Inductive addimm_cases: forall (e: expr), Type :=
  | addimm_case1: forall m, addimm_cases (Eop (Ointconst m) Enil)
  | addimm_case2: forall addr args, addimm_cases (Eop (Olea addr) args)
  | addimm_default: forall (e: expr), addimm_cases e.

Definition addimm_match (e: expr) :=
  match e as zz1 return addimm_cases zz1 with
  | Eop (Ointconst m) Enil => addimm_case1 m
  | Eop (Olea addr) args => addimm_case2 addr args
  | e => addimm_default e
  end.

Definition addimm (n: int) (e: expr) :=
 if Int.eq n Int.zero then e else match addimm_match e with
  | addimm_case1 m => (* Eop (Ointconst m) Enil *)
      Eop (Ointconst(Int.add n m)) Enil
  | addimm_case2 addr args => (* Eop (Olea addr) args *)
      Eop (Olea (offset_addressing addr n)) args
  | addimm_default e =>
      Eop (Olea (Aindexed n)) (e ::: Enil)
  end.

(** Original definition:
<<
Nondetfunction add (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => addimm n1 t2
  | t1, Eop (Ointconst n2) Enil => addimm n2 t1
  | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) =>
      Eop (Olea (Aindexed2 (Int.add n1 n2))) (t1:::t2:::Enil)
  | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Ascaled sc n2)) (t2:::Enil) =>
      Eop (Olea (Aindexed2scaled sc (Int.add n1 n2))) (t1:::t2:::Enil)
  | Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) =>
      Eop (Olea (Aindexed2scaled sc (Int.add n1 n2))) (t2:::t1:::Enil)
  | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil =>
      Eop (Olea (Abased id (Int.add ofs n1))) (t1:::Enil)
  | Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Aindexed n2)) (t2:::Enil) =>
      Eop (Olea (Abased id (Int.add ofs n2))) (t2:::Enil)
  | Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil =>
      Eop (Olea (Abasedscaled sc id (Int.add ofs n1))) (t1:::Enil)
  | Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Ascaled sc n2)) (t2:::Enil) =>
      Eop (Olea (Abasedscaled sc id (Int.add ofs n2))) (t2:::Enil)
  | Eop (Olea (Ascaled sc n)) (t1:::Enil), t2 =>
      Eop (Olea (Aindexed2scaled sc n)) (t2:::t1:::Enil)
  | t1, Eop (Olea (Ascaled sc n)) (t2:::Enil) =>
      Eop (Olea (Aindexed2scaled sc n)) (t1:::t2:::Enil)
  | Eop (Olea (Aindexed n)) (t1:::Enil), t2 =>
      Eop (Olea (Aindexed2 n)) (t1:::t2:::Enil)
  | t1, Eop (Olea (Aindexed n)) (t2:::Enil) =>
      Eop (Olea (Aindexed2 n)) (t1:::t2:::Enil)
  | _, _ =>
      Eop (Olea (Aindexed2 Int.zero)) (e1:::e2:::Enil)
  end.
>>
*)

Inductive add_cases: forall (e1: expr) (e2: expr), Type :=
  | add_case1: forall n1 t2, add_cases (Eop (Ointconst n1) Enil) (t2)
  | add_case2: forall t1 n2, add_cases (t1) (Eop (Ointconst n2) Enil)
  | add_case3: forall n1 t1 n2 t2, add_cases (Eop (Olea (Aindexed n1)) (t1:::Enil)) (Eop (Olea (Aindexed n2)) (t2:::Enil))
  | add_case4: forall n1 t1 sc n2 t2, add_cases (Eop (Olea (Aindexed n1)) (t1:::Enil)) (Eop (Olea (Ascaled sc n2)) (t2:::Enil))
  | add_case5: forall sc n1 t1 n2 t2, add_cases (Eop (Olea (Ascaled sc n1)) (t1:::Enil)) (Eop (Olea (Aindexed n2)) (t2:::Enil))
  | add_case6: forall n1 t1 id ofs, add_cases (Eop (Olea (Aindexed n1)) (t1:::Enil)) (Eop (Olea (Aglobal id ofs)) Enil)
  | add_case7: forall id ofs n2 t2, add_cases (Eop (Olea (Aglobal id ofs)) Enil) (Eop (Olea (Aindexed n2)) (t2:::Enil))
  | add_case8: forall sc n1 t1 id ofs, add_cases (Eop (Olea (Ascaled sc n1)) (t1:::Enil)) (Eop (Olea (Aglobal id ofs)) Enil)
  | add_case9: forall id ofs sc n2 t2, add_cases (Eop (Olea (Aglobal id ofs)) Enil) (Eop (Olea (Ascaled sc n2)) (t2:::Enil))
  | add_case10: forall sc n t1 t2, add_cases (Eop (Olea (Ascaled sc n)) (t1:::Enil)) (t2)
  | add_case11: forall t1 sc n t2, add_cases (t1) (Eop (Olea (Ascaled sc n)) (t2:::Enil))
  | add_case12: forall n t1 t2, add_cases (Eop (Olea (Aindexed n)) (t1:::Enil)) (t2)
  | add_case13: forall t1 n t2, add_cases (t1) (Eop (Olea (Aindexed n)) (t2:::Enil))
  | add_default: forall (e1: expr) (e2: expr), add_cases e1 e2.

Definition add_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return add_cases zz1 zz2 with
  | Eop (Ointconst n1) Enil, t2 => add_case1 n1 t2
  | t1, Eop (Ointconst n2) Enil => add_case2 t1 n2
  | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) => add_case3 n1 t1 n2 t2
  | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Ascaled sc n2)) (t2:::Enil) => add_case4 n1 t1 sc n2 t2
  | Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) => add_case5 sc n1 t1 n2 t2
  | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil => add_case6 n1 t1 id ofs
  | Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Aindexed n2)) (t2:::Enil) => add_case7 id ofs n2 t2
  | Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil => add_case8 sc n1 t1 id ofs
  | Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Ascaled sc n2)) (t2:::Enil) => add_case9 id ofs sc n2 t2
  | Eop (Olea (Ascaled sc n)) (t1:::Enil), t2 => add_case10 sc n t1 t2
  | t1, Eop (Olea (Ascaled sc n)) (t2:::Enil) => add_case11 t1 sc n t2
  | Eop (Olea (Aindexed n)) (t1:::Enil), t2 => add_case12 n t1 t2
  | t1, Eop (Olea (Aindexed n)) (t2:::Enil) => add_case13 t1 n t2
  | e1, e2 => add_default e1 e2
  end.

Definition add (e1: expr) (e2: expr) :=
  match add_match e1 e2 with
  | add_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *)
      addimm n1 t2
  | add_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *)
      addimm n2 t1
  | add_case3 n1 t1 n2 t2 => (* Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) *)
      Eop (Olea (Aindexed2 (Int.add n1 n2))) (t1:::t2:::Enil)
  | add_case4 n1 t1 sc n2 t2 => (* Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Ascaled sc n2)) (t2:::Enil) *)
      Eop (Olea (Aindexed2scaled sc (Int.add n1 n2))) (t1:::t2:::Enil)
  | add_case5 sc n1 t1 n2 t2 => (* Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) *)
      Eop (Olea (Aindexed2scaled sc (Int.add n1 n2))) (t2:::t1:::Enil)
  | add_case6 n1 t1 id ofs => (* Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil *)
      Eop (Olea (Abased id (Int.add ofs n1))) (t1:::Enil)
  | add_case7 id ofs n2 t2 => (* Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Aindexed n2)) (t2:::Enil) *)
      Eop (Olea (Abased id (Int.add ofs n2))) (t2:::Enil)
  | add_case8 sc n1 t1 id ofs => (* Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil *)
      Eop (Olea (Abasedscaled sc id (Int.add ofs n1))) (t1:::Enil)
  | add_case9 id ofs sc n2 t2 => (* Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Ascaled sc n2)) (t2:::Enil) *)
      Eop (Olea (Abasedscaled sc id (Int.add ofs n2))) (t2:::Enil)
  | add_case10 sc n t1 t2 => (* Eop (Olea (Ascaled sc n)) (t1:::Enil), t2 *)
      Eop (Olea (Aindexed2scaled sc n)) (t2:::t1:::Enil)
  | add_case11 t1 sc n t2 => (* t1, Eop (Olea (Ascaled sc n)) (t2:::Enil) *)
      Eop (Olea (Aindexed2scaled sc n)) (t1:::t2:::Enil)
  | add_case12 n t1 t2 => (* Eop (Olea (Aindexed n)) (t1:::Enil), t2 *)
      Eop (Olea (Aindexed2 n)) (t1:::t2:::Enil)
  | add_case13 t1 n t2 => (* t1, Eop (Olea (Aindexed n)) (t2:::Enil) *)
      Eop (Olea (Aindexed2 n)) (t1:::t2:::Enil)
  | add_default e1 e2 =>
      Eop (Olea (Aindexed2 Int.zero)) (e1:::e2:::Enil)
  end.

(** ** Integer and pointer subtraction *)

(** Original definition:
<<
Nondetfunction sub (e1: expr) (e2: expr) :=
  match e1, e2 with
  | t1, Eop (Ointconst n2) Enil => addimm (Int.neg n2) t1
  | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) =>
      addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
  | Eop (Olea (Aindexed n1)) (t1:::Enil), t2 =>
      addimm n1 (Eop Osub (t1:::t2:::Enil))
  | t1, Eop (Olea (Aindexed n2)) (t2:::Enil) =>
      addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil))
  | _, _ =>
      Eop Osub (e1:::e2:::Enil)
  end.
>>
*)

Inductive sub_cases: forall (e1: expr) (e2: expr), Type :=
  | sub_case1: forall t1 n2, sub_cases (t1) (Eop (Ointconst n2) Enil)
  | sub_case2: forall n1 t1 n2 t2, sub_cases (Eop (Olea (Aindexed n1)) (t1:::Enil)) (Eop (Olea (Aindexed n2)) (t2:::Enil))
  | sub_case3: forall n1 t1 t2, sub_cases (Eop (Olea (Aindexed n1)) (t1:::Enil)) (t2)
  | sub_case4: forall t1 n2 t2, sub_cases (t1) (Eop (Olea (Aindexed n2)) (t2:::Enil))
  | sub_default: forall (e1: expr) (e2: expr), sub_cases e1 e2.

Definition sub_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return sub_cases zz1 zz2 with
  | t1, Eop (Ointconst n2) Enil => sub_case1 t1 n2
  | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) => sub_case2 n1 t1 n2 t2
  | Eop (Olea (Aindexed n1)) (t1:::Enil), t2 => sub_case3 n1 t1 t2
  | t1, Eop (Olea (Aindexed n2)) (t2:::Enil) => sub_case4 t1 n2 t2
  | e1, e2 => sub_default e1 e2
  end.

Definition sub (e1: expr) (e2: expr) :=
  match sub_match e1 e2 with
  | sub_case1 t1 n2 => (* t1, Eop (Ointconst n2) Enil *)
      addimm (Int.neg n2) t1
  | sub_case2 n1 t1 n2 t2 => (* Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) *)
      addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
  | sub_case3 n1 t1 t2 => (* Eop (Olea (Aindexed n1)) (t1:::Enil), t2 *)
      addimm n1 (Eop Osub (t1:::t2:::Enil))
  | sub_case4 t1 n2 t2 => (* t1, Eop (Olea (Aindexed n2)) (t2:::Enil) *)
      addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil))
  | sub_default e1 e2 =>
      Eop Osub (e1:::e2:::Enil)
  end.

Definition negint (e: expr) := Eop Oneg (e ::: Enil).

(** ** Immediate shifts *)

Definition shift_is_scale (n: int) : bool :=
  Int.eq n (Int.repr 1) || Int.eq n (Int.repr 2) || Int.eq n (Int.repr 3).

(** Original definition:
<<
Nondetfunction shlimm (e1: expr) (n: int) :=
  if Int.eq n Int.zero then e1 else
  match e1 with
  | Eop (Ointconst n1) Enil =>
      Eop (Ointconst(Int.shl n1 n)) Enil
  | Eop (Oshlimm n1) (t1:::Enil) =>
      if Int.ltu (Int.add n n1) Int.iwordsize
      then Eop (Oshlimm (Int.add n n1)) (t1:::Enil)
      else Eop (Oshlimm n) (e1:::Enil)
  | Eop (Olea (Aindexed n1)) (t1:::Enil) =>
      if shift_is_scale n
      then Eop (Olea (Ascaled (Int.shl Int.one n) (Int.shl n1 n))) (t1:::Enil)
      else Eop (Oshlimm n) (e1:::Enil)
  | _ =>
      if shift_is_scale n
      then Eop (Olea (Ascaled (Int.shl Int.one n) Int.zero)) (e1:::Enil)
      else Eop (Oshlimm n) (e1:::Enil)
  end.
>>
*)

Inductive shlimm_cases: forall (e1: expr) , Type :=
  | shlimm_case1: forall n1, shlimm_cases (Eop (Ointconst n1) Enil)
  | shlimm_case2: forall n1 t1, shlimm_cases (Eop (Oshlimm n1) (t1:::Enil))
  | shlimm_case3: forall n1 t1, shlimm_cases (Eop (Olea (Aindexed n1)) (t1:::Enil))
  | shlimm_default: forall (e1: expr) , shlimm_cases e1.

Definition shlimm_match (e1: expr)  :=
  match e1 as zz1 return shlimm_cases zz1 with
  | Eop (Ointconst n1) Enil => shlimm_case1 n1
  | Eop (Oshlimm n1) (t1:::Enil) => shlimm_case2 n1 t1
  | Eop (Olea (Aindexed n1)) (t1:::Enil) => shlimm_case3 n1 t1
  | e1 => shlimm_default e1
  end.

Definition shlimm (e1: expr) (n: int) :=
 if Int.eq n Int.zero then e1 else match shlimm_match e1 with
  | shlimm_case1 n1 => (* Eop (Ointconst n1) Enil *)
      Eop (Ointconst(Int.shl n1 n)) Enil
  | shlimm_case2 n1 t1 => (* Eop (Oshlimm n1) (t1:::Enil) *)
      if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshlimm (Int.add n n1)) (t1:::Enil) else Eop (Oshlimm n) (e1:::Enil)
  | shlimm_case3 n1 t1 => (* Eop (Olea (Aindexed n1)) (t1:::Enil) *)
      if shift_is_scale n then Eop (Olea (Ascaled (Int.shl Int.one n) (Int.shl n1 n))) (t1:::Enil) else Eop (Oshlimm n) (e1:::Enil)
  | shlimm_default e1 =>
      if shift_is_scale n then Eop (Olea (Ascaled (Int.shl Int.one n) Int.zero)) (e1:::Enil) else Eop (Oshlimm n) (e1:::Enil)
  end.

(** Original definition:
<<
Nondetfunction shruimm (e1: expr) (n: int) :=
  if Int.eq n Int.zero then e1 else
  match e1 with
  | Eop (Ointconst n1) Enil =>
      Eop (Ointconst(Int.shru n1 n)) Enil
  | Eop (Oshruimm n1) (t1:::Enil) =>
      if Int.ltu (Int.add n n1) Int.iwordsize
      then Eop (Oshruimm (Int.add n n1)) (t1:::Enil)
      else Eop (Oshruimm n) (e1:::Enil)
  | _ =>
      Eop (Oshruimm n) (e1:::Enil)
  end.
>>
*)

Inductive shruimm_cases: forall (e1: expr) , Type :=
  | shruimm_case1: forall n1, shruimm_cases (Eop (Ointconst n1) Enil)
  | shruimm_case2: forall n1 t1, shruimm_cases (Eop (Oshruimm n1) (t1:::Enil))
  | shruimm_default: forall (e1: expr) , shruimm_cases e1.

Definition shruimm_match (e1: expr)  :=
  match e1 as zz1 return shruimm_cases zz1 with
  | Eop (Ointconst n1) Enil => shruimm_case1 n1
  | Eop (Oshruimm n1) (t1:::Enil) => shruimm_case2 n1 t1
  | e1 => shruimm_default e1
  end.

Definition shruimm (e1: expr) (n: int) :=
 if Int.eq n Int.zero then e1 else match shruimm_match e1 with
  | shruimm_case1 n1 => (* Eop (Ointconst n1) Enil *)
      Eop (Ointconst(Int.shru n1 n)) Enil
  | shruimm_case2 n1 t1 => (* Eop (Oshruimm n1) (t1:::Enil) *)
      if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshruimm (Int.add n n1)) (t1:::Enil) else Eop (Oshruimm n) (e1:::Enil)
  | shruimm_default e1 =>
      Eop (Oshruimm n) (e1:::Enil)
  end.

(** Original definition:
<<
Nondetfunction shrimm (e1: expr) (n: int) :=
  if Int.eq n Int.zero then e1 else
  match e1 with
  | Eop (Ointconst n1) Enil =>
      Eop (Ointconst(Int.shr n1 n)) Enil
  | Eop (Oshrimm n1) (t1:::Enil) =>
      if Int.ltu (Int.add n n1) Int.iwordsize
      then Eop (Oshrimm (Int.add n n1)) (t1:::Enil)
      else Eop (Oshrimm n) (e1:::Enil)
  | _ =>
      Eop (Oshrimm n) (e1:::Enil)
  end.
>>
*)

Inductive shrimm_cases: forall (e1: expr) , Type :=
  | shrimm_case1: forall n1, shrimm_cases (Eop (Ointconst n1) Enil)
  | shrimm_case2: forall n1 t1, shrimm_cases (Eop (Oshrimm n1) (t1:::Enil))
  | shrimm_default: forall (e1: expr) , shrimm_cases e1.

Definition shrimm_match (e1: expr)  :=
  match e1 as zz1 return shrimm_cases zz1 with
  | Eop (Ointconst n1) Enil => shrimm_case1 n1
  | Eop (Oshrimm n1) (t1:::Enil) => shrimm_case2 n1 t1
  | e1 => shrimm_default e1
  end.

Definition shrimm (e1: expr) (n: int) :=
 if Int.eq n Int.zero then e1 else match shrimm_match e1 with
  | shrimm_case1 n1 => (* Eop (Ointconst n1) Enil *)
      Eop (Ointconst(Int.shr n1 n)) Enil
  | shrimm_case2 n1 t1 => (* Eop (Oshrimm n1) (t1:::Enil) *)
      if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshrimm (Int.add n n1)) (t1:::Enil) else Eop (Oshrimm n) (e1:::Enil)
  | shrimm_default e1 =>
      Eop (Oshrimm n) (e1:::Enil)
  end.

(** ** Integer multiply *)

Definition mulimm_base (n1: int) (e2: expr) :=
  match Int.one_bits n1 with
  | i :: nil =>
      shlimm e2 i
  | i :: j :: nil =>
      Elet e2 (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j))
  | _ =>
      Eop (Omulimm n1) (e2:::Enil)
  end.

(** Original definition:
<<
Nondetfunction mulimm (n1: int) (e2: expr) :=
  if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil
  else if Int.eq n1 Int.one then e2
  else match e2 with
  | Eop (Ointconst n2) Enil => Eop (Ointconst(Int.mul n1 n2)) Enil
  | Eop (Olea (Aindexed n2)) (t2:::Enil) => addimm (Int.mul n1 n2) (mulimm_base n1 t2)
  | _ => mulimm_base n1 e2
  end.
>>
*)

Inductive mulimm_cases: forall (e2: expr), Type :=
  | mulimm_case1: forall n2, mulimm_cases (Eop (Ointconst n2) Enil)
  | mulimm_case2: forall n2 t2, mulimm_cases (Eop (Olea (Aindexed n2)) (t2:::Enil))
  | mulimm_default: forall (e2: expr), mulimm_cases e2.

Definition mulimm_match (e2: expr) :=
  match e2 as zz1 return mulimm_cases zz1 with
  | Eop (Ointconst n2) Enil => mulimm_case1 n2
  | Eop (Olea (Aindexed n2)) (t2:::Enil) => mulimm_case2 n2 t2
  | e2 => mulimm_default e2
  end.

Definition mulimm (n1: int) (e2: expr) :=
 if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.one then e2 else match mulimm_match e2 with
  | mulimm_case1 n2 => (* Eop (Ointconst n2) Enil *)
      Eop (Ointconst(Int.mul n1 n2)) Enil
  | mulimm_case2 n2 t2 => (* Eop (Olea (Aindexed n2)) (t2:::Enil) *)
      addimm (Int.mul n1 n2) (mulimm_base n1 t2)
  | mulimm_default e2 =>
      mulimm_base n1 e2
  end.

(** Original definition:
<<
Nondetfunction mul (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => mulimm n1 t2
  | t1, Eop (Ointconst n2) Enil => mulimm n2 t1
  | _, _ => Eop Omul (e1:::e2:::Enil)
  end.
>>
*)

Inductive mul_cases: forall (e1: expr) (e2: expr), Type :=
  | mul_case1: forall n1 t2, mul_cases (Eop (Ointconst n1) Enil) (t2)
  | mul_case2: forall t1 n2, mul_cases (t1) (Eop (Ointconst n2) Enil)
  | mul_default: forall (e1: expr) (e2: expr), mul_cases e1 e2.

Definition mul_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return mul_cases zz1 zz2 with
  | Eop (Ointconst n1) Enil, t2 => mul_case1 n1 t2
  | t1, Eop (Ointconst n2) Enil => mul_case2 t1 n2
  | e1, e2 => mul_default e1 e2
  end.

Definition mul (e1: expr) (e2: expr) :=
  match mul_match e1 e2 with
  | mul_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *)
      mulimm n1 t2
  | mul_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *)
      mulimm n2 t1
  | mul_default e1 e2 =>
      Eop Omul (e1:::e2:::Enil)
  end.

(** ** Bitwise and, or, xor *)

(** Original definition:
<<
Nondetfunction andimm (n1: int) (e2: expr) :=
  if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil
  else if Int.eq n1 Int.mone then e2
  else match e2 with
  | Eop (Ointconst n2) Enil =>
      Eop (Ointconst (Int.and n1 n2)) Enil
  | Eop (Oandimm n2) (t2:::Enil) =>
     Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
  | Eop Ocast8unsigned (t2:::Enil) =>
     Eop (Oandimm (Int.and n1 (Int.repr 255))) (t2:::Enil)
  | Eop Ocast16unsigned (t2:::Enil) =>
     Eop (Oandimm (Int.and n1 (Int.repr 65535))) (t2:::Enil)
  | _ =>
     Eop (Oandimm n1) (e2:::Enil)
  end.
>>
*)

Inductive andimm_cases: forall (e2: expr), Type :=
  | andimm_case1: forall n2, andimm_cases (Eop (Ointconst n2) Enil)
  | andimm_case2: forall n2 t2, andimm_cases (Eop (Oandimm n2) (t2:::Enil))
  | andimm_case3: forall t2, andimm_cases (Eop Ocast8unsigned (t2:::Enil))
  | andimm_case4: forall t2, andimm_cases (Eop Ocast16unsigned (t2:::Enil))
  | andimm_default: forall (e2: expr), andimm_cases e2.

Definition andimm_match (e2: expr) :=
  match e2 as zz1 return andimm_cases zz1 with
  | Eop (Ointconst n2) Enil => andimm_case1 n2
  | Eop (Oandimm n2) (t2:::Enil) => andimm_case2 n2 t2
  | Eop Ocast8unsigned (t2:::Enil) => andimm_case3 t2
  | Eop Ocast16unsigned (t2:::Enil) => andimm_case4 t2
  | e2 => andimm_default e2
  end.

Definition andimm (n1: int) (e2: expr) :=
 if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.mone then e2 else match andimm_match e2 with
  | andimm_case1 n2 => (* Eop (Ointconst n2) Enil *)
      Eop (Ointconst (Int.and n1 n2)) Enil
  | andimm_case2 n2 t2 => (* Eop (Oandimm n2) (t2:::Enil) *)
      Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
  | andimm_case3 t2 => (* Eop Ocast8unsigned (t2:::Enil) *)
      Eop (Oandimm (Int.and n1 (Int.repr 255))) (t2:::Enil)
  | andimm_case4 t2 => (* Eop Ocast16unsigned (t2:::Enil) *)
      Eop (Oandimm (Int.and n1 (Int.repr 65535))) (t2:::Enil)
  | andimm_default e2 =>
      Eop (Oandimm n1) (e2:::Enil)
  end.

(** Original definition:
<<
Nondetfunction and (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => andimm n1 t2
  | t1, Eop (Ointconst n2) Enil => andimm n2 t1
  | _, _ => Eop Oand (e1:::e2:::Enil)
  end.
>>
*)

Inductive and_cases: forall (e1: expr) (e2: expr), Type :=
  | and_case1: forall n1 t2, and_cases (Eop (Ointconst n1) Enil) (t2)
  | and_case2: forall t1 n2, and_cases (t1) (Eop (Ointconst n2) Enil)
  | and_default: forall (e1: expr) (e2: expr), and_cases e1 e2.

Definition and_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return and_cases zz1 zz2 with
  | Eop (Ointconst n1) Enil, t2 => and_case1 n1 t2
  | t1, Eop (Ointconst n2) Enil => and_case2 t1 n2
  | e1, e2 => and_default e1 e2
  end.

Definition and (e1: expr) (e2: expr) :=
  match and_match e1 e2 with
  | and_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *)
      andimm n1 t2
  | and_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *)
      andimm n2 t1
  | and_default e1 e2 =>
      Eop Oand (e1:::e2:::Enil)
  end.

(** Original definition:
<<
Nondetfunction orimm (n1: int) (e2: expr) :=
  if Int.eq n1 Int.zero then e2
  else if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil
  else match e2 with
  | Eop (Ointconst n2) Enil =>
      Eop (Ointconst (Int.or n1 n2)) Enil
  | Eop (Oorimm n2) (t2:::Enil) =>
     Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
  | _ =>
     Eop (Oorimm n1) (e2:::Enil)
  end.
>>
*)

Inductive orimm_cases: forall (e2: expr), Type :=
  | orimm_case1: forall n2, orimm_cases (Eop (Ointconst n2) Enil)
  | orimm_case2: forall n2 t2, orimm_cases (Eop (Oorimm n2) (t2:::Enil))
  | orimm_default: forall (e2: expr), orimm_cases e2.

Definition orimm_match (e2: expr) :=
  match e2 as zz1 return orimm_cases zz1 with
  | Eop (Ointconst n2) Enil => orimm_case1 n2
  | Eop (Oorimm n2) (t2:::Enil) => orimm_case2 n2 t2
  | e2 => orimm_default e2
  end.

Definition orimm (n1: int) (e2: expr) :=
 if Int.eq n1 Int.zero then e2 else if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil else match orimm_match e2 with
  | orimm_case1 n2 => (* Eop (Ointconst n2) Enil *)
      Eop (Ointconst (Int.or n1 n2)) Enil
  | orimm_case2 n2 t2 => (* Eop (Oorimm n2) (t2:::Enil) *)
      Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
  | orimm_default e2 =>
      Eop (Oorimm n1) (e2:::Enil)
  end.

Definition same_expr_pure (e1 e2: expr) :=
  match e1, e2 with
  | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false
  | _, _ => false
  end.

(** Original definition:
<<
Nondetfunction or (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => orimm n1 t2
  | t1, Eop (Ointconst n2) Enil => orimm n2 t1
  | Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) =>
      if Int.eq (Int.add n1 n2) Int.iwordsize then
        if same_expr_pure t1 t2
        then Eop (Ororimm n2) (t1:::Enil)
        else Eop (Oshldimm n1) (t1:::t2:::Enil)
      else Eop Oor (e1:::e2:::Enil)
  | Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) =>
      if Int.eq (Int.add n1 n2) Int.iwordsize then
        if same_expr_pure t1 t2
        then Eop (Ororimm n2) (t1:::Enil)
        else Eop (Oshldimm n1) (t1:::t2:::Enil)
      else Eop Oor (e1:::e2:::Enil)
  | _, _ =>
      Eop Oor (e1:::e2:::Enil)
  end.
>>
*)

Inductive or_cases: forall (e1: expr) (e2: expr), Type :=
  | or_case1: forall n1 t2, or_cases (Eop (Ointconst n1) Enil) (t2)
  | or_case2: forall t1 n2, or_cases (t1) (Eop (Ointconst n2) Enil)
  | or_case3: forall n1 t1 n2 t2, or_cases (Eop (Oshlimm n1) (t1:::Enil)) (Eop (Oshruimm n2) (t2:::Enil))
  | or_case4: forall n2 t2 n1 t1, or_cases (Eop (Oshruimm n2) (t2:::Enil)) (Eop (Oshlimm n1) (t1:::Enil))
  | or_default: forall (e1: expr) (e2: expr), or_cases e1 e2.

Definition or_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return or_cases zz1 zz2 with
  | Eop (Ointconst n1) Enil, t2 => or_case1 n1 t2
  | t1, Eop (Ointconst n2) Enil => or_case2 t1 n2
  | Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) => or_case3 n1 t1 n2 t2
  | Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) => or_case4 n2 t2 n1 t1
  | e1, e2 => or_default e1 e2
  end.

Definition or (e1: expr) (e2: expr) :=
  match or_match e1 e2 with
  | or_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *)
      orimm n1 t2
  | or_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *)
      orimm n2 t1
  | or_case3 n1 t1 n2 t2 => (* Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) *)
      if Int.eq (Int.add n1 n2) Int.iwordsize then if same_expr_pure t1 t2 then Eop (Ororimm n2) (t1:::Enil) else Eop (Oshldimm n1) (t1:::t2:::Enil) else Eop Oor (e1:::e2:::Enil)
  | or_case4 n2 t2 n1 t1 => (* Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) *)
      if Int.eq (Int.add n1 n2) Int.iwordsize then if same_expr_pure t1 t2 then Eop (Ororimm n2) (t1:::Enil) else Eop (Oshldimm n1) (t1:::t2:::Enil) else Eop Oor (e1:::e2:::Enil)
  | or_default e1 e2 =>
      Eop Oor (e1:::e2:::Enil)
  end.

(** Original definition:
<<
Nondetfunction xorimm (n1: int) (e2: expr) :=
  if Int.eq n1 Int.zero then e2
  else match e2 with
  | Eop (Ointconst n2) Enil =>
      Eop (Ointconst (Int.xor n1 n2)) Enil
  | Eop (Oxorimm n2) (t2:::Enil) =>
     Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil)
  | _ =>
     Eop (Oxorimm n1) (e2:::Enil)
  end.
>>
*)

Inductive xorimm_cases: forall (e2: expr), Type :=
  | xorimm_case1: forall n2, xorimm_cases (Eop (Ointconst n2) Enil)
  | xorimm_case2: forall n2 t2, xorimm_cases (Eop (Oxorimm n2) (t2:::Enil))
  | xorimm_default: forall (e2: expr), xorimm_cases e2.

Definition xorimm_match (e2: expr) :=
  match e2 as zz1 return xorimm_cases zz1 with
  | Eop (Ointconst n2) Enil => xorimm_case1 n2
  | Eop (Oxorimm n2) (t2:::Enil) => xorimm_case2 n2 t2
  | e2 => xorimm_default e2
  end.

Definition xorimm (n1: int) (e2: expr) :=
 if Int.eq n1 Int.zero then e2 else match xorimm_match e2 with
  | xorimm_case1 n2 => (* Eop (Ointconst n2) Enil *)
      Eop (Ointconst (Int.xor n1 n2)) Enil
  | xorimm_case2 n2 t2 => (* Eop (Oxorimm n2) (t2:::Enil) *)
      Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil)
  | xorimm_default e2 =>
      Eop (Oxorimm n1) (e2:::Enil)
  end.

(** Original definition:
<<
Nondetfunction xor (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => xorimm n1 t2
  | t1, Eop (Ointconst n2) Enil => xorimm n2 t1
  | _, _ => Eop Oxor (e1:::e2:::Enil)
  end.
>>
*)

Inductive xor_cases: forall (e1: expr) (e2: expr), Type :=
  | xor_case1: forall n1 t2, xor_cases (Eop (Ointconst n1) Enil) (t2)
  | xor_case2: forall t1 n2, xor_cases (t1) (Eop (Ointconst n2) Enil)
  | xor_default: forall (e1: expr) (e2: expr), xor_cases e1 e2.

Definition xor_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return xor_cases zz1 zz2 with
  | Eop (Ointconst n1) Enil, t2 => xor_case1 n1 t2
  | t1, Eop (Ointconst n2) Enil => xor_case2 t1 n2
  | e1, e2 => xor_default e1 e2
  end.

Definition xor (e1: expr) (e2: expr) :=
  match xor_match e1 e2 with
  | xor_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *)
      xorimm n1 t2
  | xor_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *)
      xorimm n2 t1
  | xor_default e1 e2 =>
      Eop Oxor (e1:::e2:::Enil)
  end.

(** ** Integer division and modulus *)

Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil).
Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil).

Definition shrximm (e1: expr) (n2: int) :=
  if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).

(** ** General shifts *)

(** Original definition:
<<
Nondetfunction shl (e1: expr) (e2: expr) :=
  match e2 with
  | Eop (Ointconst n2) Enil => shlimm e1 n2
  | _ => Eop Oshl (e1:::e2:::Enil)
  end.
>>
*)

Inductive shl_cases: forall (e2: expr), Type :=
  | shl_case1: forall n2, shl_cases (Eop (Ointconst n2) Enil)
  | shl_default: forall (e2: expr), shl_cases e2.

Definition shl_match (e2: expr) :=
  match e2 as zz1 return shl_cases zz1 with
  | Eop (Ointconst n2) Enil => shl_case1 n2
  | e2 => shl_default e2
  end.

Definition shl (e1: expr) (e2: expr) :=
  match shl_match e2 with
  | shl_case1 n2 => (* Eop (Ointconst n2) Enil *)
      shlimm e1 n2
  | shl_default e2 =>
      Eop Oshl (e1:::e2:::Enil)
  end.

(** Original definition:
<<
Nondetfunction shr (e1: expr) (e2: expr) :=
  match e2 with
  | Eop (Ointconst n2) Enil => shrimm e1 n2
  | _ => Eop Oshr (e1:::e2:::Enil)
  end.
>>
*)

Inductive shr_cases: forall (e2: expr), Type :=
  | shr_case1: forall n2, shr_cases (Eop (Ointconst n2) Enil)
  | shr_default: forall (e2: expr), shr_cases e2.

Definition shr_match (e2: expr) :=
  match e2 as zz1 return shr_cases zz1 with
  | Eop (Ointconst n2) Enil => shr_case1 n2
  | e2 => shr_default e2
  end.

Definition shr (e1: expr) (e2: expr) :=
  match shr_match e2 with
  | shr_case1 n2 => (* Eop (Ointconst n2) Enil *)
      shrimm e1 n2
  | shr_default e2 =>
      Eop Oshr (e1:::e2:::Enil)
  end.

(** Original definition:
<<
Nondetfunction shru (e1: expr) (e2: expr) :=
  match e2 with
  | Eop (Ointconst n2) Enil => shruimm e1 n2
  | _ => Eop Oshru (e1:::e2:::Enil)
  end.
>>
*)

Inductive shru_cases: forall (e2: expr), Type :=
  | shru_case1: forall n2, shru_cases (Eop (Ointconst n2) Enil)
  | shru_default: forall (e2: expr), shru_cases e2.

Definition shru_match (e2: expr) :=
  match e2 as zz1 return shru_cases zz1 with
  | Eop (Ointconst n2) Enil => shru_case1 n2
  | e2 => shru_default e2
  end.

Definition shru (e1: expr) (e2: expr) :=
  match shru_match e2 with
  | shru_case1 n2 => (* Eop (Ointconst n2) Enil *)
      shruimm e1 n2
  | shru_default e2 =>
      Eop Oshru (e1:::e2:::Enil)
  end.

(** ** Floating-point arithmetic *)

Definition negf (e: expr) :=  Eop Onegf (e ::: Enil).
Definition absf (e: expr) :=  Eop Oabsf (e ::: Enil).
Definition addf (e1 e2: expr) :=  Eop Oaddf (e1 ::: e2 ::: Enil).
Definition subf (e1 e2: expr) :=  Eop Osubf (e1 ::: e2 ::: Enil).
Definition mulf (e1 e2: expr) :=  Eop Omulf (e1 ::: e2 ::: Enil).

Definition divfimm (e: expr) (n: float) :=
  match Float.exact_inverse n with
  | Some n' => Eop Omulf (e ::: Eop (Ofloatconst n') Enil ::: Enil)
  | None    => Eop Odivf (e ::: Eop (Ofloatconst n) Enil ::: Enil)
  end.

(** Original definition:
<<
Nondetfunction divf (e1: expr) (e2: expr) :=
  match e2 with
  | Eop (Ofloatconst n2) Enil => divfimm e1 n2
  | _ => Eop Odivf (e1 ::: e2 ::: Enil)
  end.
>>
*)

Inductive divf_cases: forall (e2: expr), Type :=
  | divf_case1: forall n2, divf_cases (Eop (Ofloatconst n2) Enil)
  | divf_default: forall (e2: expr), divf_cases e2.

Definition divf_match (e2: expr) :=
  match e2 as zz1 return divf_cases zz1 with
  | Eop (Ofloatconst n2) Enil => divf_case1 n2
  | e2 => divf_default e2
  end.

Definition divf (e1: expr) (e2: expr) :=
  match divf_match e2 with
  | divf_case1 n2 => (* Eop (Ofloatconst n2) Enil *)
      divfimm e1 n2
  | divf_default e2 =>
      Eop Odivf (e1 ::: e2 ::: Enil)
  end.

(** ** Comparisons *)

(** Original definition:
<<
Nondetfunction compimm (default: comparison -> int -> condition)
                       (sem: comparison -> int -> int -> bool)
                       (c: comparison) (e1: expr) (n2: int) :=
  match c, e1 with
  | c, Eop (Ointconst n1) Enil =>
      Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil
  | Ceq, Eop (Ocmp c) el =>
      if Int.eq_dec n2 Int.zero then
        Eop (Ocmp (negate_condition c)) el
      else if Int.eq_dec n2 Int.one then
        Eop (Ocmp c) el
      else
        Eop (Ointconst Int.zero) Enil
  | Cne, Eop (Ocmp c) el =>
      if Int.eq_dec n2 Int.zero then
        Eop (Ocmp c) el
      else if Int.eq_dec n2 Int.one then
        Eop (Ocmp (negate_condition c)) el
      else
        Eop (Ointconst Int.one) Enil
  | Ceq, Eop (Oandimm n1) (t1 ::: Enil) =>
      if Int.eq_dec n2 Int.zero then
        Eop (Ocmp (Cmaskzero n1)) (t1 ::: Enil)
      else
        Eop (Ocmp (default c n2)) (e1 ::: Enil)
  | Cne, Eop (Oandimm n1) (t1 ::: Enil) =>
      if Int.eq_dec n2 Int.zero then
        Eop (Ocmp (Cmasknotzero n1)) (t1 ::: Enil)
      else
        Eop (Ocmp (default c n2)) (e1 ::: Enil)
  | _, _ =>
       Eop (Ocmp (default c n2)) (e1 ::: Enil)
  end.
>>
*)

Inductive compimm_cases: forall (c: comparison) (e1: expr) , Type :=
  | compimm_case1: forall c n1, compimm_cases (c) (Eop (Ointconst n1) Enil)
  | compimm_case2: forall c el, compimm_cases (Ceq) (Eop (Ocmp c) el)
  | compimm_case3: forall c el, compimm_cases (Cne) (Eop (Ocmp c) el)
  | compimm_case4: forall n1 t1, compimm_cases (Ceq) (Eop (Oandimm n1) (t1 ::: Enil))
  | compimm_case5: forall n1 t1, compimm_cases (Cne) (Eop (Oandimm n1) (t1 ::: Enil))
  | compimm_default: forall (c: comparison) (e1: expr) , compimm_cases c e1.

Definition compimm_match (c: comparison) (e1: expr)  :=
  match c as zz1, e1 as zz2 return compimm_cases zz1 zz2 with
  | c, Eop (Ointconst n1) Enil => compimm_case1 c n1
  | Ceq, Eop (Ocmp c) el => compimm_case2 c el
  | Cne, Eop (Ocmp c) el => compimm_case3 c el
  | Ceq, Eop (Oandimm n1) (t1 ::: Enil) => compimm_case4 n1 t1
  | Cne, Eop (Oandimm n1) (t1 ::: Enil) => compimm_case5 n1 t1
  | c, e1 => compimm_default c e1
  end.

Definition compimm (default: comparison -> int -> condition) (sem: comparison -> int -> int -> bool) (c: comparison) (e1: expr) (n2: int) :=
  match compimm_match c e1 with
  | compimm_case1 c n1 => (* c, Eop (Ointconst n1) Enil *)
      Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil
  | compimm_case2 c el => (* Ceq, Eop (Ocmp c) el *)
      if Int.eq_dec n2 Int.zero then Eop (Ocmp (negate_condition c)) el else if Int.eq_dec n2 Int.one then Eop (Ocmp c) el else Eop (Ointconst Int.zero) Enil
  | compimm_case3 c el => (* Cne, Eop (Ocmp c) el *)
      if Int.eq_dec n2 Int.zero then Eop (Ocmp c) el else if Int.eq_dec n2 Int.one then Eop (Ocmp (negate_condition c)) el else Eop (Ointconst Int.one) Enil
  | compimm_case4 n1 t1 => (* Ceq, Eop (Oandimm n1) (t1 ::: Enil) *)
      if Int.eq_dec n2 Int.zero then Eop (Ocmp (Cmaskzero n1)) (t1 ::: Enil) else Eop (Ocmp (default c n2)) (e1 ::: Enil)
  | compimm_case5 n1 t1 => (* Cne, Eop (Oandimm n1) (t1 ::: Enil) *)
      if Int.eq_dec n2 Int.zero then Eop (Ocmp (Cmasknotzero n1)) (t1 ::: Enil) else Eop (Ocmp (default c n2)) (e1 ::: Enil)
  | compimm_default c e1 =>
      Eop (Ocmp (default c n2)) (e1 ::: Enil)
  end.

(** Original definition:
<<
Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 =>
      compimm Ccompimm Int.cmp (swap_comparison c) t2 n1
  | t1, Eop (Ointconst n2) Enil =>
      compimm Ccompimm Int.cmp c t1 n2
  | _, _ =>
      Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil)
  end.
>>
*)

Inductive comp_cases: forall (e1: expr) (e2: expr), Type :=
  | comp_case1: forall n1 t2, comp_cases (Eop (Ointconst n1) Enil) (t2)
  | comp_case2: forall t1 n2, comp_cases (t1) (Eop (Ointconst n2) Enil)
  | comp_default: forall (e1: expr) (e2: expr), comp_cases e1 e2.

Definition comp_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return comp_cases zz1 zz2 with
  | Eop (Ointconst n1) Enil, t2 => comp_case1 n1 t2
  | t1, Eop (Ointconst n2) Enil => comp_case2 t1 n2
  | e1, e2 => comp_default e1 e2
  end.

Definition comp (c: comparison) (e1: expr) (e2: expr) :=
  match comp_match e1 e2 with
  | comp_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *)
      compimm Ccompimm Int.cmp (swap_comparison c) t2 n1
  | comp_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *)
      compimm Ccompimm Int.cmp c t1 n2
  | comp_default e1 e2 =>
      Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil)
  end.

(** Original definition:
<<
Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 =>
      compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1
  | t1, Eop (Ointconst n2) Enil =>
      compimm Ccompuimm Int.cmpu c t1 n2
  | _, _ =>
      Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil)
  end.
>>
*)

Inductive compu_cases: forall (e1: expr) (e2: expr), Type :=
  | compu_case1: forall n1 t2, compu_cases (Eop (Ointconst n1) Enil) (t2)
  | compu_case2: forall t1 n2, compu_cases (t1) (Eop (Ointconst n2) Enil)
  | compu_default: forall (e1: expr) (e2: expr), compu_cases e1 e2.

Definition compu_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return compu_cases zz1 zz2 with
  | Eop (Ointconst n1) Enil, t2 => compu_case1 n1 t2
  | t1, Eop (Ointconst n2) Enil => compu_case2 t1 n2
  | e1, e2 => compu_default e1 e2
  end.

Definition compu (c: comparison) (e1: expr) (e2: expr) :=
  match compu_match e1 e2 with
  | compu_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *)
      compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1
  | compu_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *)
      compimm Ccompuimm Int.cmpu c t1 n2
  | compu_default e1 e2 =>
      Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil)
  end.

Definition compf (c: comparison) (e1: expr) (e2: expr) :=
  Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil).

(** ** Integer conversions *)

(** Original definition:
<<
Nondetfunction cast8unsigned (e: expr) :=
  match e with
  | Eop (Oandimm n) (t:::Enil) =>
      Eop (Oandimm (Int.and (Int.repr 255) n)) (t:::Enil)
  | _ =>
      Eop Ocast8unsigned (e:::Enil)
  end.
>>
*)

Inductive cast8unsigned_cases: forall (e: expr), Type :=
  | cast8unsigned_case1: forall n t, cast8unsigned_cases (Eop (Oandimm n) (t:::Enil))
  | cast8unsigned_default: forall (e: expr), cast8unsigned_cases e.

Definition cast8unsigned_match (e: expr) :=
  match e as zz1 return cast8unsigned_cases zz1 with
  | Eop (Oandimm n) (t:::Enil) => cast8unsigned_case1 n t
  | e => cast8unsigned_default e
  end.

Definition cast8unsigned (e: expr) :=
  match cast8unsigned_match e with
  | cast8unsigned_case1 n t => (* Eop (Oandimm n) (t:::Enil) *)
      Eop (Oandimm (Int.and (Int.repr 255) n)) (t:::Enil)
  | cast8unsigned_default e =>
      Eop Ocast8unsigned (e:::Enil)
  end.

Definition cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil).

(** Original definition:
<<
Nondetfunction cast16unsigned (e: expr) :=
  match e with
  | Eop (Oandimm n) (t:::Enil) =>
      Eop (Oandimm (Int.and (Int.repr 65535) n)) (t:::Enil)
  | _ =>
      Eop Ocast16unsigned (e:::Enil)
  end.
>>
*)

Inductive cast16unsigned_cases: forall (e: expr), Type :=
  | cast16unsigned_case1: forall n t, cast16unsigned_cases (Eop (Oandimm n) (t:::Enil))
  | cast16unsigned_default: forall (e: expr), cast16unsigned_cases e.

Definition cast16unsigned_match (e: expr) :=
  match e as zz1 return cast16unsigned_cases zz1 with
  | Eop (Oandimm n) (t:::Enil) => cast16unsigned_case1 n t
  | e => cast16unsigned_default e
  end.

Definition cast16unsigned (e: expr) :=
  match cast16unsigned_match e with
  | cast16unsigned_case1 n t => (* Eop (Oandimm n) (t:::Enil) *)
      Eop (Oandimm (Int.and (Int.repr 65535) n)) (t:::Enil)
  | cast16unsigned_default e =>
      Eop Ocast16unsigned (e:::Enil)
  end.

Definition cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil).

(** Floating-point conversions *)

Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil).

Definition intuoffloat (e: expr) :=
  Elet e
    (Elet (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil)
      (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil))
        (intoffloat (Eletvar 1))
        (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.

Definition floatofintu (e: expr) :=
  let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in
  Elet e
    (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil))
      (floatofint (Eletvar O))
      (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f)).

(** ** Addressing modes *)

(** Original definition:
<<
Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
  match e with
  | Eop (Olea addr) args => (addr, args)
  | _ => (Aindexed Int.zero, e:::Enil)
  end.
>>
*)

Inductive addressing_cases: forall (e: expr), Type :=
  | addressing_case1: forall addr args, addressing_cases (Eop (Olea addr) args)
  | addressing_default: forall (e: expr), addressing_cases e.

Definition addressing_match (e: expr) :=
  match e as zz1 return addressing_cases zz1 with
  | Eop (Olea addr) args => addressing_case1 addr args
  | e => addressing_default e
  end.

Definition addressing (chunk: memory_chunk) (e: expr) :=
  match addressing_match e with
  | addressing_case1 addr args => (* Eop (Olea addr) args *)
      (addr, args)
  | addressing_default e =>
      (Aindexed Int.zero, e:::Enil)
  end.

author: PrincetonUniversity

repo: compcomp


text:
(* Example taken from RelationAlgebra *)
(* Was failing from r16205 up to now *)

Require Import BinNums.

Section A.

Context (A:Type) {X: A} (tst:A->Type) (top:forall X, X).

Inductive v: (positive -> A) -> Type :=
| v_L: forall f', v f'
| v_N: forall f',
  v (fun n => f' (xO n)) ->
  (positive -> tst (f' xH)) ->
  v (fun n => f' (xI n)) -> v f'.

Fixpoint v_add f' (t: v f') n: (positive -> tst (f' n)) -> v f' :=
  match t in (v o) return ((positive -> (tst (o n))) -> v o) with
    | v_L f' =>
        match n return ((positive ->  (tst (f' n))) -> v f') with
        | xH => fun x => v_N _ (v_L _) x (v_L _)
        | xO n => fun x => v_N _
          (v_add (fun n => f' (xO n)) (v_L _) n x) (fun _ => top _) (v_L _)
        | xI n => fun x => v_N _
          (v_L _) (fun _ => top _) (v_add (fun n => f' (xI n)) (v_L _) n x)
        end
    | v_N f' l y r =>
        match n with
        | xH => fun x => v_N _ l x r
        | xO n => fun x => v_N _ (v_add (fun n => f' (xO n)) l n x) y r
        | xI n => fun x => v_N _ l y (v_add (fun n => f' (xI n)) r n x)
        end
    end.

End A.

author: princeton-vl

repo: CoqGym

save_path: github-repos/coq/princeton-vl-CoqGym


text:
Require Import HoTT.

Definition unit_path : forall (x y :Unit), x = y
 := fun x y => match x, y with tt,tt => 1 end.
(* Proof. *)
(*   intros x y. *)
(*   destruct x. destruct y. exact idpath. *)
(* Qed. *)
Lemma unit_hprop : forall (x y: Unit) (p : x=y),
                     (unit_path x y) = p.
Proof.
  intros x y. induction p. destruct x. simpl.
  reflexivity.
Qed.

Theorem t281 : forall (x y : Unit) (p q : x = y), p = q.
Proof.
  induction p. intro q. transitivity (unit_path x x).
  symmetry. apply unit_hprop. apply unit_hprop.
Qed.

Definition path_empt : forall (p q: Type),
  p = Empty -> q = Empty -> p = q :=
fun (p q : Type) (H1 : p = Empty) (H2 : q = Empty) =>
let t := Empty in
match H1 in (_ = y) return (q = y -> p = q) with
| 1 => fun H3 : q = p => H3^
end H2.

(* Below we want to characterise the path space of the cartesian
product, in terms of the paths spaces of its constituents *)

(* The theorem is

  [(x = y) <~> ((fst x = fst y) * (snd x = snd y))]

We can easily define a function
f : x = y -> ((fst x = fst y) * (snd x = snd y))
 *)

Definition f {A B : Type} {x y : A * B} :
             x = y -> (fst x = fst y) * (snd x = snd y)
  := fun p => (ap fst p, ap snd p).

(* Then we use [ap2] (defn below) to write out an inverse of [f] *)

Definition ap2 {C D E : Type} (f : C -> D -> E)
           {c c' : C} {d d' : D} (p : c = c') (q : d = d')
           : f c d = f c' d'
  := (ap (fun c => f c d) p) @ (ap (f c') q).

(* equivalent definition *)
Definition ap2' {C D E : Type} (f : C -> D -> E)
           {c c' : C} {d d' : D} (p : c = c') (q : d = d')
           : f c d = f c' d'
  := (ap (f c) q)  @ (ap (fun c => f c d') p).

Definition g {A B : Type} {x y : A * B} :
             (fst x = fst y) * (snd x = snd y) -> x = y
  := fun p => ap2 (fun a b => (a,b)) (fst p) (snd p).

(* Finally, we can prove the characterization *)
Theorem id_space_prod :  forall {A B : Type} (x y : A * B),
  (x = y) <~> ((fst x = fst y) * (snd x = snd y)).
Proof.
  intros A B x y.
  split with (equiv_fun := f).
  Check BuildIsEquiv.
  refine (BuildIsEquiv _ _ f g _ _ _).
  (* f . g = id *)
  unfold Sect. intro q.
  destruct q as [q1 q2].
  (* we cannot do induction on q1 or q2 at this point, as we don't
   have free endpoints. however, we use the induction on the product
   type to assume that [x] and [y] are pairs themselves. this way we
   can get rid of the dependency in the endpoints *)
  destruct x as [x1 x2]; destruct y as [y1 y2]; simpl in *.
  induction q1; induction q2.
  unfold g. unfold f. simpl. reflexivity.
  (* g . f = id *)
  unfold Sect; intro p.
  unfold f. unfold g. simpl. unfold ap2.
  induction p. simpl. reflexivity.
  (* adjointness *)
  intro p. simpl. induction p. simpl. reflexivity.
Qed.

(** Eckmann-Hilton *)

Lemma t1 {A : Type} {m n : A} : forall (p q : (idpath m) = (idpath m)),
  ap2 (fun x y => x @ y) p q = p @ q.
Proof.
  intros p q.
  unfold ap2.

  (* Here we need to prove that

     - [ap (fun x => x @ 1) p = p]
     - [ap (fun x => 1 @ x) p = p]

     Once again, we cannot do this directly, as [p] doesn't have
     free endpoints *)
  Check (ap idmap p = p).
  Check (ap (fun x => x @ 1) p).
  Check p.
  Check ((fun y => 1 @ y) = idmap).
  Abort.

Lemma ap_id1 {A : Type} {m : A} (k l : m = m) (p : k = l)
  : ap (fun x => x @ 1) p
    = (concat_p1 k) @ (p @ (concat_p1 l)^).
Proof.
  induction p. simpl.
  rewrite concat_1p. symmetry. apply concat_pV.
Qed.

Lemma ap_id1'' {A : Type} {m : A} (k l : m = m) (p : k = l)
  : ap (fun x => x @ 1) p
  = ((concat_p1 k) @ p) @ (concat_p1 l)^.
Proof.
  induction p. simpl.
  rewrite concat_pp_p.
  rewrite concat_1p. symmetry. apply concat_pV.
Qed.

Lemma ap_id2 {A : Type} {m : A} (k l : m = m) (p : k = l)
  : ap (fun x => 1 @ x) p
    = (concat_1p k) @ p @ (concat_1p l)^.
Proof.
  induction p. simpl.
  rewrite concat_p1. symmetry. apply concat_pV.
Qed.

Lemma t1 {A : Type} {m : A} : forall (p q : (idpath m) = (idpath m)),
  ap2 (fun x y => x @ y) p q = p @ q.
Proof.
  intros. unfold ap2. rewrite ap_id1.
  rewrite ap_id2. simpl.
  repeat (rewrite concat_p1).
  repeat (rewrite concat_1p).
  reflexivity.
Qed.

Lemma t2 {A : Type} {m : A} : forall (p q : (idpath m) = (idpath m)),
  ap2' (fun x y => x @ y) p q = q @ p.
Proof.
  intros. unfold ap2'. rewrite ap_id2.
  rewrite ap_id1. simpl.
  repeat (rewrite concat_p1).
  repeat (rewrite concat_1p).
  reflexivity.
Qed.

Lemma t3 {A : Type} {m : A} (k l : m = m) : forall (p q : k = l),
  ap2 (fun x y => x @ y) p q =
  ap2' (fun x y => x @ y) p q.
Proof.
  intros. induction p. unfold ap2. simpl.
  rewrite concat_1p.
  unfold ap2'. simpl.
  rewrite concat_p1.
  reflexivity.
Qed.

Theorem EckmannHilton {A : Type} :
  forall (m : A) (p q : (idpath m) = (idpath m)), p @ q = q @ p.
Proof.
  intros. rewrite <- t1. rewrite <- t2.
  rewrite t3. reflexivity.
Qed.

Definition whR {A : Type} {a b c : A}
  {p q : a = b} (al : p = q) (r : b = c) : p @ r = q @ r
  := match r with
       | 1 => ap (fun x => x @ 1) al
     end.
Definition whL {A : Type} {a b c : A}
  {r s : b = c} (p : a = b) (be : r = s)  : p @ r = p @ s.
induction p; apply (ap (fun x => 1 @ x) be). Qed.
  (* := match p with *)
  (*      | 1 => ap (fun x => 1 @ x) be *)
  (*    end. *)

author: co-dan

repo: hott-snippets

save_path: github-repos/coq/co-dan-hott-snippets


text:
(*
 Copyright 2022 ZhengPu Shi
  This file is part of coq-matrix. It is distributed under the MIT
  "expat license". You should have recieved a LICENSE file with it.

  purpose   : extension for Q (rational number).
  author    : ZhengPu Shi
  date      : 2022.04
*)

Require Export BasicConfig.

Require Export QArith Qround.
Open Scope Q.

(* ######################################################################### *)
(** ** Convertion between Q and other types *)

(** Z to Q *)
Definition Z2Q (z : Z) : Q := inject_Z z.

(** nat to Q *)
Definition nat2Q (n : nat) : Q := Z2Q (Z.of_nat n).

(** Q to Z *)
Definition Q2Z_ceiling (q : Q) : Z := Qceiling q.
Definition Q2Z_floor (q : Q) : Z := Qfloor q.

(* ######################################################################### *)
(** * Properties for Qeqb and Qeq *)

(** This axiom just for convenient printing and parsing, LIMITED USE IT.

  For example, 3#2 and 6#4 is equivalent, but they are not the same.
  We mainly use this axiom to ensure 3#2 = 6#4, but not to say 3=6 and 2=4.

  Be careful for use of any axiom!!
*)
Axiom Qeq_iff_eq : forall (a b : Q), Qeq a b <-> a = b.

Lemma Qneq_iff_neq : forall (a b : Q), ~(Qeq a b) <-> a <> b.
Proof.
  intros. split; intros.
  - intro. apply Qeq_iff_eq in H0. easy.
  - intro. apply Qeq_iff_eq in H0. easy.
Qed.

Lemma Qeqdec : @decidable Q.
Proof.
  intros a b.
  destruct (Qeq_dec a b) as [H|H] eqn : E1.
  - left. apply Qeq_iff_eq. auto.
  - right. intro. apply Qeq_iff_eq in H0. auto.
Defined.

Definition Qeqb := Qeq_bool.

Infix     "=="          := Qeq            : Q_scope.
Notation  "a != b"      := (~(a == b))    : Q_scope.
Infix     "=?"          := Qeqb           : Q_scope.

(** Reflection of (==) and (=?) *)
Lemma Qeqb_true_iff_equiv : forall x y, x =? y = true <-> x == y.
Proof. apply Qeq_bool_iff. Qed.

Lemma Qeqb_false_iff_equiv : forall x y, x =? y = false <-> x != y.
Proof.
  intros; split; intros.
  - intro. apply Qeqb_true_iff_equiv in H0. rewrite H in H0. easy.
  - destruct (Qeqb x y) eqn:E1; auto. apply Qeqb_true_iff_equiv in E1. easy.
Qed.

Lemma Qeqb_true_iff : forall x y, x =? y = true <-> x = y.
Proof.
  intros; split; intros.
  - apply Qeq_iff_eq. apply Qeqb_true_iff_equiv. auto.
  - apply Qeq_iff_eq in H. apply Qeqb_true_iff_equiv. auto.
Qed.

Lemma Qeqb_false_iff : forall x y, x =? y = false <-> x <> y.
Proof.
  intros; split; intros.
  - intro. apply Qeq_iff_eq in H0. apply Qeqb_false_iff_equiv in H. easy.
  - apply Qeqb_false_iff_equiv. apply Qneq_iff_neq. auto.
Qed.

(** (==) is equivalence relation *)
Lemma Qeq_equiv : equivalence _ Qeq.
Proof. split;intro;intros;try easy. rewrite H;try easy. Qed.

(** ( + ) is proper function about (==) *)
Lemma Qplus_Qeq_proper : Proper (Qeq ==> Qeq ==> Qeq) Qplus.
Proof. intro;intros. intro;intros. rewrite H,H0;easy. Qed.

(** ( * ) is proper function about (==) *)
Lemma Qmult_Qeq_proper : Proper (Qeq ==> Qeq ==> Qeq) Qmult.
Proof. intro;intros. intro;intros. rewrite H,H0;easy. Qed.

(** ( - a) is proper function about (==) *)
Lemma Qopp_Qeq_proper : Proper (Qeq ==> Qeq) Qopp.
Proof. intro; intros. rewrite H; easy. Qed.

(* ######################################################################### *)
(** ** Others *)

(** This is needed by field_theory (EQ version, original is equiv version) *)
Lemma Qmult_inv_l_EQ : forall p : Q, p <> 0 -> /p * p = 1.
Proof.
  intros. apply Qeq_iff_eq. rewrite Qmult_comm.
  apply Qmult_inv_r. apply Qneq_iff_neq. auto.
Qed.

(** ** sqrt of Q *)

Definition Qsqrt (q : Q) := Qmake (Z.sqrt (Qnum q)) (Pos.sqrt (Qden q)).

(* Example *)
(* Compute Qsqrt 1.21. *)

author: zhengpushi

repo: coq-matrix

save_path: github-repos/coq/zhengpushi-coq-matrix


text:
Require Import aarch64_types aarch64.
Require Import ZArith Sail.Prompt_monad Sail.Prompt bbv.Word Sail.Real Sail.Values.

Local Open Scope Z.

(*
(*<*)
(* Author: Thomas Bauereiss *)
theory Address_Translation_Orig
  imports "Sail-AArch64.Aarch64_lemmas"
begin
(*>*)

section \<open>Critical parts of original definition\<close>

text \<open>We copy a few parts of the translation table walk function in the original model,
in particular the table walk loop, into individual definitions in order to reason about them
separately.  Note that this just serves to make it easier to state some of the auxiliary
lemmas; the main proof refers only to the original model.\<close>
*)

Ltac remove_binders t :=
  let rec aux t :=
  lazymatch t with
  | (fun (x : ?T) => @?X x) =>
    let t' :=
      constr:(fun (x : T) =>
        ltac:(let t := eval cbv beta in (X x) in
              let r := (aux t) in
              exact r))
    in lazymatch t' with
    | (fun _ => ?X) => X
    | _ => t'
    end
  | ?X => X
  end in
  aux t.
(*
From Ltac2 Require Ltac2 Std Message.

Section loopbodydef.
Set Default Proof Mode "Classic".
Import Std.
Ltac2 fixdeltafn x := { rBeta := false; rMatch := false; rFix := true; rCofix := false; rZeta := false; rDelta := true; rConst := [x] }.
Ltac2 betafl := { rBeta := true; rMatch := false; rFix := false; rCofix := false; rZeta := false; rDelta := false; rConst := [] }.

(* cbn is good for fixpoints, terrible for lone definitions *)
Ltac2 loop_body fn appliedfn :=
  let fnbody := eval_cbn (fixdeltafn fn) appliedfn in
(*  let fnbody := eval hnf in fnbody in  TODO: hnf is too much *)
  let rec aux t :=
    (* TODO somehow try to keep original variable names *)
    (*let x1 := fresh "x1" in
    let x2 := fresh "x2" in*)
    lazy_match! t with
    | context [whileMT ?vars _ _ ?body] => body
    | context [untilMT ?vars _ _ ?body] => body
    | fun _ => ?x => aux x
    | (fun x1 : ?ty => @?x x1) =>
      constr:(fun (x1 : $ty) =>
                ltac2:(let t := eval_cbv betafl '($x &x1) in
                       let r := (aux t) in
                       exact $r))
(*
  | (fix foo (x1 : ?T1) (x2 : ?T2 x1) {struct x2} := @?X x1 x2) =>
      constr:(fun (x1 : T1) (x2 : T2 x1) =>
        ltac:(let t := eval cbv beta in (X x1 x2) in
              let r := (aux t) in
              exact r))*)
    | bind _ _ =>
      match! t with
      | bind ?m _ => aux m
      | bind _ ?f => aux f
      end
    | bind0 _ _ =>
      match! t with
      | bind0 ?m _ => aux m
      | bind0 _ ?m => aux m
      end
    | try_catch _ _ =>
      match! t with
      | try_catch ?m _ => aux m
      | try_catch _ ?h => aux h
      end
    | catch_early_return ?m => aux m
    | liftR ?m => aux m
    | try_catchR _ _ =>
      match! t with
      | try_catchR ?m _ => aux m
      | try_catchR _ ?h => aux h
      end
    | let x1 := _ in @?x x1 =>
      constr:(fun x1 =>
        ltac2:(let t := eval_cbv betafl '($x &x1) in
               let r := (aux t) in
               exact $r))
    | let '(x1, x2) := _ in @?x x1 x2 =>
      constr:(fun x1 x2 =>
        ltac2:(let t := eval_cbv betafl '($x &x1 &x2) in
               let r := (aux t) in
               exact $r))
    | let '(existT _ x1 x2) := _ in @?x x1 x2 =>
      constr:(fun x1 x2 =>
        ltac2:(let t := eval_cbv betafl '($x &x1 &x2) in
               let r := (aux t) in
               exact $r))
    | if ?g then _ else _ =>
      match! t with
      | if _ then ?x else _ => aux x
      | if _ then _ else ?x => aux x
      end
    | match _ with left _ => _ | right _ => _ end =>
      match! t with
      | match _ with left x1 => @?x x1 | right _ => _ end =>
          constr:(fun x1 =>
            ltac2:(let t := eval_cbv betafl '($x &x1) in
                   let r := (aux t) in
                   exact $r))
      | match _ with left _ => _ | right x1 => @?x x1 end =>
          constr:(fun x1 =>
            ltac2:(let t := eval_cbv betafl '($x &x1) in
                   let r := (aux t) in
                   exact $r))
      end
(*    | ?x _ => (*idtac "app" x;*) fail
    | _ =>
      match! t with
      | ?x => is_var x; idtac "var"
      | ?x => let ty := type of x in idtac "mystery term" x "of type" ty
      end*)
    end in
  aux fnbody.

End loopbodydef.
*)
(*
Goal forall (x : Sail.Values.mword 16), True.
  intro x.
  set (tm := _ChooseRandomNonExcludedTag x).
cbn delta [_ChooseRandomNonExcludedTag] in tm.
cbv delta [_ChooseRandomNonExcludedTag] in tm.
let t := loop_body _ChooseRandomNonExcludedTag (_ChooseRandomNonExcludedTag x) in
idtac t.
Abort.*)
(*Require Import String.
Local Open Scope Z.

Fixpoint test (x1 : Z) (b : bool) (_acc : Acc (Zwf 0) x1) {struct _acc} : M Z
with foo (x : Z) (_acc : Acc (Zwf 0) x) {struct _acc} : M Z.
exact (  assert_exp' (Z.geb x1 0) "bad" >>= fun _ =>
  ((assert_exp (x1 >=? 1) "bad" >>
               let '(a,b,c) := (3,4,5) in
               ((aarch64_extras.undefined_nat tt)) >>= fun '(existT _ w__23 _ : {n : Z & ArithFact (n >= 0)}) =>
  if Sumbool.sumbool_of_bool (2 <=? x1) then
    returnm (1,build_ex 2,3) >>= fun '((y,existT _ z _,w) : Z * {x : Z & ArithFact (x <= x1)} * Z) =>
                        whileMT (x1 + z) (fun x => x) (fun x => returnm (Z.geb x 1)) (fun x => returnm (x - 1 + a - y))
  else returnm 5) : M Z)).
exact (returnm x).
Defined.

Require LoopExtract.

Definition xyz (x : Z) `{ArithFact (x > 5)} := x.
(*Goal forall x : Z, True.
  intros x.
Set Debug Ltac.
  let t := constr:(fun (_: x > 5) => xyz x) in
  let rec f t :=
      lazymatch t with
      | fun (_ : ?T) => ?X => constr:(fun _ : T => ltac:(let t := (f X) in exact t))
      | fun (x : ?T) => @?X x => constr:(fun x : T => ltac:(let t := eval cbv beta in (X x) in let t := (f t) in exact t))
      | _ => constr:(t + 1)
      end in
  let t := f t in
  idtac t.
Abort.*) (*
  match t with
  | fun (x : ?T) => @?X x => let t' := constr:(fun x : T => ltac:(let t := eval cbv beta in (X x) in
    match t with
    | fun (x : ?T) => @?X x => let t' := constr:(fun x : T => ltac:(let t := eval cbv beta in (X x) in exact t)) in exact t'
    end)) in idtac t'
  end.
*)
Goal forall (xx1 : Z) (b:bool) (_acc : Acc (Zwf 0) xx1), True.
  intros xx1 b [_acc].

  let t := ltac2:(LoopExtract.loop_body  reference:(&test) constr:(test xx1 b (Acc_intro xx1 _acc))) in
  set (x := t).

  let t0 := eval cbv delta [x] in x in
  let t := remove_binders t0 in
  idtac t.

Abort.

Definition TranslationTableWalk_loop_body
 (singlepriv : bool) (apply_nvnv1_effect : bool) (hierattrsdisabled : bool) (largegrain : bool)
 (outputsize : Z) (ipaddress : word 52) (reversedescriptors : bool) (s2fs1walk : bool)
 (iswrite : bool) (acctype : AccType) (vaddress : word 64) (secondstage : bool)
 (inputaddr : word 64) (grainsize : Z) (stride : Z)
 : AccessDescriptor * Z * Z * word 2 * word 52 * bool * word 64 * AddressDescriptor *
   AddressDescriptor * bool * Z * word 1 * word 1 * TLBRecord * word 1 ->
   monad register_value (AccessDescriptor *
                                          Z * Z * word 2 *
                                                       word 52 *
                                                       bool *
                                                       word 64 *
                                                       AddressDescriptor *
                                                       AddressDescriptor * bool * Z * word 1 * word 1 * TLBRecord * word 1)
                                          (TLBRecord + exception).
assert (Acc (Zwf 0) 1) as acc.
apply Zwf_guarded.
generalize (Sail.Operators_mwords.vec_of_bits (Sail.Values.B0::nil)). intro s1_nonsecure.
generalize 1. intro size.
destruct acc as [acc].

let t := loop_body  _rec_AArch64_TranslationTableWalk
           (_rec_AArch64_TranslationTableWalk ipaddress s1_nonsecure vaddress acctype iswrite secondstage s2fs1walk size 1 (Acc_intro 1 acc)) in
let t := remove_binders t in
set (body := t).

assert (H1 : (1 >=? 0) = true) by reflexivity.

let t := eval cbv delta [full] in full in
    let t := remove_binders t in
    let t := eval cbv beta in (t H1) in
    match t with
    | context [H1] => idtac "found"
    | _ => idtac "not present"
    end.
idtac t.

let t := loop_body  _rec_AArch64_TranslationTableWalk
           (_rec_AArch64_TranslationTableWalk ipaddress s1_nonsecure vaddress acctype iswrite secondstage s2fs1walk size 1 (Acc_intro 1 acc)) in
let t := remove_binders t in
set (body := t).

(*
Goal True.

let t := loop_body _rec_AArch64_TranslationTableWalk in
idtac t.
*)
Definition TranslationTableWalk_loop_body
 (singlepriv : bool) (apply_nvnv1_effect : bool) (hierattrsdisabled : bool) (largegrain : bool)
 (outputsize : Z) (ipaddress : word 52) (reversedescriptors : bool) (s2fs1walk : bool)
 (iswrite : bool) (acctype : AccType) (vaddress : word 64) (secondstage : bool)
 (inputaddr : word 64) (grainsize : Z) (stride : Z)
 : AccessDescriptor * Z * Z * word 2 * word 52 * bool * word 64 * AddressDescriptor *
   AddressDescriptor * bool * Z * word 1 * word 1 * TLBRecord * word 1 ->
   monad register_value (AccessDescriptor *
                                          Z * Z * word 2 *
                                                       word 52 *
                                                       bool *
                                                       word 64 *
                                                       AddressDescriptor *
                                                       AddressDescriptor * bool * Z * word 1 * word 1 * TLBRecord * word 1)
                                          (TLBRecord + exception).
let t := loop_body _rec_AArch64_TranslationTableWalk in
exact t.
admit.
Admitted.

(*let s1_nonsecure := fresh "s1_nonsecure" in
let size := fresh "size" in
let _reclimit := fresh "_reclimit" in
let _acc := fresh "_acc" in
let s1_nonsecure := constr:(WS false WO) in
let size := constr:(1%Z:Z) in
let _reclimit := constr:(1%Z) in
let _acc := constr:(Zwf_guarded 1) in
let fn := constr:(_rec_AArch64_TranslationTableWalk ipaddress s1_nonsecure vaddress acctype iswrite secondstage s2fs1walk size _reclimit _acc) in
let fnbody := eval simpl in fn in
match fnbody with
| context [untilMT _ _ _ ?body] => exact body
end.
  TranslationTableWalk_loop_body                =
            (\<lambda> varstup .
            (let (accdesc,
                 addrselectbottom,
                 addrselecttop,
                 ap_table,
                 baseaddress,
                 blocktranslate,
                 desc,
                 descaddr,
                 descaddr2,
                 hwupdatewalk,
                 level,
                 ns_table,
                 pxn_table,
                 result,
                 xn_table) = varstup in
              (let addrselectbottom =
                ((((((( 3 :: int)::ii) - ((ex_int level)))) * ((ex_int stride))))
                  +
                  ((ex_int grainsize))) in
              liftR ((ZeroExtend_slice_append (( 52 :: int)::ii) inputaddr addrselectbottom
                        ((((((ex_int addrselecttop)) - ((ex_int addrselectbottom))))
                            +
                            (( 1 :: int)::ii))) (vec_of_bits [B0,B0,B0]  ::  3 Word.word)
                       :: ( 52 Word.word) M)) \<bind> (\<lambda> (index1 :: 52 bits) .
              (let (tmp_210 :: FullAddress) = ((AddressDescriptor_paddress   descaddr)) in
              (let tmp_210 =
                ((tmp_210 (|
                  FullAddress_physicaladdress := ((or_vec baseaddress index1  ::  52 Word.word))|))) in
              (let descaddr = ((descaddr (| AddressDescriptor_paddress := tmp_210 |))) in
              (let (tmp_220 :: FullAddress) = ((AddressDescriptor_paddress   descaddr)) in
              (let tmp_220 = ((tmp_220 (| FullAddress_NS := ns_table |))) in
              (let descaddr = ((descaddr (| AddressDescriptor_paddress := tmp_220 |))) in
              or_boolM (return secondstage)
                (liftR (HasS2Translation () ) \<bind> (\<lambda> (w__143 :: bool) .  return ((\<not> w__143)))) \<bind> (\<lambda> (w__144 ::
                bool) .
              (if w__144 then
                 (let (descaddr2 :: AddressDescriptor) = descaddr in
                 return (descaddr2, hwupdatewalk, result))
               else
                 (let hwupdatewalk = False in
                 liftR (AArch64_SecondStageWalk descaddr vaddress acctype iswrite (( 8 :: int)::ii)
                          hwupdatewalk) \<bind> (\<lambda> (w__145 :: AddressDescriptor) .
                 (let descaddr2 = w__145 in
                 (if ((IsFault descaddr2)) then
                    (let (tmp_230 :: AddressDescriptor) = ((TLBRecord_addrdesc   result)) in
                    (let tmp_230 =
                      ((tmp_230 (| AddressDescriptor_fault := ((AddressDescriptor_fault   descaddr2))|))) in
                    (let result = ((result (| TLBRecord_addrdesc := tmp_230 |))) in
                    (early_return result :: (unit, TLBRecord) MR) \<then> return result)))
                  else return result) \<bind> (\<lambda> (result :: TLBRecord) .
                 return (descaddr2, hwupdatewalk, result)))))) \<bind> (\<lambda> varstup .  (let ((descaddr2 ::
                AddressDescriptor), (hwupdatewalk :: bool), (result :: TLBRecord)) = varstup in
              liftR ((ZeroExtend__1 (( 64 :: int)::ii) vaddress  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__146 :: 64 bits) .
              (let descaddr2 = ((descaddr2 (| AddressDescriptor_vaddress := w__146 |))) in
              liftR (CreateAccessDescriptorPTW acctype secondstage s2fs1walk level) \<bind> (\<lambda> (w__147 ::
                AccessDescriptor) .
              (let accdesc = w__147 in
              liftR ((aget__Mem descaddr2 (( 8 :: int)::ii) accdesc  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__148 :: 64
                bits) .
              (let desc = w__148 in
              (if reversedescriptors then liftR ((BigEndianReverse desc  :: ( 64 Word.word) M))
               else return desc) \<bind> (\<lambda> (desc :: 64 bits) .
              (if (((((((vec_of_bits [access_vec_dec desc (( 0 :: int)::ii)]  ::  1 Word.word) = (vec_of_bits [B0]  ::  1 Word.word)))) \<or> ((((((((slice desc (( 0 :: int)::ii) (( 2 :: int)::ii)  ::  2 Word.word)) = (vec_of_bits [B0,B1]  ::  2 Word.word)))) \<and> (((((ex_int level)) = (( 3 :: int)::ii))))))))))
               then
                 (let (tmp_240 :: AddressDescriptor) = ((TLBRecord_addrdesc   result)) in
                 liftR (AArch64_TranslationFault ipaddress level acctype iswrite secondstage
                          s2fs1walk) \<bind> (\<lambda> (w__150 :: FaultRecord) .
                 (let tmp_240 = ((tmp_240 (| AddressDescriptor_fault := w__150 |))) in
                 (let result = ((result (| TLBRecord_addrdesc := tmp_240 |))) in
                 (early_return result :: (unit, TLBRecord) MR) \<then>
                 return (addrselecttop,
                         ap_table,
                         baseaddress,
                         blocktranslate,
                         level,
                         ns_table,
                         pxn_table,
                         result,
                         xn_table)))))
               else if ((((((((slice desc (( 0 :: int)::ii) (( 2 :: int)::ii)  ::  2 Word.word)) = (vec_of_bits [B0,B1]  ::  2 Word.word)))) \<or> (((((ex_int level)) = (( 3 :: int)::ii)))))))
               then
                 (let (blocktranslate :: bool) = True in
                 return (addrselecttop,
                         ap_table,
                         baseaddress,
                         blocktranslate,
                         level,
                         ns_table,
                         pxn_table,
                         result,
                         xn_table))
               else
                 or_boolM
                   (return ((((((((((ex_int outputsize)) < (( 52 :: int)::ii))) \<and> largegrain))) \<and> ((\<not> ((IsZero ((slice desc (( 12 :: int)::ii) (( 4 :: int)::ii)  ::  4 Word.word))))))))))
                   (and_boolM (return ((((ex_int outputsize)) < (( 48 :: int)::ii))))
                      (liftR (IsZero_slice desc outputsize
                                ((((- ((ex_int outputsize)))) + (( 48 :: int)::ii)))) \<bind> (\<lambda> (w__151 ::
                         bool) .
                       return ((\<not> w__151))))) \<bind> (\<lambda> (w__153 :: bool) .
                 if w__153 then
                   (let (tmp_250 :: AddressDescriptor) = ((TLBRecord_addrdesc   result)) in
                   liftR (AArch64_AddressSizeFault ipaddress level acctype iswrite secondstage
                            s2fs1walk) \<bind> (\<lambda> (w__154 :: FaultRecord) .
                   (let tmp_250 = ((tmp_250 (| AddressDescriptor_fault := w__154 |))) in
                   (let result = ((result (| TLBRecord_addrdesc := tmp_250 |))) in
                   (early_return result :: (unit, TLBRecord) MR) \<then>
                   return (addrselecttop,
                           ap_table,
                           baseaddress,
                           blocktranslate,
                           level,
                           ns_table,
                           pxn_table,
                           result,
                           xn_table)))))
                 else
                   (let gsz = grainsize in
                   liftR (assert_exp True ('''')) \<then>
                   ((let (baseaddress :: 52 bits) =
                     (if (((((ex_int outputsize)) = (( 52 :: int)::ii)))) then
                       (concat_vec ((slice desc (( 12 :: int)::ii) (( 4 :: int)::ii)  ::  4 Word.word))
                          ((slice_zeros_concat
                              ((((((- gsz)) + (( 48 :: int)::ii))) + gsz)) desc
                              gsz ((((- gsz)) + (( 48 :: int)::ii))) gsz
                             ::  48 Word.word))
                         ::  52 Word.word)
                     else
                       (place_slice (( 52 :: int)::ii) desc gsz ((((- gsz)) + (( 48 :: int)::ii)))
                          gsz
                         ::  52 Word.word)) in
                   (let (ns_table :: 1 bits) =
                     (if ((\<not> secondstage)) then
                       (or_vec ns_table (vec_of_bits [access_vec_dec desc (( 63 :: int)::ii)]  ::  1 Word.word)
                         ::  1 Word.word)
                     else ns_table) in
                   (let ((ap_table :: 2 bits), (pxn_table :: 1 bits), (xn_table :: 1 bits)) =
                     (if (((((\<not> secondstage)) \<and> ((\<not> hierattrsdisabled))))) then
                       (let (ap_table :: 2 bits) =
                         ((set_slice (( 2 :: int)::ii) (( 1 :: int)::ii) ap_table (( 1 :: int)::ii)
                            ((or_vec (vec_of_bits [access_vec_dec ap_table (( 1 :: int)::ii)]  ::  1 Word.word)
                                (vec_of_bits [access_vec_dec desc (( 62 :: int)::ii)]  ::  1 Word.word)
                               ::  1 Word.word))
                           ::  2 Word.word)) in
                       (let ((pxn_table :: 1 bits), (xn_table :: 1 bits)) =
                         (if apply_nvnv1_effect then
                           (let (pxn_table :: 1 bits) =
                             ((or_vec pxn_table
                                (vec_of_bits [access_vec_dec desc (( 60 :: int)::ii)]  ::  1 Word.word)
                               ::  1 Word.word)) in
                           (pxn_table, xn_table))
                         else
                           (let (xn_table :: 1 bits) =
                             ((or_vec xn_table
                                (vec_of_bits [access_vec_dec desc (( 60 :: int)::ii)]  ::  1 Word.word)
                               ::  1 Word.word)) in
                           (pxn_table, xn_table))) in
                       (let ((ap_table :: 2 bits), (pxn_table :: 1 bits)) =
                         (if ((\<not> singlepriv)) then
                           (let ((ap_table :: 2 bits), (pxn_table :: 1 bits)) =
                             (if ((\<not> apply_nvnv1_effect)) then
                               (let (pxn_table :: 1 bits) =
                                 ((or_vec pxn_table
                                    (vec_of_bits [access_vec_dec desc (( 59 :: int)::ii)]  ::  1 Word.word)
                                   ::  1 Word.word)) in
                               (let (ap_table :: 2 bits) =
                                 ((set_slice (( 2 :: int)::ii) (( 1 :: int)::ii) ap_table (( 0 :: int)::ii)
                                    ((or_vec
                                        (vec_of_bits [access_vec_dec ap_table (( 0 :: int)::ii)]  ::  1 Word.word)
                                        (vec_of_bits [access_vec_dec desc (( 61 :: int)::ii)]  ::  1 Word.word)
                                       ::  1 Word.word))
                                   ::  2 Word.word)) in
                               (ap_table, pxn_table)))
                             else (ap_table, pxn_table)) in
                           (ap_table, pxn_table))
                         else (ap_table, pxn_table)) in
                       (ap_table, pxn_table, xn_table))))
                     else (ap_table, pxn_table, xn_table)) in
                   (let (level :: ii) = (((ex_int level)) + (( 1 :: int)::ii)) in
                   (let (addrselecttop :: ii) = (((ex_int addrselectbottom)) - (( 1 :: int)::ii)) in
                   (let (blocktranslate :: bool) = False in
                   return (addrselecttop,
                           ap_table,
                           baseaddress,
                           blocktranslate,
                           level,
                           ns_table,
                           pxn_table,
                           result,
                           xn_table))))))))))) \<bind> (\<lambda> varstup .  (let ((addrselecttop :: ii), (ap_table :: 2
                bits), (baseaddress :: 52 bits), (blocktranslate :: bool), (level :: ii), (ns_table :: 1
                bits), (pxn_table :: 1 bits), (result :: TLBRecord), (xn_table :: 1 bits)) = varstup in
              return (accdesc,
                      addrselectbottom,
                      addrselecttop,
                      ap_table,
                      baseaddress,
                      blocktranslate,
                      desc,
                      descaddr,
                      descaddr2,
                      hwupdatewalk,
                      level,
                      ns_table,
                      pxn_table,
                      result,
                      xn_table)))))))))))))))))))))))
*)

Definition TranslationTableWalk_loop_cond {rv e} : AccessDescriptor * Z * Z * word 2 * word 52 * bool * word 64 * AddressDescriptor *
   AddressDescriptor * bool * Z * word 1 * word 1 * TLBRecord * word 1 -> monad rv bool e :=
            (fun varstup =>
            (let '(accdesc,
                 addrselectbottom,
                 addrselecttop,
                 ap_table,
                 baseaddress,
                 blocktranslate,
                 desc,
                 descaddr,
                 descaddr2,
                 hwupdatewalk,
                 level,
                 ns_table,
                 pxn_table,
                 result,
                 xn_table) := varstup in
              returnm blocktranslate)).

Local Open Scope Z.

Definition TranslationTableWalk_loop_termination_precond
 (vars : AccessDescriptor * Z * Z * word 2 * word 52 * bool * word 64 * AddressDescriptor *
   AddressDescriptor * bool * Z * word 1 * word 1 * TLBRecord * word 1 ) : Prop :=
     match vars with (accdesc,
                 addrselectbottom,
                 addrselecttop,
                 ap_table,
                 baseaddress,
                 blocktranslate,
                 desc,
                 descaddr,
                 descaddr2,
                 hwupdatewalk,
                 level,
                 ns_table,
                 pxn_table,
                 result,
                 xn_table) => level >= 0 /\ level < 4
     end.

(*
Definition
  "TranslationTableWalk_loop_variant vars =
     (case vars of (accdesc,
                 addrselectbottom,
                 addrselecttop,
                 ap_table,
                 baseaddress,
                 blocktranslate,
                 desc,
                 descaddr,
                 descaddr2,
                 hwupdatewalk,
                 level,
                 ns_table,
                 pxn_table,
                 result,
                 xn_table) \<Rightarrow> 4 - nat level)"
*)
*)
Import List.ListNotations.
Import Sail.Values Sail.Operators_mwords.

Definition calc_outputsize (PS : mword 3) (largegrain : bool) : Z :=
  if eq_vec PS (vec_of_bits [B0; B0; B0]) then 32
  else if eq_vec PS (vec_of_bits [B0; B0; B1]) then 36
  else if eq_vec PS (vec_of_bits [B0; B1; B0]) then 40
  else if eq_vec PS (vec_of_bits [B0; B1; B1]) then 42
  else if eq_vec PS (vec_of_bits [B1; B0; B0]) then 44
  else if eq_vec PS (vec_of_bits [B1; B0; B1]) then 48
  else if eq_vec PS (vec_of_bits [B1; B1; B0]) then if largegrain then 52 else 48 else 48.

Lemma calc_outputsize_bounds (*[simp]:*) PS largegrain :
  32 <= calc_outputsize PS largegrain <= 52.
(*  "52 < calc_outputsize PS largegrain \<longleftrightarrow> False"
  by (auto simp: calc_outputsize_def)*)
unfold calc_outputsize.
repeat match goal with |- context [if ?c then _ else _] => destruct c end; omega.
Qed.

(*
definition Parameters_EL0 where
  "Parameters_EL0 descaddr secondstage top1 (inputaddr :: 64 word) c =
     (if ((((vec_of_bits [access_vec_dec inputaddr top1]  ::  1 Word.word) = (vec_of_bits [B0]  ::  1 Word.word)))) then
        liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__82 :: 64 bits) .
        (let inputsize =
          ((( 64 :: int)::ii) - ((Word.uint ((slice w__82 (( 0 :: int)::ii) (( 6 :: int)::ii)  ::  6 Word.word))))) in
        liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__83 :: 64 bits) .
        (let largegrain =
          (((slice w__83 (( 14 :: int)::ii) (( 2 :: int)::ii)  ::  2 Word.word)) = (vec_of_bits [B0,B1]  ::  2 Word.word)) in
        liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__84 :: 64 bits) .
        (let midgrain =
          (((slice w__84 (( 14 :: int)::ii) (( 2 :: int)::ii)  ::  2 Word.word)) = (vec_of_bits [B1,B0]  ::  2 Word.word)) in
        (let inputsize_max =
          (if (((((Have52BitVAExt () )) \<and> largegrain))) then (( 52 :: int)::ii)
          else (( 48 :: int)::ii)) in
        (if ((((ex_int inputsize)) > ((ex_int inputsize_max)))) then
           (let c = (ConstrainUnpredictable Unpredictable_RESTnSZ) in
           liftR (assert_exp ((((((c = Constraint_FORCE))) \<or> (((c = Constraint_FAULT)))))) ('''')) \<then>
           ((let (inputsize :: ii) =
             (if (((c = Constraint_FORCE))) then inputsize_max
             else inputsize) in
           return (c, inputsize))))
         else return (c, inputsize)) \<bind> (\<lambda> varstup .  (let ((c :: Constraint), (inputsize ::
          ii)) = varstup in
        (let inputsize_min = ((( 64 :: int)::ii) - (( 39 :: int)::ii)) in
        (if ((((ex_int inputsize)) < ((ex_int inputsize_min)))) then
           (let c = (ConstrainUnpredictable Unpredictable_RESTnSZ) in
           liftR (assert_exp ((((((c = Constraint_FORCE))) \<or> (((c = Constraint_FAULT)))))) ('''')) \<then>
           ((let (inputsize :: ii) =
             (if (((c = Constraint_FORCE))) then inputsize_min
             else inputsize) in
           return inputsize)))
         else return inputsize) \<bind> (\<lambda> (inputsize :: ii) .
        and_boolM
          (return (((((((ex_int inputsize)) \<ge> ((ex_int inputsize_min)))) \<and> ((((ex_int inputsize)) \<le> ((ex_int inputsize_max))))))))
          (liftR ((IsZero_slice inputaddr inputsize
                     ((((((ex_int top1)) - ((ex_int inputsize)))) +
                         (( 1 :: int)::ii)))))) \<bind> (\<lambda> (w__86 :: bool) .
        (let basefound = w__86 in
        liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__87 :: 64 bits) .
        (let disabled =
          ((vec_of_bits [access_vec_dec w__87 (( 7 :: int)::ii)]  ::  1 Word.word) = (vec_of_bits [B1]  ::  1 Word.word)) in
        liftR ((read_reg TTBR0_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__88 :: 64 bits) .
        (let baseregister = w__88 in
        liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__89 :: 64 bits) .
        liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__90 :: 64 bits) .
        liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__91 :: 64 bits) .
        liftR (WalkAttrDecode ((slice w__89 (( 12 :: int)::ii) (( 2 :: int)::ii)  ::  2 Word.word))
                 ((slice w__90 (( 10 :: int)::ii) (( 2 :: int)::ii)  ::  2 Word.word))
                 ((slice w__91 (( 8 :: int)::ii) (( 2 :: int)::ii)  ::  2 Word.word)) secondstage) \<bind> (\<lambda> (w__92 ::
          MemoryAttributes) .
        (let descaddr = ((descaddr (| AddressDescriptor_memattrs := w__92 |))) in
        and_boolM (return ((AArch64_HaveHPDExt () )))
          (liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__93 :: 64 bits) .
           return ((((vec_of_bits [access_vec_dec w__93 (( 41 :: int)::ii)]  ::  1 Word.word) = (vec_of_bits [B1]  ::  1 Word.word)))))) \<bind> (\<lambda> (w__94 :: bool) .
        (let (hierattrsdisabled :: bool) = w__94 in
        return (basefound,
                baseregister,
                descaddr,
                disabled,
                hierattrsdisabled,
                inputsize,
                largegrain,
                midgrain)))))))))))))))))))))))))
      else
        liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__95 :: 64 bits) .
        (let inputsize =
          ((( 64 :: int)::ii) - ((Word.uint ((slice w__95 (( 16 :: int)::ii) (( 6 :: int)::ii)  ::  6 Word.word))))) in
        liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__96 :: 64 bits) .
        (let largegrain =
          (((slice w__96 (( 30 :: int)::ii) (( 2 :: int)::ii)  ::  2 Word.word)) = (vec_of_bits [B1,B1]  ::  2 Word.word)) in
        liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__97 :: 64 bits) .
        (let midgrain =
          (((slice w__97 (( 30 :: int)::ii) (( 2 :: int)::ii)  ::  2 Word.word)) = (vec_of_bits [B0,B1]  ::  2 Word.word)) in
        (let inputsize_max =
          (if (((((Have52BitVAExt () )) \<and> largegrain))) then (( 52 :: int)::ii)
          else (( 48 :: int)::ii)) in
        (if ((((ex_int inputsize)) > ((ex_int inputsize_max)))) then
           (let c = (ConstrainUnpredictable Unpredictable_RESTnSZ) in
           liftR (assert_exp ((((((c = Constraint_FORCE))) \<or> (((c = Constraint_FAULT)))))) ('''')) \<then>
           ((let (inputsize :: ii) =
             (if (((c = Constraint_FORCE))) then inputsize_max
             else inputsize) in
           return (c, inputsize))))
         else return (c, inputsize)) \<bind> (\<lambda> varstup .  (let ((c :: Constraint), (inputsize ::
          ii)) = varstup in
        (let inputsize_min = ((( 64 :: int)::ii) - (( 39 :: int)::ii)) in
        (if ((((ex_int inputsize)) < ((ex_int inputsize_min)))) then
           (let c = (ConstrainUnpredictable Unpredictable_RESTnSZ) in
           liftR (assert_exp ((((((c = Constraint_FORCE))) \<or> (((c = Constraint_FAULT)))))) ('''')) \<then>
           ((let (inputsize :: ii) =
             (if (((c = Constraint_FORCE))) then inputsize_min
             else inputsize) in
           return inputsize)))
         else return inputsize) \<bind> (\<lambda> (inputsize :: ii) .
        and_boolM
          (return (((((((ex_int inputsize)) \<ge> ((ex_int inputsize_min)))) \<and> ((((ex_int inputsize)) \<le> ((ex_int inputsize_max))))))))
          (liftR ((IsOnes_slice inputaddr inputsize
                     ((((((ex_int top1)) - ((ex_int inputsize)))) +
                         (( 1 :: int)::ii)))))) \<bind> (\<lambda> (w__99 :: bool) .
        (let basefound = w__99 in
        liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__100 :: 64 bits) .
        (let disabled =
          ((vec_of_bits [access_vec_dec w__100 (( 23 :: int)::ii)]  ::  1 Word.word) = (vec_of_bits [B1]  ::  1 Word.word)) in
        liftR ((read_reg TTBR1_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__101 :: 64 bits) .
        (let baseregister = w__101 in
        liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__102 :: 64 bits) .
        liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__103 :: 64 bits) .
        liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__104 :: 64 bits) .
        liftR (WalkAttrDecode ((slice w__102 (( 28 :: int)::ii) (( 2 :: int)::ii)  ::  2 Word.word))
                 ((slice w__103 (( 26 :: int)::ii) (( 2 :: int)::ii)  ::  2 Word.word))
                 ((slice w__104 (( 24 :: int)::ii) (( 2 :: int)::ii)  ::  2 Word.word)) secondstage) \<bind> (\<lambda> (w__105 ::
          MemoryAttributes) .
        (let descaddr = ((descaddr (| AddressDescriptor_memattrs := w__105 |))) in
        and_boolM (return ((AArch64_HaveHPDExt () )))
          (liftR ((read_reg TCR_EL1_ref  :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__106 :: 64 bits) .
           return ((((vec_of_bits [access_vec_dec w__106 (( 42 :: int)::ii)]  ::  1 Word.word) = (vec_of_bits [B1]  ::  1 Word.word)))))) \<bind> (\<lambda> (w__107 :: bool) .
        (let (hierattrsdisabled :: bool) = w__107 in
        return (basefound,
                baseregister,
                descaddr,
                disabled,
                hierattrsdisabled,
                inputsize,
                largegrain,
                midgrain))))))))))))))))))))))))))"
*)
Definition calc_startlevel inputsize grainsize stride :=
  Z.sub 4 (round_up (div_real (to_real (Z.sub inputsize grainsize)) (to_real stride))).

Definition calc_baseaddress (baseregister : mword 64) baselowerbound outputsize `{ArithFact (baselowerbound >=? 0)} :=
  if sumbool_of_bool ((Z.eqb outputsize 52)) then
    let 'z :=
        projT1
          (build_ex
             (if sumbool_of_bool ((Z.ltb baselowerbound 6)) then 6
              else baselowerbound)
           : {n : Z & ArithFact (n >=? 0)}) in
    liftR (assert_exp' (Z.geb (Z.add (Z.opp (projT1 (__id z))) 48) 0) "model/aarch_mem.sail 10457:41 - 10457:42") >>= fun _ =>
    let baseaddress : bits 52 :=
        autocast (concat_vec
                    (concat_vec (slice baseregister 2 4)
                                (slice baseregister z (Z.add (Z.opp z) 48))) (zeros z)) in
    returnm baseaddress
  else
    liftR ((ZeroExtend_slice_append 52 baseregister baselowerbound
                                    (Z.add (Z.opp baselowerbound) 48) (zeros baselowerbound)))
  : MR (mword 52) TLBRecord.

Definition calc_firstblocklevel_grainsize largegrain midgrain :=
  (if sumbool_of_bool (largegrain) then
     let grainsize := 16 in
     let firstblocklevel : Z := if ((Have52BitPAExt tt)) then 1 else 2 in
     (firstblocklevel, build_ex grainsize)
   else
     let '(firstblocklevel, existT _ grainsize _) :=
         (if sumbool_of_bool (midgrain) then
            let grainsize := 14 in
            let firstblocklevel : Z := 2 in
            (firstblocklevel, build_ex grainsize)
          else
            let grainsize := 12 in
            let firstblocklevel : Z := 1 in
            (firstblocklevel, build_ex grainsize))
         : (Z * {n : Z & ArithFact (n >=? 0)}) in
     (firstblocklevel, build_ex grainsize))
  : (Z * {n : Z & ArithFact (n >=? 0)}).

Definition calc_contiguousbitcheck inputsize largegrain midgrain level :=
  if sumbool_of_bool (largegrain) then andb (Z.eqb level 2) (Z.ltb inputsize 34)
  else if sumbool_of_bool (midgrain) then andb (Z.eqb level 2) (Z.ltb inputsize 30)
  else andb (Z.eqb level 1) (Z.ltb inputsize 34).

author: rems-project


Require Import ZArith.
Local Open Scope Z_scope.
Require Import Integers.
Require Import floyd.sublist.
Require Import compcert.common.Values.
Require Export List. Export ListNotations.
Require Export aes.list_utils.

Definition partially_filled(i n: Z)(f: Z -> int): list val :=
  (map Vint (fill_list i f)) ++ (repeat_op_table (n-i) Vundef id).

Lemma update_partially_filled: forall (i: Z) (f: Z -> int) (l: Z),
  0 <= i < l ->
  upd_Znth i (partially_filled i l f) (Vint (f i))
  = partially_filled (i+1) l f.
Admitted.

Lemma Znth_partially_filled: forall (i j n: Z) (f: Z -> int),
  0 <= i -> i < j -> j <= n ->
  Znth i (partially_filled j n f) Vundef = Vint (f i).
Admitted.