fix missing files

src/ABI/FarRetABI.v

@@ -79,12 +79,12 @@ End BinaryCoder.
 
 Section LayoutCoder.
 
-  Definition encode_layout: @encoder params_layout params :=
+ Definition encode_layout: @encoder params_layout params :=
 fun params =>
   match params with
   | mk_params (ForwardExistingFatPointer fptr) =>
       match FatPointerABI.encode_layout fptr with
-        | Some ptr_layout =>
+      | Some ptr_layout =>
             Some
               {|
                 raw_memory_forwarding_type_enum := FarCallForwardPageType.ForwardFatPointer;
@@ -115,9 +115,9 @@ fun params =>
           end
       end
   .
-
   Theorem layout_coding_revertible: revertible decode_layout encode_layout.
-    unfold revertible.
+Proof.
+  unfold revertible.
     unfold revertible, decode_layout, encode_layout, fwd_memory_adapter.
     move => [fwd_memory encoded].
     case_eq fwd_memory.
@@ -144,7 +144,8 @@ fun params =>
        repeat f_equal =>//=; by destruct s.
      }
     }
-  Qed.
+    Qed.
+
 
   Definition coder_layout := mk_coder decode_layout encode_layout layout_coding_revertible.
 

src/ABI/ForwardPageTypesABI.v

@@ -18,8 +18,8 @@ Definition data_page_type_to_u8 (t:data_page_type) : u8 :=
 
 Definition span_of (fp: fat_ptr_layout) : option span :=
   if fp.(offset) == zero32
-  then None
-  else Some (mk_span fp.(start) fp.(length))
+  then Some (mk_span fp.(start) fp.(length))
+  else None
 .
 
 Definition fwd_memory_adapter (fwd_type: u8) (raw_fat_ptr_layout: fat_ptr_layout) : option MemoryManagement.fwd_memory:=

src/lib/Arith_ext.v

@@ -0,0 +1,36 @@
+Require Lia ZArith.
+
+(** * Additional properties of natural numbers *)
+
+Section PowerTwo.
+  Import Coq.ZArith.Zpower.
+  Import Coq.ZArith.BinIntDef.
+  Import BinNums.
+
+
+  Open Scope Z_scope.
+
+  Theorem two_power_nat_0 :
+    two_power_nat 0 = 1%Z.
+  Proof.
+    reflexivity.
+  Qed.
+
+  Theorem two_power_nat_gt_0:
+    forall n : nat, BinInt.Z.gt (two_power_nat n) 0%Z.
+  Proof.
+    induction n.
+    - rewrite two_power_nat_0.
+      reflexivity.
+    - rewrite two_power_nat_S.
+      Lia.lia.
+  Qed.
+
+
+  (* Lemma two_power_nat_two_p: *)
+  (*   forall x, two_power_nat x = two_p (Z.of_nat x). *)
+  (* Proof. *)
+  (*   induction x. auto. *)
+  (*   rewrite two_power_nat_S. rewrite Nat2Z.inj_succ. rewrite two_p_S. Lia.lia. Lia.lia. *)
+  (* Qed. *)
+End PowerTwo.

src/lib/Decidability.v

@@ -0,0 +1,46 @@
+From Coq.Logic   Require Decidable.
+
+Import Decidable.
+
+Section Decidability.
+
+  Definition dec(A: Prop) := { A } + { ~ A }.
+
+  Lemma dec_decidable :
+    forall P, dec P -> decidable P.
+  Proof. unfold dec, decidable. intros ? []; tauto. Qed.
+
+
+  Theorem dec_conj:
+    forall A B: Prop,
+      dec A ->
+      dec B ->
+      dec (A /\ B).
+  Proof. unfold dec. intros; tauto. Qed.
+
+  Theorem dec_not : forall A:Prop, dec A -> dec (~ A).
+  Proof. unfold dec. tauto. Qed.
+
+  Theorem dec_not_not : forall P:Prop, dec P -> ~ ~ P -> P.
+  Proof. unfold dec; tauto. Qed.
+
+  Theorem not_not : forall P: Prop,
+      dec P -> ~ ~ P -> P.
+  Proof. unfold dec; tauto. Qed.
+
+  Theorem dec_or:
+    forall A B: Prop,
+      dec A ->
+      dec B ->
+      dec (A \/ B).
+  Proof. unfold dec; intros; tauto. Qed.
+
+  Definition eq_dec (T:Type) := forall x1 x2: T, dec (x1 = x2).
+
+End Decidability.
+
+Ltac decide_equality :=
+  unfold eq_dec, dec in *;
+  repeat decide equality;
+  unfold eq_dec, dec in *;
+  eauto with decidable_prop.

src/lib/PArith_ext.v

@@ -0,0 +1,52 @@
+Require BinNums BinInt ZArith Arith_ext.
+
+(** * Additional properties of positive numbers *)
+
+
+(** ** Power *)
+Section ModuloPowerOfTwo.
+Import Arith_ext BinNums BinInt ZArith Lia.
+
+Open Scope Z_scope.
+
+
+Fixpoint mod_pow2 (p: positive) (n: nat) {struct n} : Z :=
+  match n, p with
+  | O, _ => 0
+  | S m, xH => 1
+  | S m, xO tail => Z.double (mod_pow2 tail m)
+  | S m, xI tail => Z.succ_double (mod_pow2 tail m)
+  end.
+
+Theorem mod_pow2_ge_0:
+  forall p n, mod_pow2 p n >= 0.
+Proof.
+  induction p; destruct n; simpl; auto with zarith.
+  - rewrite Z.succ_double_spec.
+    apply Z.le_ge.
+    apply Z.add_nonneg_nonneg; auto with zarith.
+    replace 0 with ( 0 * mod_pow2 p n); [|auto with zarith].
+    eapply Zmult_le_compat_r; [auto with zarith|].
+    apply Z.ge_le.
+    apply IHp.
+  - rewrite Z.double_spec.
+    replace 0 with ( 0 * mod_pow2 p n); [|auto with zarith].
+    eapply Zmult_ge_compat_r; [auto with zarith|].
+    apply IHp.
+Qed.
+
+Lemma mod_pow2_limit:
+  forall p n, mod_pow2 p n < two_power_nat n.
+Proof.
+  intros p n; revert p.
+  induction n; simpl; intros.
+  - rewrite Arith_ext.two_power_nat_0. lia.
+  - rewrite two_power_nat_S. destruct p.
+    + pose (IHn p). rewrite Z.succ_double_spec. lia.
+    + pose (IHn p). rewrite Z.double_spec. lia.
+    + pose (two_power_nat_gt_0 n). lia.
+Qed.
+
+
+Close Scope Z_scope.
+End ModuloPowerOfTwo.

src/lib/PMap_ext.v

@@ -0,0 +1,15 @@
+Require FMapPositive.
+
+Import FMapPositive.PositiveMap BinPos.
+
+Definition pmap_slice {V} (m:t V) (from_incl to_excl:positive ) : t V :=
+  let leb x y := negb (Pos.ltb y x) in
+  let in_range k := andb (leb from_incl k) (Pos.ltb k to_excl) in
+  let f k cell accmap :=
+    if in_range k
+    then
+      add k cell accmap
+    else
+      accmap
+    in
+  fold f m (empty _).

src/lib/ZArith_ext.v

@@ -0,0 +1,128 @@
+Require Coq.Logic.Decidable.
+Require Decidability.
+Require PArith.
+Require PArith_ext.
+Require ZArith.
+Require Lia.
+
+(** * Properties of Z *)
+
+Section Decidability.
+  (** ** Decidability *)
+  Import Decidability ZArith.
+
+  Lemma eq_dec : eq_dec BinNums.Z.
+    decide_equality.
+  Defined.
+
+  Open Scope Z_scope.
+  Definition lt_dec: forall (x y: Z), {x < y} + {x >= y}.
+  Proof.
+    unfold Z.lt, Z.ge.
+    intros x y; destruct (Z.compare x y); auto; right; intro H; inversion H.
+  Defined.
+
+  Definition gt_dec: forall (x y: Z), {x > y} + {x <= y}.
+  Proof.
+    unfold Z.gt, Z.le.
+    intros x y; destruct (Z.compare x y); auto; right; intro H; inversion H.
+  Defined.
+
+End Decidability.
+
+
+Section ModuloPowerOfTwo.
+  Import ZArith.
+  Import PArith_ext.
+  Open Scope Z.
+
+  Definition mod_pow2 (z: Z) (n: nat) : Z :=
+    match z with
+    | Z0 => 0
+    | Zpos p => mod_pow2 p n
+    | Zneg p => let r := mod_pow2 p n in
+               if ZArith_ext.eq_dec r 0%Z
+               then 0
+               else ZArith.Zpower.two_power_nat n - r
+    end.
+
+
+  Theorem mod_pow2_ge_0:
+    forall z n, mod_pow2 z n >= 0.
+  Proof.
+    intros. unfold mod_pow2. pose ( Arith_ext.two_power_nat_gt_0 n) as Hpos.
+    destruct z.
+    - auto with zarith.
+    - exact (PArith_ext.mod_pow2_ge_0 p n).
+    - destruct (eq_dec _ 0) .
+      + auto with zarith.
+      + pose (PArith_ext.mod_pow2_ge_0 p n).
+        pose (PArith_ext.mod_pow2_limit p n).
+        Lia.lia.
+  Qed.
+
+  Theorem mod_pow2_limit:
+    forall z n, mod_pow2 z n < two_power_nat n.
+  Proof.
+    intros. unfold mod_pow2. pose ( Arith_ext.two_power_nat_gt_0 n) as Hpos.
+    destruct z.
+    - auto with zarith.
+    - pose (PArith_ext.mod_pow2_limit p n). auto with zarith.
+    - destruct (eq_dec _ 0) .
+      + auto with zarith.
+      + pose (PArith_ext.mod_pow2_ge_0 p n).
+        pose (PArith_ext.mod_pow2_limit p n).
+        Lia.lia.
+  Qed.
+
+  Theorem mod_pow2_range:
+    forall z n, 0 <= mod_pow2 z n < two_power_nat n.
+  Proof.
+    split.
+    - apply Z.ge_le. apply mod_pow2_ge_0.
+    - apply mod_pow2_limit.
+  Qed.
+
+  (* Lemma mod_modulus_range: *)
+  (*   forall x, 0 <= Z_mod_modulus x < characteristic. *)
+  (* Proof (Z_mod_two_p_range bits). *)
+
+  (* Lemma Z_mod_modulus_range': *)
+  (*   forall x, -1 < Z_mod_modulus x < modulus. *)
+  (* Proof. *)
+
+  (*   Lemma Z_mod_modulus_eq: *)
+  (*     forall x, Z_mod_modulus x = x mod modulus. *)
+  (*   Proof (Z_mod_two_p_eq wordsize). *)
+
+
+  Close Scope Z_scope.
+End ModuloPowerOfTwo.
+
+Section Range.
+Import ZArith.
+Definition in_range (x y z:Z) : bool :=
+  if Z_le_dec x y then
+    if Z_lt_dec y z then true
+    else false
+  else false.
+
+Theorem in_range_spec_l:
+  forall x y z, (x <= y < z)%Z -> in_range x y z = true.
+Proof.
+unfold in_range; intros x y z [H H'].
+destruct (Z_le_dec _ _); auto.
+destruct (Z_lt_dec _ _); auto.
+Qed.
+
+Theorem in_range_spec_r:
+  forall x y z, in_range x y z = true -> (x <= y < z)%Z.
+Proof.
+  unfold in_range.
+  intros x y z H.
+  destruct (Z_le_dec _ _); try destruct (Z_lt_dec _ _); auto; try discriminate.
+Qed.
+
+End Range.
+#[export]
+  Hint Resolve  eq_dec gt_dec lt_dec: decidable_prop.