Module Archi


Architecture-dependent parameters for PowerPC

From Flocq Require Import Binary Bits.
Require Import ZArith List.

Definition ptr64 := false.

Definition big_endian := true.

Definition align_int64 := 8%Z.
Definition align_float64 := 8%Z.

Can we use the 64-bit extensions to the PowerPC architecture?
Parameter ppc64 : bool.

Should single-precision FP arguments passed on stack be passed as singles or use double FP format.
Parameter single_passed_as_single : bool.

Definition splitlong := negb ppc64.

Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.
Proof.
  reflexivity.
Qed.

Definition default_nan_64 := (false, iter_nat 51 _ xO xH).
Definition default_nan_32 := (false, iter_nat 22 _ xO xH).


Definition choose_nan_64 (l: list (bool * positive)) : bool * positive :=
  match l with nil => default_nan_64 | n :: _ => n end.

Definition choose_nan_32 (l: list (bool * positive)) : bool * positive :=
  match l with nil => default_nan_32 | n :: _ => n end.

Lemma choose_nan_64_idem: forall n,
  choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil).
Proof.
auto. Qed.

Lemma choose_nan_32_idem: forall n,
  choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil).
Proof.
auto. Qed.

Definition fma_order {A: Type} (x y z: A) := (x, z, y).

Definition fma_invalid_mul_is_nan := false.

Definition float_of_single_preserves_sNaN := true.

Global Opaque ptr64 big_endian splitlong
              default_nan_64 choose_nan_64
              default_nan_32 choose_nan_32
              fma_order fma_invalid_mul_is_nan
              float_of_single_preserves_sNaN.