text:
(* Class Hierarchy, including definition of Countable Dense Linear Order Without Endpoints *)

Require Import SetoidClass List Omega.
Import ListNotations.

Definition nat_dec_eq : forall x y : nat, {x = y} + {x <> y}.
Proof.
  decide equality.
Defined.

Instance SetoidProd{X Y}`{Setoid X,Setoid Y} : Setoid (X * Y) :=
  {|
    equiv := fun '(x1,y1) '(x2,y2) => x1 == x2 /\ y1 == y2
  |}.
Proof.
  split.
  intros [x y]; split; reflexivity.
  intros [x y] [x' y'] [H1 H2]; split; symmetry; auto.
  intros [x y] [x' y'] [x'' y''] [H1 H2] [H3 H4]; split.
  rewrite H1; auto.
  rewrite H2; auto.
Defined.

Class Eq X `{Setoid X} := {
  dec_eq : forall x x', {x == x'} + {~ x == x'}
  }.

Instance EqProd{X Y}`{Eq X, Eq Y} : Eq (X * Y).
Proof.
  constructor; intros [x1 y1] [x2 y2].
  destruct (dec_eq x1 x2).
  destruct (dec_eq y1 y2).
  left; split; auto.
  right; intros [_ G]; contradiction.
  right; intros [G _]; contradiction.
Defined.

Fixpoint setoidIn{X}`{Eq X} (x : X) xs : Prop :=
  match xs with
  | [] => False
  | y::ys => x == y \/ setoidIn x ys
  end.

Lemma dec_setoidIn{X}`{Setoid X}`{Eq X} : forall (x : X) xs, {setoidIn x xs} + {~setoidIn x xs}.
Proof.
  induction xs.
  right; simpl; tauto.
  destruct (dec_eq x a).
  left; simpl; tauto.
  destruct IHxs.
  left; simpl; tauto.
  right; simpl; tauto.
Defined.

Lemma setoidIn_equiv{X}`{Setoid X}`{Eq X} : forall (x x' : X) xs,
  x == x' -> setoidIn x xs -> setoidIn x' xs.
Proof.
  induction xs; intros.
  destruct H3.
  destruct H3.
  left.
  rewrite <- H2; auto.
  right.
  apply IHxs; auto.
Qed.

Class Ord X `{Setoid X} := {
  lt : X -> X -> Prop;
  lt_morph : forall x x' y y', x == x' -> y == y' ->
    lt x y -> lt x' y';
  lt_irref : forall x, ~ lt x x;
  lt_trans : forall x y z, lt x y -> lt y z -> lt x z;
  lt_trich : forall x y, {lt x y} + {x == y} + {lt y x}
  }.

Arguments lt {_} {_} {_} _ _.
Infix "<<" := lt (at level 20).

Lemma lt_asymm {X}`{Ord X} : forall x y, x << y -> ~ y << x.
Proof.
  intros x y Hxy Hyx.
  elim (lt_irref x).
  apply (lt_trans _ y _); auto.
Qed.

Class Iso {X} {Y} `{Setoid X,Setoid Y} (oX : Ord X)(oY : Ord Y) := {
  forward : X -> Y;
  forward_morph : forall x x', x == x' -> forward x == forward x';
  back : Y -> X;
  back_morph : forall y y', y == y' -> back y == back y';
  fb_eq : forall y, forward (back y) == y;
  bf_eq : forall x, back (forward x) == x;
  forward_ord_morph : forall x x', x << x' -> forward x << forward x';
  back_ord_morph : forall y y', y << y' -> back y << back y'
  }.

Class CDLOWOEP {X} `{Setoid X} (O:Ord X) := {

  (*countable*)
  to_nat : X -> nat;
  from_nat : nat -> X;
  to_nat_morph : forall x x', x == x' -> to_nat x = to_nat x';
  to_from : forall n, to_nat (from_nat n) = n;
  from_to : forall x, from_nat (to_nat x) == x;

  (*dense*)
  mid : X -> X -> X;
  mid_morph : forall x x' y y', x == x' -> y == y' -> mid x y == mid x' y';
  mid_comm  : forall x x', mid x x' == mid x' x;
  mid_lt_left : forall x x', x << x' -> x << mid x x';
  mid_lt_right : forall x x', x << x' -> mid x x' << x';
  mid_idem : forall x, mid x x == x;

  (*without endpoints*)
  left : X -> X;
  left_morph : forall x x', x == x' -> left x == left x';
  left_lt: forall x, left x << x;
  right : X -> X;
  right_morph : forall x x', x == x' -> right x == right x';
  right_lt : forall x, x << right x

  }.

Lemma mid_lt_left2{X}`{CDLOWOEP X} : forall x x', x << x' -> x << mid x' x.
Proof.
  intros.
  apply (lt_morph x x (mid x x') (mid x' x)).
  - reflexivity.
  - apply mid_comm.
  - apply mid_lt_left; auto.
Qed.

Lemma mid_lt_right2{X}`{CDLOWOEP X} : forall x x', x << x' -> mid x' x << x'.
Proof.
  intros.
  apply (lt_morph (mid x x') (mid x' x) x' x').
  - apply mid_comm.
  - reflexivity.
  - apply mid_lt_right; auto.
Qed.

Instance CDLOWOEP_Eq{X}`{sX : Setoid X}(oX : Ord X)`{@CDLOWOEP X sX oX} : Eq X.
Proof.
  constructor; intros.
  destruct (lt_trich x x') as [[Hlt|Heq]|Hgt].
  - right; intro.
    elim (lt_irref x).
    eapply lt_morph.
    + reflexivity.
    + symmetry; exact H0.
    + exact Hlt.
  - left; exact Heq.
  - right; intro.
    elim (lt_irref x).
    eapply lt_morph.
    + symmetry; exact H0.
    + reflexivity.
    + exact Hgt.
Defined.

author: emarzion

repo: cantor

save_path: github-repos/coq/emarzion-cantor


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 GNU Lesser General Public License as        *)
(*  published by the Free Software Foundation, either version 2.1 of   *)
(*  the License, or  (at your option) any later version.               *)
(*  This file is also distributed under the terms of the               *)
(*  INRIA Non-Commercial License Agreement.                            *)
(*                                                                     *)
(* *********************************************************************)

(** This file defines a number of data types and operations used in
  the abstract syntax trees of many of the intermediate languages. *)

Require Import String.
Require Import Coqlib Maps Errors Integers Floats.
Require Archi.

Set Implicit Arguments.

(** * Syntactic elements *)

(** Identifiers (names of local variables, of global symbols and functions,
  etc) are represented by the type [positive] of positive integers. *)

Definition ident := positive.

Definition ident_eq := peq.

(** The intermediate languages are weakly typed, using the following types: *)

Inductive typ : Type :=
  | Tint                (**r 32-bit integers or pointers *)
  | Tfloat              (**r 64-bit double-precision floats *)
  | Tlong               (**r 64-bit integers *)
  | Tsingle             (**r 32-bit single-precision floats *)
  | Tany32              (**r any 32-bit value *)
  | Tany64.             (**r any 64-bit value, i.e. any value *)

Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}.
Proof. decide equality. Defined.
Global Opaque typ_eq.

Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2}
                     := list_eq_dec typ_eq.

Definition Tptr : typ := if Archi.ptr64 then Tlong else Tint.

Definition typesize (ty: typ) : Z :=
  match ty with
  | Tint => 4
  | Tfloat => 8
  | Tlong => 8
  | Tsingle => 4
  | Tany32 => 4
  | Tany64 => 8
  end.

Lemma typesize_pos: forall ty, typesize ty > 0.
Proof. destruct ty; simpl; lia. Qed.

Lemma typesize_Tptr: typesize Tptr = if Archi.ptr64 then 8 else 4.
Proof. unfold Tptr; destruct Archi.ptr64; auto. Qed.

(** All values of size 32 bits are also of type [Tany32].  All values
  are of type [Tany64].  This corresponds to the following subtyping
  relation over types. *)

Definition subtype (ty1 ty2: typ) : bool :=
  match ty1, ty2 with
  | Tint, Tint => true
  | Tlong, Tlong => true
  | Tfloat, Tfloat => true
  | Tsingle, Tsingle => true
  | (Tint | Tsingle | Tany32), Tany32 => true
  | _, Tany64 => true
  | _, _ => false
  end.

Fixpoint subtype_list (tyl1 tyl2: list typ) : bool :=
  match tyl1, tyl2 with
  | nil, nil => true
  | ty1::tys1, ty2::tys2 => subtype ty1 ty2 && subtype_list tys1 tys2
  | _, _ => false
  end.

(** To describe the values returned by functions, we use the more precise
    types below. *)

Inductive rettype : Type :=
  | Tret (t: typ)                       (**r like type [t] *)
  | Tint8signed                         (**r 8-bit signed integer *)
  | Tint8unsigned                       (**r 8-bit unsigned integer *)
  | Tint16signed                        (**r 16-bit signed integer *)
  | Tint16unsigned                      (**r 16-bit unsigned integer *)
  | Tvoid.                              (**r no value returned *)

Coercion Tret: typ >-> rettype.

Lemma rettype_eq: forall (t1 t2: rettype), {t1=t2} + {t1<>t2}.
Proof. generalize typ_eq; decide equality. Defined.
Global Opaque rettype_eq.

Definition proj_rettype (r: rettype) : typ :=
  match r with
  | Tret t => t
  | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => Tint
  | Tvoid => Tint
  end.

(** Additionally, function definitions and function calls are annotated
  by function signatures indicating:
- the number and types of arguments;
- the type of the returned value;
- additional information on which calling convention to use.

These signatures are used in particular to determine appropriate
calling conventions for the function. *)

Record calling_convention : Type := mkcallconv {
  cc_vararg: option Z;  (**r variable-arity function (+ number of fixed args) *)
  cc_unproto: bool;     (**r old-style unprototyped function *)
  cc_structret: bool    (**r function returning a struct  *)
}.

Definition cc_default :=
  {| cc_vararg := None; cc_unproto := false; cc_structret := false |}.

Definition calling_convention_eq (x y: calling_convention) : {x=y} + {x<>y}.
Proof.
  decide equality; try (apply bool_dec). decide equality; apply Z.eq_dec.
Defined.
Global Opaque calling_convention_eq.

Record signature : Type := mksignature {
  sig_args: list typ;
  sig_res: rettype;
  sig_cc: calling_convention
}.

Definition proj_sig_res (s: signature) : typ := proj_rettype s.(sig_res).

Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}.
Proof.
  generalize rettype_eq, list_typ_eq, calling_convention_eq; decide equality.
Defined.
Global Opaque signature_eq.

Definition signature_main :=
  {| sig_args := nil; sig_res := Tint; sig_cc := cc_default |}.

(** Memory accesses (load and store instructions) are annotated by
  a ``memory chunk'' indicating the type, size and signedness of the
  chunk of memory being accessed. *)

Inductive memory_chunk : Type :=
  | Mint8signed     (**r 8-bit signed integer *)
  | Mint8unsigned   (**r 8-bit unsigned integer *)
  | Mint16signed    (**r 16-bit signed integer *)
  | Mint16unsigned  (**r 16-bit unsigned integer *)
  | Mint32          (**r 32-bit integer, or pointer *)
  | Mint64          (**r 64-bit integer *)
  | Mfloat32        (**r 32-bit single-precision float *)
  | Mfloat64        (**r 64-bit double-precision float *)
  | Many32          (**r any value that fits in 32 bits *)
  | Many64.         (**r any value *)

Definition chunk_eq: forall (c1 c2: memory_chunk), {c1=c2} + {c1<>c2}.
Proof. decide equality. Defined.
Global Opaque chunk_eq.

Definition Mptr : memory_chunk := if Archi.ptr64 then Mint64 else Mint32.

(** The type (integer/pointer or float) of a chunk. *)

Definition type_of_chunk (c: memory_chunk) : typ :=
  match c with
  | Mint8signed => Tint
  | Mint8unsigned => Tint
  | Mint16signed => Tint
  | Mint16unsigned => Tint
  | Mint32 => Tint
  | Mint64 => Tlong
  | Mfloat32 => Tsingle
  | Mfloat64 => Tfloat
  | Many32 => Tany32
  | Many64 => Tany64
  end.

Lemma type_of_Mptr: type_of_chunk Mptr = Tptr.
Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed.

(** Same, as a return type. *)

Definition rettype_of_chunk (c: memory_chunk) : rettype :=
  match c with
  | Mint8signed => Tint8signed
  | Mint8unsigned => Tint8unsigned
  | Mint16signed => Tint16signed
  | Mint16unsigned => Tint16unsigned
  | Mint32 => Tint
  | Mint64 => Tlong
  | Mfloat32 => Tsingle
  | Mfloat64 => Tfloat
  | Many32 => Tany32
  | Many64 => Tany64
  end.

Lemma proj_rettype_of_chunk:
  forall chunk, proj_rettype (rettype_of_chunk chunk) = type_of_chunk chunk.
Proof.
  destruct chunk; auto.
Qed.

(** The chunk that is appropriate to store and reload a value of
  the given type, without losing information. *)

Definition chunk_of_type (ty: typ) :=
  match ty with
  | Tint => Mint32
  | Tfloat => Mfloat64
  | Tlong => Mint64
  | Tsingle => Mfloat32
  | Tany32 => Many32
  | Tany64 => Many64
  end.

Lemma chunk_of_Tptr: chunk_of_type Tptr = Mptr.
Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed.

(** Initialization data for global variables. *)

Inductive init_data: Type :=
  | Init_int8: int -> init_data
  | Init_int16: int -> init_data
  | Init_int32: int -> init_data
  | Init_int64: int64 -> init_data
  | Init_float32: float32 -> init_data
  | Init_float64: float -> init_data
  | Init_space: Z -> init_data
  | Init_addrof: ident -> ptrofs -> init_data.  (**r address of symbol + offset *)

Definition init_data_size (i: init_data) : Z :=
  match i with
  | Init_int8 _ => 1
  | Init_int16 _ => 2
  | Init_int32 _ => 4
  | Init_int64 _ => 8
  | Init_float32 _ => 4
  | Init_float64 _ => 8
  | Init_addrof _ _ => if Archi.ptr64 then 8 else 4
  | Init_space n => Z.max n 0
  end.

Fixpoint init_data_list_size (il: list init_data) {struct il} : Z :=
  match il with
  | nil => 0
  | i :: il' => init_data_size i + init_data_list_size il'
  end.

Lemma init_data_size_pos:
  forall i, init_data_size i >= 0.
Proof.
  destruct i; simpl; try extlia. destruct Archi.ptr64; lia.
Qed.

Lemma init_data_list_size_pos:
  forall il, init_data_list_size il >= 0.
Proof.
  induction il; simpl. lia. generalize (init_data_size_pos a); lia.
Qed.

(** Information attached to global variables. *)

Record globvar (V: Type) : Type := mkglobvar {
  gvar_info: V;                    (**r language-dependent info, e.g. a type *)
  gvar_init: list init_data;       (**r initialization data *)
  gvar_readonly: bool;             (**r read-only variable? (const) *)
  gvar_volatile: bool              (**r volatile variable? *)
}.

(** Whole programs consist of:
- a collection of global definitions (name and description);
- a set of public names (the names that are visible outside
  this compilation unit);
- the name of the ``main'' function that serves as entry point in the program.

A global definition is either a global function or a global variable.
The type of function descriptions and that of additional information
for variables vary among the various intermediate languages and are
taken as parameters to the [program] type.  The other parts of whole
programs are common to all languages. *)

Inductive globdef (F V: Type) : Type :=
  | Gfun (f: F)
  | Gvar (v: globvar V).

Arguments Gfun [F V].
Arguments Gvar [F V].

Record program (F V: Type) : Type := mkprogram {
  prog_defs: list (ident * globdef F V);
  prog_public: list ident;
  prog_main: ident
}.

Definition prog_defs_names (F V: Type) (p: program F V) : list ident :=
  List.map fst p.(prog_defs).

(** The "definition map" of a program maps names of globals to their definitions.
  If several definitions have the same name, the one appearing last in [p.(prog_defs)] wins. *)

Definition prog_defmap (F V: Type) (p: program F V) : PTree.t (globdef F V) :=
  PTree_Properties.of_list p.(prog_defs).

Section DEFMAP.

Variables F V: Type.
Variable p: program F V.

Lemma in_prog_defmap:
  forall id g, (prog_defmap p)!id = Some g -> In (id, g) (prog_defs p).
Proof.
  apply PTree_Properties.in_of_list.
Qed.

Lemma prog_defmap_dom:
  forall id, In id (prog_defs_names p) -> exists g, (prog_defmap p)!id = Some g.
Proof.
  apply PTree_Properties.of_list_dom.
Qed.

Lemma prog_defmap_unique:
  forall defs1 id g defs2,
  prog_defs p = defs1 ++ (id, g) :: defs2 ->
  ~In id (map fst defs2) ->
  (prog_defmap p)!id = Some g.
Proof.
  unfold prog_defmap; intros. rewrite H. apply PTree_Properties.of_list_unique; auto.
Qed.

Lemma prog_defmap_norepet:
  forall id g,
  list_norepet (prog_defs_names p) ->
  In (id, g) (prog_defs p) ->
  (prog_defmap p)!id = Some g.
Proof.
  apply PTree_Properties.of_list_norepet.
Qed.

End DEFMAP.

(** * Generic transformations over programs *)

(** We now define a general iterator over programs that applies a given
  code transformation function to all function descriptions and leaves
  the other parts of the program unchanged. *)

Section TRANSF_PROGRAM.

Variable A B V: Type.
Variable transf: A -> B.

Definition transform_program_globdef (idg: ident * globdef A V) : ident * globdef B V :=
  match idg with
  | (id, Gfun f) => (id, Gfun (transf f))
  | (id, Gvar v) => (id, Gvar v)
  end.

Definition transform_program (p: program A V) : program B V :=
  mkprogram
    (List.map transform_program_globdef p.(prog_defs))
    p.(prog_public)
    p.(prog_main).

End TRANSF_PROGRAM.

(** The following is a more general presentation of [transform_program]:
- Global variable information can be transformed, in addition to function
  definitions.
- The transformation functions can fail and return an error message.
- The transformation for function definitions receives a global context
  (derived from the compilation unit being transformed) as additiona
  argument.
- The transformation functions receive the name of the global as
  additional argument. *)

Local Open Scope error_monad_scope.

Section TRANSF_PROGRAM_GEN.

Variables A B V W: Type.
Variable transf_fun: ident -> A -> res B.
Variable transf_var: ident -> V -> res W.

Definition transf_globvar (i: ident) (g: globvar V) : res (globvar W) :=
  do info' <- transf_var i g.(gvar_info);
  OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)).

Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) :=
  match l with
  | nil => OK nil
  | (id, Gfun f) :: l' =>
    match transf_fun id f with
      | Error msg => Error (MSG "In function " :: CTX id :: MSG ": " :: msg)
      | OK tf =>
        do tl' <- transf_globdefs l'; OK ((id, Gfun tf) :: tl')
    end
  | (id, Gvar v) :: l' =>
    match transf_globvar id v with
      | Error msg => Error (MSG "In variable " :: CTX id :: MSG ": " :: msg)
      | OK tv =>
        do tl' <- transf_globdefs l'; OK ((id, Gvar tv) :: tl')
    end
  end.

Definition transform_partial_program2 (p: program A V) : res (program B W) :=
  do gl' <- transf_globdefs p.(prog_defs);
  OK (mkprogram gl' p.(prog_public) p.(prog_main)).

End TRANSF_PROGRAM_GEN.

(** The following is a special case of [transform_partial_program2],
  where only function definitions are transformed, but not variable definitions. *)

Section TRANSF_PARTIAL_PROGRAM.

Variable A B V: Type.
Variable transf_fun: A -> res B.

Definition transform_partial_program (p: program A V) : res (program B V) :=
  transform_partial_program2 (fun i f => transf_fun f) (fun i v => OK v) p.

End TRANSF_PARTIAL_PROGRAM.

Lemma transform_program_partial_program:
  forall (A B V: Type) (transf_fun: A -> B) (p: program A V),
  transform_partial_program (fun f => OK (transf_fun f)) p = OK (transform_program transf_fun p).
Proof.
  intros. unfold transform_partial_program, transform_partial_program2.
  assert (EQ: forall l,
              transf_globdefs (fun i f => OK (transf_fun f)) (fun i (v: V) => OK v) l =
              OK (List.map (transform_program_globdef transf_fun) l)).
  { induction l as [ | [id g] l]; simpl.
  - auto.
  - destruct g; simpl; rewrite IHl; simpl. auto. destruct v; auto.
  }
  rewrite EQ; simpl. auto.
Qed.

(** * External functions *)

(** For most languages, the functions composing the program are either
  internal functions, defined within the language, or external functions,
  defined outside.  External functions include system calls but also
  compiler built-in functions.  We define a type for external functions
  and associated operations. *)

Inductive external_function : Type :=
  | EF_external (name: string) (sg: signature)
     (** A system call or library function.  Produces an event
         in the trace. *)
  | EF_builtin (name: string) (sg: signature)
     (** A compiler built-in function.  Behaves like an external, but
         can be inlined by the compiler. *)
  | EF_runtime (name: string) (sg: signature)
     (** A function from the run-time library.  Behaves like an
         external, but must not be redefined. *)
  | EF_vload (chunk: memory_chunk)
     (** A volatile read operation.  If the address given as first argument
         points within a volatile global variable, generate an
         event and return the value found in this event.  Otherwise,
         produce no event and behave like a regular memory load. *)
  | EF_vstore (chunk: memory_chunk)
     (** A volatile store operation.   If the address given as first argument
         points within a volatile global variable, generate an event.
         Otherwise, produce no event and behave like a regular memory store. *)
  | EF_malloc
     (** Dynamic memory allocation.  Takes the requested size in bytes
         as argument; returns a pointer to a fresh block of the given size.
         Produces no observable event. *)
  | EF_free
     (** Dynamic memory deallocation.  Takes a pointer to a block
         allocated by an [EF_malloc] external call and frees the
         corresponding block.
         Produces no observable event. *)
  | EF_memcpy (sz: Z) (al: Z)
     (** Block copy, of [sz] bytes, between addresses that are [al]-aligned. *)
  | EF_annot (kind: positive) (text: string) (targs: list typ)
     (** A programmer-supplied annotation.  Takes zero, one or several arguments,
         produces an event carrying the text and the values of these arguments,
         and returns no value. *)
  | EF_annot_val (kind: positive) (text: string) (targ: typ)
     (** Another form of annotation that takes one argument, produces
         an event carrying the text and the value of this argument,
         and returns the value of the argument. *)
  | EF_inline_asm (text: string) (sg: signature) (clobbers: list string)
     (** Inline [asm] statements.  Semantically, treated like an
         annotation with no parameters ([EF_annot text nil]).  To be
         used with caution, as it can invalidate the semantic
         preservation theorem.  Generated only if [-finline-asm] is
         given. *)
  | EF_debug (kind: positive) (text: ident) (targs: list typ).
     (** Transport debugging information from the front-end to the generated
         assembly.  Takes zero, one or several arguments like [EF_annot].
         Unlike [EF_annot], produces no observable event. *)

(** The type signature of an external function. *)

Definition ef_sig (ef: external_function): signature :=
  match ef with
  | EF_external name sg => sg
  | EF_builtin name sg => sg
  | EF_runtime name sg => sg
  | EF_vload chunk => mksignature (Tptr :: nil) (rettype_of_chunk chunk) cc_default
  | EF_vstore chunk => mksignature (Tptr :: type_of_chunk chunk :: nil) Tvoid cc_default
  | EF_malloc => mksignature (Tptr :: nil) Tptr cc_default
  | EF_free => mksignature (Tptr :: nil) Tvoid cc_default
  | EF_memcpy sz al => mksignature (Tptr :: Tptr :: nil) Tvoid cc_default
  | EF_annot kind text targs => mksignature targs Tvoid cc_default
  | EF_annot_val kind text targ => mksignature (targ :: nil) targ cc_default
  | EF_inline_asm text sg clob => sg
  | EF_debug kind text targs => mksignature targs Tvoid cc_default
  end.

(** Whether an external function should be inlined by the compiler. *)

Definition ef_inline (ef: external_function) : bool :=
  match ef with
  | EF_external name sg => false
  | EF_builtin name sg => true
  | EF_runtime name sg => false
  | EF_vload chunk => true
  | EF_vstore chunk => true
  | EF_malloc => false
  | EF_free => false
  | EF_memcpy sz al => true
  | EF_annot kind text targs => true
  | EF_annot_val kind Text rg => true
  | EF_inline_asm text sg clob => true
  | EF_debug kind text targs => true
  end.

(** Whether an external function must reload its arguments. *)

Definition ef_reloads (ef: external_function) : bool :=
  match ef with
  | EF_annot kind text targs => false
  | EF_debug kind text targs => false
  | _ => true
  end.

(** Equality between external functions.  Used in module [Allocation]. *)

Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}.
Proof.
  generalize ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros.
  decide equality.
Defined.
Global Opaque external_function_eq.

(** Function definitions are the union of internal and external functions. *)

Inductive fundef (F: Type): Type :=
  | Internal: F -> fundef F
  | External: external_function -> fundef F.

Arguments External [F].

Section TRANSF_FUNDEF.

Variable A B: Type.
Variable transf: A -> B.

Definition transf_fundef (fd: fundef A): fundef B :=
  match fd with
  | Internal f => Internal (transf f)
  | External ef => External ef
  end.

End TRANSF_FUNDEF.

Section TRANSF_PARTIAL_FUNDEF.

Variable A B: Type.
Variable transf_partial: A -> res B.

Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
  match fd with
  | Internal f => do f' <- transf_partial f; OK (Internal f')
  | External ef => OK (External ef)
  end.

End TRANSF_PARTIAL_FUNDEF.

(** * Register pairs *)

Set Contextual Implicit.

(** In some intermediate languages (LTL, Mach), 64-bit integers can be
  split into two 32-bit halves and held in a pair of registers.
  Syntactically, this is captured by the type [rpair] below. *)

Inductive rpair (A: Type) : Type :=
  | One (r: A)
  | Twolong (rhi rlo: A).

Definition typ_rpair (A: Type) (typ_of: A -> typ) (p: rpair A): typ :=
  match p with
  | One r => typ_of r
  | Twolong rhi rlo => Tlong
  end.

Definition map_rpair (A B: Type) (f: A -> B) (p: rpair A): rpair B :=
  match p with
  | One r => One (f r)
  | Twolong rhi rlo => Twolong (f rhi) (f rlo)
  end.

Definition regs_of_rpair (A: Type) (p: rpair A): list A :=
  match p with
  | One r => r :: nil
  | Twolong rhi rlo => rhi :: rlo :: nil
  end.

Fixpoint regs_of_rpairs (A: Type) (l: list (rpair A)): list A :=
  match l with
  | nil => nil
  | p :: l => regs_of_rpair p ++ regs_of_rpairs l
  end.

Lemma in_regs_of_rpairs:
  forall (A: Type) (x: A) p, In x (regs_of_rpair p) -> forall l, In p l -> In x (regs_of_rpairs l).
Proof.
  induction l; simpl; intros. auto. apply in_app. destruct H0; auto. subst a. auto.
Qed.

Lemma in_regs_of_rpairs_inv:
  forall (A: Type) (x: A) l, In x (regs_of_rpairs l) -> exists p, In p l /\ In x (regs_of_rpair p).
Proof.
  induction l; simpl; intros. contradiction.
  rewrite in_app_iff in H; destruct H.
  exists a; auto.
  apply IHl in H. firstorder auto.
Qed.

Definition forall_rpair (A: Type) (P: A -> Prop) (p: rpair A): Prop :=
  match p with
  | One r => P r
  | Twolong rhi rlo => P rhi /\ P rlo
  end.

(** * Arguments and results to builtin functions *)

Inductive builtin_arg (A: Type) : Type :=
  | BA (x: A)
  | BA_int (n: int)
  | BA_long (n: int64)
  | BA_float (f: float)
  | BA_single (f: float32)
  | BA_loadstack (chunk: memory_chunk) (ofs: ptrofs)
  | BA_addrstack (ofs: ptrofs)
  | BA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: ptrofs)
  | BA_addrglobal (id: ident) (ofs: ptrofs)
  | BA_splitlong (hi lo: builtin_arg A)
  | BA_addptr (a1 a2: builtin_arg A).

Inductive builtin_res (A: Type) : Type :=
  | BR (x: A)
  | BR_none
  | BR_splitlong (hi lo: builtin_res A).

Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident :=
  match a with
  | BA_loadglobal chunk id ofs => id :: nil
  | BA_addrglobal id ofs => id :: nil
  | BA_splitlong hi lo => globals_of_builtin_arg hi ++ globals_of_builtin_arg lo
  | BA_addptr a1 a2 => globals_of_builtin_arg a1 ++ globals_of_builtin_arg a2
  | _ => nil
  end.

Definition globals_of_builtin_args (A: Type) (al: list (builtin_arg A)) : list ident :=
  List.fold_right (fun a l => globals_of_builtin_arg a ++ l) nil al.

Fixpoint params_of_builtin_arg (A: Type) (a: builtin_arg A) : list A :=
  match a with
  | BA x => x :: nil
  | BA_splitlong hi lo => params_of_builtin_arg hi ++ params_of_builtin_arg lo
  | BA_addptr a1 a2 => params_of_builtin_arg a1 ++ params_of_builtin_arg a2
  | _ => nil
  end.

Definition params_of_builtin_args (A: Type) (al: list (builtin_arg A)) : list A :=
  List.fold_right (fun a l => params_of_builtin_arg a ++ l) nil al.

Fixpoint params_of_builtin_res (A: Type) (a: builtin_res A) : list A :=
  match a with
  | BR x => x :: nil
  | BR_none => nil
  | BR_splitlong hi lo => params_of_builtin_res hi ++ params_of_builtin_res lo
  end.

Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_arg B :=
  match a with
  | BA x => BA (f x)
  | BA_int n => BA_int n
  | BA_long n => BA_long n
  | BA_float n => BA_float n
  | BA_single n => BA_single n
  | BA_loadstack chunk ofs => BA_loadstack chunk ofs
  | BA_addrstack ofs => BA_addrstack ofs
  | BA_loadglobal chunk id ofs => BA_loadglobal chunk id ofs
  | BA_addrglobal id ofs => BA_addrglobal id ofs
  | BA_splitlong hi lo =>
      BA_splitlong (map_builtin_arg f hi) (map_builtin_arg f lo)
  | BA_addptr a1 a2 =>
      BA_addptr (map_builtin_arg f a1) (map_builtin_arg f a2)
  end.

Fixpoint map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_res B :=
  match a with
  | BR x => BR (f x)
  | BR_none => BR_none
  | BR_splitlong hi lo =>
      BR_splitlong (map_builtin_res f hi) (map_builtin_res f lo)
  end.

(** Which kinds of builtin arguments are supported by which external function. *)

Inductive builtin_arg_constraint : Type :=
  | OK_default
  | OK_const
  | OK_addrstack
  | OK_addressing
  | OK_all.

author: AbsInt

repo: CompCert

save_path: github-repos/coq/AbsInt-CompCert


text:
(** * Kripke Semantics *)

Set Implicit Arguments.

(* Require Import decidable_IN. *)
Require Import associations.
Require Import sublist.
Require Import language_syntax.
Require Import substitution_wellformedness.
Require Import variable_sets.
Require Import fresh_name.
Require Import LJT_and_weakening.
Require Import renaming.

(** ** Kripke Model *)

(** We use the conventional Kripke model adopted by Troelstra and van Dalen
   for the semantics of LJT.

   - A Kripke model is a tuple of a partially-ordered set of _worlds_, a domain,
     interpretations of constants and function symbols into the domain,
     and a binary relation between worlds and atomic sentences. *)

Record Kripke : Type := {
  worlds: Type;
  wle : worlds -> worlds -> Type;
  wle_refl : forall w, wle w w;
  wle_trans : forall w w' w'', wle w w' -> wle w' w'' -> wle w w'';
  domain : Type;
  csts : name -> domain;
  funs : function -> domain -> domain -> domain;
  atoms : worlds -> predicate * domain -> Type;
  atoms_mon : forall w w', wle w w' -> forall P, atoms w P -> atoms w' P
  }.

Notation "w <= w'" := (wle _ w w') (at level 70).

(** ** Semantics *)

(** Interpretation of a pseudo-term in a Kripke model using associations for variables.

   - The interpretation of pseudo-terms is made total by ignoring insignificant variables.

   - The being-in-a-list part of a term is simply ignored during the interpretation.

   - The trace relocation has no impact on the Kripke semantics. *)

Fixpoint psem K (t : trm) (rho: assoc (domain K)) (eta: assoc (domain K)){struct t} :
  domain K :=
  match t with
    | Ltr x  => match fun_assoc eta x with
                    | Some u => u
                    | None => csts _ 0 (* fixed value *)
                  end
    | Par y => match fun_assoc rho y with
                    | Some u => u
                    | None => csts _ 0 (* fixed value *)
                  end
    | Cst c => csts _ c
    | App f t1 t2 => funs _ f (psem K t1 rho eta) (psem K t2 rho eta)
  end.

(** Forcing: The Kripke semantics is extended to all formulae *)

Reserved Notation "w ||- A {[ rho , eta ]}" (at level 80).

Fixpoint force K (w: worlds K)  (A : fml) rho eta {struct A} : Type :=
  match A with
    | Atom (p,t) => atoms K w (p, psem K t rho eta)
    | B --> C    => forall w', w <= w' ->
                    w' ||- B {[ rho, eta ]} -> w' ||- C {[rho, eta]}
    | Forall y B => forall w', w <= w' ->
                    forall (d :domain K), w' ||- B {[rho, (y, d) :: eta]}
  end

  where " w ||- A {[ rho , eta ]} " := (force _ w A  rho eta).

Notation "w ||- A {[ rho , eta ]}" := (force _ w A rho eta) (at level 80).

(** Forcing is monotone w.r.t. the world relation. *)

Lemma mono_force : forall K (w w':worlds K) rho eta,
  w <= w' ->
  forall (A : fml),
    w ||- A {[rho, eta]} -> w' ||- A {[rho, eta]}.
Proof.
  induction A as [ [p t]| |]; simpl; intros;
  [ apply atoms_mon with (w:=w)
  | apply X0
  | apply X0]; eauto using wle_trans.
Qed.

(** ** Equivalence of associations *)

Definition assoc_equiv (A:Type) m (eta eta0:assoc A) :=
  forall x, IN_name x m -> eta ^^ x = eta0 ^^ x.

Hint Unfold assoc_equiv.

Lemma assoc_equiv_comm : forall (A:Type) m (eta eta0:assoc A),
  assoc_equiv m eta eta0 ->
  assoc_equiv m eta0 eta.
Proof.
  firstorder using assoc_equiv.
Qed.

Lemma assoc_equiv_cons : forall (A: Type) m (eta eta0 : assoc A),
  assoc_equiv m eta eta0 ->
  forall x d,
    assoc_equiv (x :: m) ((x, d) :: eta) ((x, d) :: eta0).
Proof.
  unfold assoc_equiv; intros; simpl; case_var; auto.
  eauto using neq_IN_cons.
Qed.

Hint Resolve assoc_equiv_comm assoc_equiv_cons.

(** A specified tactic for handling [assoc_equiv]. *)

Ltac solve_assoc :=
  let z := fresh "z" in
    let Hz := fresh "Hz" in
      intros z Hz; simpl in *; repeat case_var; intuition.

(** Semantics for well-defined terms/formulas is fixed. *)

Lemma psem_assoc_equiv : forall K m eta eta0 rho (t:trm),
  sub_name (ol_t t) m->
  assoc_equiv m eta eta0 ->
  psem K t rho eta = psem K t rho eta0.
Proof.
  induction t; intros H ?; simpl in H; simpl; auto.
  - rewrite H0; auto with datatypes.
  - f_equal; auto with datatypes.
Qed.

Lemma wf_t_ol_t_empty : forall t : trm,
  wf_t t -> ol_t t = nil.
Proof.
  induction t; simpl; intros; auto;
  [ inversion H
  | rewrite IHt1, IHt2; auto with datatypes; inversion_clear H; auto].
Qed.

Lemma psem_term_assoc_indep : forall K eta eta0 rho (t:trm),
  wf_t t ->
  psem K t rho eta = psem K t rho eta0.
Proof.
  intros; apply psem_assoc_equiv with (m:=nil);
  [ rewrite wf_t_ol_t_empty; auto with datatypes
  | unfold assoc_equiv; intros ? H0; inversion H0].
Qed.

Lemma force_assoc_equiv : forall (A:fml) m K (w:worlds K) rho eta eta0,
  sub_name (ol A) m ->
  assoc_equiv m eta eta0 ->
  w ||- A {[rho , eta]} ->
  w ||- A {[rho, eta0]}.
Proof.
  induction A as [ [p t]| | y A]; simpl; intros.
  -  rewrite psem_assoc_equiv with (eta0:=eta0)(m:=m) in X; auto.
  -  apply IHA2 with (m:=m) (eta:=eta) ; eauto with datatypes.
  -  apply mono_force with (w:=w); try assumption.
     apply IHA with (m:=(y::m))  (eta := (y,d)::eta); auto with datatypes.
     apply X; auto; apply wle_refl.
Qed.

Lemma force_fml_assoc_indep : forall K (w:worlds K) rho eta eta0 (A:fml),
  wf A ->
  w ||- A {[rho , eta]} ->
  w ||- A {[rho , eta0]}.
Proof.
  intros; apply force_assoc_equiv with (m:=nil : list name) (eta :=eta);
  try firstorder; rewrite wf_ol_empty; auto.
Qed.

(** Fresh parameters have no impact on semantics. *)

Lemma psem_fresh_par : forall  (t:trm) K a d rho eta,
  a # op_t t ->
  psem K t rho eta =  psem K t ((a,d)::rho) eta.
Proof.
  induction t; simpl; intros; auto;
    [ repeat case_var; intuition congruence
    | destruct_notin; f_equal; auto
    ].
Qed.

Lemma force_fresh_parL : forall (A: fml) K (w:worlds K) a d rho eta,
  w ||- A {[rho, eta]} ->
  a # op A ->
  w ||- A {[(a,d) :: rho, eta]}

  with force_fresh_parR : forall (A:fml) K (w:worlds K) a d rho eta,
    w ||- A {[(a,d) :: rho, eta]} ->
    a # op A ->
    w ||- A {[rho, eta]}.
Proof.
  - induction A as [ [p t]| | ]; simpl; intros;
    [ rewrite <- psem_fresh_par
    | destruct_notin
    | idtac
    ]; eauto.

  - induction A as [ [p t]| | ]; simpl; intros;
    [ rewrite <- psem_fresh_par in *; auto
      | destruct_notin; eauto
      | eauto
    ].
Qed.

Lemma psem_tsubst : forall (t:trm) x (u:trm) K rho eta,
  psem K t rho ((x, psem K u rho eta) :: eta) =
  psem K (t [[nil, (x,u):: nil]]) rho eta.
Proof.
  induction t; simpl; intros; auto.
  - case_var; auto.
  - f_equal; auto.
Qed.

Definition wo_list_assoc_equiv (A : Type) (zeta zeta0: assoc A):=
  forall z, zeta ^^ z = zeta0 ^^z.

Proposition lem0: forall (A : Type) (zeta zeta0 : assoc A),
  wo_list_assoc_equiv zeta zeta0 ->
  forall m, assoc_equiv m zeta zeta0.
Proof.
  intros; auto.
Qed.

Proposition lem1 : forall (B: fml) K0 (w0 : worlds K0) rho zeta zeta0,
  wo_list_assoc_equiv zeta zeta0 ->
  w0 ||- B {[rho, zeta]} -> w0 ||- B {[rho, zeta0]}.
Proof.
  intros;
  apply force_assoc_equiv with (eta:= zeta) (m:=ol B); auto.
Qed.

Theorem force_subst : forall (A : fml) x (u : trm) K (w:worlds K) rho eta,
  wf_t u ->
  w ||- A {[rho , (x, psem K u rho eta) :: eta]} ->
  w ||- (A [nil , (x,u)::nil]) {[rho, eta]}

with subst_force : forall (A: fml) x (u : trm) K (w:worlds K) rho eta,
  wf_t u ->
  w ||- (A [nil, (x,u)::nil]) {[rho, eta]} ->
  w ||- A {[rho, (x, psem K u rho eta) :: eta]}.
Proof.
  (* force_subst *)
  - induction A as [ [p t] | A1 A2 | y A ]; simpl; intros.
    + rewrite <- psem_tsubst; assumption.
    + apply force_subst; auto; apply X; auto;
      apply subst_force with (l:=l); auto.
    + case_var.
      * rewrite <- nil_subst;
        apply force_assoc_equiv with (m:=(ol A)) (eta:=((x, d) :: (x, psem K u rho eta) :: eta)); auto ; solve_assoc.

      * apply force_subst; auto.
        destruct (x==y); [ contradict n| idtac]; auto.

        rewrite psem_term_assoc_indep with (eta0 := eta); auto.

        apply lem1 with (zeta:= ((y, d) :: (x, psem K u rho eta) :: eta));
        [intro z; unfold wo_list_assoc_equiv; simpl;
         repeat case_var; intuition try congruence
        | apply X, X0].

  (* subst_force *)
  - induction A as  [ [p t] | A1 A2 | y A ]; simpl; intros.
    + rewrite <- psem_tsubst in X; assumption.
    + apply subst_force; auto.
    + case_var.
      * apply force_assoc_equiv with (m:= ol A)(eta := (x, d) :: eta); auto.
        solve_assoc.
        replace ( w' ||- A {[rho, (x, d) :: eta]} ) with (w' ||-  A [nil, nil] {[rho, (x, d) :: eta]}).
        apply X, X0. rewrite <- nil_subst; auto.

      * apply lem1 with (zeta := (x, psem K u rho eta) :: (y, d) :: eta).
        intro z; unfold wo_list_assoc_equiv;  auto ; simpl;
        repeat case_var; intuition try congruence.
        rewrite psem_term_assoc_indep with (eta0 := ((y, d):: eta)); auto.
Qed.

author: liganega

repo: bind

save_path: github-repos/coq/liganega-bind