Module Pun

Require Import Cells ArithLib.
Import Utf8 NPeano.
Import Coqlib Maps AST Integers Values Memory Globalenvs.
Import Util MemChunkTree AbMemSignatureCsharpminor.

Coercion is_true : bool >-> Sortclass.

Fixpoint get {A} (n: nat) (m: list A) {struct m} : (n <? length m)%nat → A.

Proof.

refine
  match n, m return (n <? length m)%nat → A with
  | O, a :: _ => λ _, a
  | S n', _ :: m' => @get A n' m'
  | _, _ => _
  end; clear;
  abstract easy.
Defined.

Lemma get_nth {A} d n m LT:
@get A n m LT = nth n m d.

Proof.

revert m n LT. induction m as [ | a m IH ]. easy.
intros [ | n ] LT. easy. apply IH.
Qed.

Ltac elim_div :=
  unfold Zdiv, Zmod;
    match goal with
      | H : context[ Zdiv_eucl ?X ?Y ] |- _ =>
         generalize (Z_div_mod_full X Y) ; destruct (Zdiv_eucl X Y)
      | |- context[ Zdiv_eucl ?X ?Y ] =>
         generalize (Z_div_mod_full X Y) ; destruct (Zdiv_eucl X Y)
    end; unfold Remainder.

Definition no_int_fragment : list memval → bool :=
  forallb (λ mv, match mv with Fragment (Vint _) _ _ => false | _ => true end).

Definition pun_u8 (f: cell → val) : Prop :=
  ∀ ab (κ: typed_memory_chunk) ofs,
  (align_chunk (proj1_sig κ) | ofs) →
  ∃ bytes,
  no_int_fragment bytes ∧
  f (cell_from ab (ofs, κ)) = decode_val (proj1_sig κ) bytes ∧
  length bytes = size_chunk_nat (proj1_sig κ) ∧
  (∀ i (LT: (i <? length bytes)%nat),
        f (cell_from ab (ofs + Z.of_nat i, exist _ Mint8unsigned I)) = decode_val Mint8unsigned (get i bytes LT :: nil))
.

Lemma decode_val_undef_in :
  ∀ (κ: typed_memory_chunk) m, In Undef m → Vundef = decode_val (proj1_sig κ) m.

Proof.

  intros [κ T] m IN.
  unfold decode_val.
  cut (proj_bytes m = None). intros ->; destruct κ; auto.
  destruct m as [ | x m ]; auto. destruct IN as [ -> | IN ]; auto.
  destruct x; auto. destruct m as [ | x m ]; simpl. now rewrite andb_false_r.
  destruct IN as [ -> | IN ]. now rewrite andb_false_r.
  destruct x; try now rewrite andb_false_r.
  destruct m as [ | x m ]. destruct IN. destruct IN as [ -> | IN ]. now rewrite ! andb_false_r.
  destruct x; try now rewrite ! andb_false_r.
  destruct m as [ | x m ]. destruct IN. destruct IN as [ -> | IN ]. now rewrite ! andb_false_r.
  destruct x; try now rewrite ! andb_false_r.
  destruct m as [ | x m ]. destruct IN. now rewrite ! andb_false_r.
  destruct T. destruct T.
  induction m as [ | x m IH ]. easy. destruct IN as [ -> | IN ]. easy. simpl. destruct x; auto. now rewrite IH.
Qed.

Lemma getN_map_seq_get n o m :
Mem.getN n o m = List.map (λ i, ZMap.get (o + Z.of_nat i) m) (List.seq O n).

Proof.

  revert n o. induction n as [ | n IH ]; intros o.
  easy.
  simpl. repeat f_equal. Psatz.lia.
  rewrite <- List.seq_shift, list_map_compose, IH.
  apply map_ext; intros; f_equal; Psatz.lia.
Qed.

Lemma map_nth' {A B} (f: A → B) m q q' n :
(n < length m)%nat →
List.nth n (map f m) q' = f (List.nth n m q).

Proof.

  revert n. induction m as [ | a m IH ].
  - easy.
  - intros [ | n ] N. easy. apply IH. simpl in *. Psatz.lia.
Qed.

Lemma conj' {P Q: Prop} : P → (P → Q) → P ∧ Q.

Proof.

tauto. Qed.

Remark mem_as_fun_pun_u8 ge (m: concrete_state) :
  (∀ ab b,
      block_of_ablock ge (fst m) ab = Some b →
      ∀ o, match ZMap.get o (Mem.mem_contents (snd m)) !! b with Fragment (Vint _) _ _ => False | _ => True end) →
  mem_as_fun ge m ∈ pun_u8.

Proof.

  Transparent Mem.load.
  intros NIF ab κ ofs AL.
  assert (match block_of_ablock ge (fst m) ab with
          | None => mem_as_fun ge m (cell_from ab (ofs, κ)) = Vundef
          | Some b => mem_as_fun ge m (cell_from ab (ofs, κ)) = extend (Mem.load (proj1_sig κ) (snd m) b) ofs
          end) as K.
  {
    clear.
    destruct ab as [ f x | b ]; simpl.
    case get_stk; simpl; auto. intros (tmp, e).
    case (e ! x); simpl; auto. intros (b, sz). reflexivity.
    case Genv.invert_symbol; simpl; auto.
  }
  destruct (block_of_ablock _ _ _) as [ b | ] eqn: Hab; rewrite K.
  - simpl. unfold Mem.load.
    case Mem.valid_access_dec.
    + intros VALID.
      eexists.
      refine (conj _ (conj eq_refl _)).
      {
        specialize (NIF _ _ Hab). clear -NIF.
        assert (let sz := size_chunk_nat (proj1_sig κ) in sz = 1 ∨ sz = 2 ∨ sz = 4 ∨ sz = 8)%nat as C.
        destruct κ as [() ()]; eauto.
        simpl in C.
        assert (∀ b c: bool, b → c → b && c) as K by (intros () (); auto).
        repeat destruct C as [ C | C ]; rewrite C; clear κ C;
        simpl;
        repeat (apply K; auto);
        match goal with
          |- appcontext[ ZMap.get ?o ] =>
          generalize (NIF o); destruct (ZMap.get o _) as [ | | () ];
          intros (); auto
        end. }
      apply conj'. apply Mem.getN_length.
      intros Hlen i LT.
      assert ((i < size_chunk_nat (proj1_sig κ))%nat) as Hi
      by (rewrite <- Hlen; apply NPeano.ltb_lt, LT).
      rewrite (get_nth Undef), getN_map_seq_get.
      rewrite map_nth' with (q := O). 2: now rewrite seq_length.
      rewrite seq_nth; auto.
      rewrite (block_of_ablock_Some _ _ _ Hab). simpl.
      unfold Mem.load.
      case Mem.valid_access_dec. reflexivity.
      intros X; elim X; clear X.
      split. simpl.
      intros n Hn. apply (proj1 VALID n).
      apply NPeano.ltb_lt in LT. rewrite Mem.getN_length in LT.
      unfold size_chunk_nat in LT. clear -Hn LT.
      pose proof (size_chunk_pos (proj1_sig κ)).
      zify. rewrite Z2Nat.id in LT; Psatz.lia.
      eexists. rewrite Z.mul_1_r. reflexivity.
    + intros Hvalid.
      assert (¬ Mem.range_perm (snd m) b ofs (ofs + size_chunk (proj1_sig κ)) Cur Readable) as Hperm.
      { now intros ?; apply Hvalid; split. }
      clear Hvalid.

      exists (
          List.map (λ i,
                    if Mem.valid_access_dec (snd m) Mint8unsigned b (ofs + Z.of_nat i) Readable
                    then ZMap.get (ofs + Z.of_nat i) ((Mem.mem_contents (snd m)) !! b)
                    else Undef
                   ) (List.seq O (size_chunk_nat (proj1_sig κ)))
        ).
  repeat (refine (conj' _ (λ H, _))).
  { specialize (NIF _ _ Hab). clear -NIF.
    assert (let sz := size_chunk_nat (proj1_sig κ) in sz = 1 ∨ sz = 2 ∨ sz = 4 ∨ sz = 8)%nat as C.
    destruct κ as [() ()]; eauto.
    simpl in C.
    assert (∀ b c: bool, b → c → b && c) as K by (intros () (); auto).
    repeat destruct C as [ C | C ]; rewrite C; clear κ C;
    simpl;
    repeat (apply K; auto);
    destruct Mem.valid_access_dec; auto;
    match goal with
      |- appcontext[ ZMap.get ?o ] =>
      generalize (NIF o); destruct (ZMap.get o _) as [ | | () ];
      intros (); auto
    end. }
  destruct κ as [() ?]; simpl.
  destruct (Mem.valid_access_dec _ _ _ _) as [ (Hperm0 & _) | Hvalid0 ]; auto.
  elim Hperm. generalize Hperm0. simpl. now rewrite ! Z.add_0_r.
  destruct (Mem.valid_access_dec _ _ _ _) as [ (Hperm0 & _) | Hvalid0]; auto.
  now rewrite ! Z.add_0_r in Hperm0.
  destruct (Mem.valid_access_dec _ _ _ (ofs + 0)) as [ (Hperm0 & _) | Hvalid0]; auto.
  destruct (Mem.valid_access_dec _ _ _ (ofs + 1)) as [ (Hperm1 & _) | Hvalid1].
  elim Hperm; intros i Hi; specialize (Hperm0 i); specialize (Hperm1 i). simpl in *.
  cut (i = ofs ∨ i = ofs + 1). 2: Psatz.lia. intros [ -> | -> ] ; [ apply Hperm0 | apply Hperm1 ]; Psatz.lia.
  apply (decode_val_undef_in (exist _ Mint16signed I)). simpl. intuition.
  destruct (Mem.valid_access_dec _ _ _ (ofs + 0)) as [ (Hperm0 & _) | Hvalid0]; auto.
  destruct (Mem.valid_access_dec _ _ _ (ofs + 1)) as [ (Hperm1 & _) | Hvalid1].
  elim Hperm; intros i Hi; specialize (Hperm0 i); specialize (Hperm1 i). simpl in *.
  cut (i = ofs ∨ i = ofs + 1). 2: Psatz.lia. intros [ -> | -> ] ; [ apply Hperm0 | apply Hperm1 ]; Psatz.lia.
  apply (decode_val_undef_in (exist _ Mint16unsigned I)). simpl. intuition.
  destruct (Mem.valid_access_dec _ _ _ (ofs + 0)) as [ (Hperm0 & _) | Hvalid0]; auto.
  destruct (Mem.valid_access_dec _ _ _ (ofs + 1)) as [ (Hperm1 & _) | Hvalid1].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 2)) as [ (Hperm2 & _) | Hvalid2].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 3)) as [ (Hperm3 & _) | Hvalid3].
  elim Hperm; intros i Hi; specialize (Hperm0 i); specialize (Hperm1 i); specialize (Hperm2 i); specialize (Hperm3 i). simpl in *.
  cut (i = ofs ∨ i = ofs + 1 ∨ i = ofs + 2 ∨ i = ofs + 3). 2: Psatz.lia.
  intros [ -> | [ -> | [ -> | -> ] ] ] ; [ apply Hperm0 | apply Hperm1 | apply Hperm2 | apply Hperm3 ]; Psatz.lia.
  apply (decode_val_undef_in (exist _ Mint32 I)). simpl. intuition.
  apply (decode_val_undef_in (exist _ Mint32 I)). simpl. intuition.
  apply (decode_val_undef_in (exist _ Mint32 I)). simpl. intuition.
  destruct (Mem.valid_access_dec _ _ _ (ofs + 0)) as [ (Hperm0 & _) | Hvalid0]; auto.
  destruct (Mem.valid_access_dec _ _ _ (ofs + 1)) as [ (Hperm1 & _) | Hvalid1].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 2)) as [ (Hperm2 & _) | Hvalid2].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 3)) as [ (Hperm3 & _) | Hvalid3].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 4)) as [ (Hperm4 & _) | Hvalid4].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 5)) as [ (Hperm5 & _) | Hvalid5].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 6)) as [ (Hperm6 & _) | Hvalid6].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 7)) as [ (Hperm7 & _) | Hvalid7].
  elim Hperm; intros i Hi; specialize (Hperm0 i); specialize (Hperm1 i); specialize (Hperm2 i); specialize (Hperm3 i); specialize (Hperm4 i); specialize (Hperm5 i); specialize (Hperm6 i); specialize (Hperm7 i). simpl in *.
  cut (i = ofs ∨ i = ofs + 1 ∨ i = ofs + 2 ∨ i = ofs + 3 ∨ i = ofs + 4 ∨ i = ofs + 5 ∨ i = ofs + 6 ∨ i = ofs + 7). 2: Psatz.lia.
  intros [ -> | [ -> | [ -> | [ -> | [ -> | [ -> | [ -> | -> ] ] ] ] ] ] ]; [ apply Hperm0 | apply Hperm1 | apply Hperm2 | apply Hperm3 | apply Hperm4 | apply Hperm5 | apply Hperm6 | apply Hperm7 ]; Psatz.lia.
  apply (decode_val_undef_in (exist _ Mint64 I)); simpl; intuition.
  apply (decode_val_undef_in (exist _ Mint64 I)); simpl; intuition.
  apply (decode_val_undef_in (exist _ Mint64 I)); simpl; intuition.
  apply (decode_val_undef_in (exist _ Mint64 I)); simpl; intuition.
  apply (decode_val_undef_in (exist _ Mint64 I)); simpl; intuition.
  apply (decode_val_undef_in (exist _ Mint64 I)); simpl; intuition.
  apply (decode_val_undef_in (exist _ Mint64 I)); simpl; intuition.
  destruct (Mem.valid_access_dec _ _ _ (ofs + 0)) as [ (Hperm0 & _) | Hvalid0]; auto.
  destruct (Mem.valid_access_dec _ _ _ (ofs + 1)) as [ (Hperm1 & _) | Hvalid1].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 2)) as [ (Hperm2 & _) | Hvalid2].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 3)) as [ (Hperm3 & _) | Hvalid3].
  elim Hperm; intros i Hi; specialize (Hperm0 i); specialize (Hperm1 i); specialize (Hperm2 i); specialize (Hperm3 i). simpl in *.
  cut (i = ofs ∨ i = ofs + 1 ∨ i = ofs + 2 ∨ i = ofs + 3). 2: Psatz.lia.
  intros [ -> | [ -> | [ -> | -> ] ] ] ; [ apply Hperm0 | apply Hperm1 | apply Hperm2 | apply Hperm3 ]; Psatz.lia.
  apply (decode_val_undef_in (exist _ Mfloat32 I)); simpl; intuition.
  apply (decode_val_undef_in (exist _ Mfloat32 I)); simpl; intuition.
  apply (decode_val_undef_in (exist _ Mfloat32 I)); simpl; intuition.
  destruct (Mem.valid_access_dec _ _ _ (ofs + 0)) as [ (Hperm0 & _) | Hvalid0]; auto.
  destruct (Mem.valid_access_dec _ _ _ (ofs + 1)) as [ (Hperm1 & _) | Hvalid1].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 2)) as [ (Hperm2 & _) | Hvalid2].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 3)) as [ (Hperm3 & _) | Hvalid3].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 4)) as [ (Hperm4 & _) | Hvalid4].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 5)) as [ (Hperm5 & _) | Hvalid5].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 6)) as [ (Hperm6 & _) | Hvalid6].
  destruct (Mem.valid_access_dec _ _ _ (ofs + 7)) as [ (Hperm7 & _) | Hvalid7].
  elim Hperm; intros i Hi; specialize (Hperm0 i); specialize (Hperm1 i); specialize (Hperm2 i); specialize (Hperm3 i); specialize (Hperm4 i); specialize (Hperm5 i); specialize (Hperm6 i); specialize (Hperm7 i). simpl in *.
  cut (i = ofs ∨ i = ofs + 1 ∨ i = ofs + 2 ∨ i = ofs + 3 ∨ i = ofs + 4 ∨ i = ofs + 5 ∨ i = ofs + 6 ∨ i = ofs + 7). 2: Psatz.lia.
  intros [ -> | [ -> | [ -> | [ -> | [ -> | [ -> | [ -> | -> ] ] ] ] ] ] ]; [ apply Hperm0 | apply Hperm1 | apply Hperm2 | apply Hperm3 | apply Hperm4 | apply Hperm5 | apply Hperm6 | apply Hperm7 ]; Psatz.lia.
  apply (decode_val_undef_in (exist _ Mfloat64 I)); simpl; intuition.
  apply (decode_val_undef_in (exist _ Mfloat64 I)); simpl; intuition.
  apply (decode_val_undef_in (exist _ Mfloat64 I)); simpl; intuition.
  apply (decode_val_undef_in (exist _ Mfloat64 I)); simpl; intuition.
  apply (decode_val_undef_in (exist _ Mfloat64 I)); simpl; intuition.
  apply (decode_val_undef_in (exist _ Mfloat64 I)); simpl; intuition.
  apply (decode_val_undef_in (exist _ Mfloat64 I)); simpl; intuition.
  easy. easy.
  now rewrite map_length, seq_length.
  intros i Hi. rewrite (get_nth Undef). apply NPeano.ltb_lt in Hi.
  rewrite H1 in *.
  rewrite (block_of_ablock_Some _ _ _ Hab). simpl. unfold Mem.load.
  rewrite map_nth' with (q := O), seq_nth.
  simpl. destruct (Mem.valid_access_dec _ _ _ _); auto.
  easy. now rewrite seq_length.
  - exists (List.map (λ _, Undef) (seq 0 (size_chunk_nat (proj1_sig κ)))).
    destruct κ as [() X];
      try elim X;
    (split; [ vm_compute; reflexivity | ];
     split; [ vm_compute; reflexivity | ];
     split; [ vm_compute; reflexivity | ]);
    intros i LT;
    repeat (destruct i as [ | i ]; try exact (false_not_true LT _));
    simpl in *;
    rewrite (block_of_ablock_None _ _ _ Hab); reflexivity.
  Opaque Mem.load.
Qed.

Open Scope Z_scope.

Fixpoint forallb {A} (f: A → bool) (m: list A) : bool :=
  match m with
  | nil => true
  | a :: m' => if f a then forallb f m' else false
  end.

Fixpoint forallb_forall {A} (f: A → bool) (m: list A) :
  forallb f m → ∀ a, In a m → f a = true.

Proof.

  destruct m as [ | a m ]. intros _ a ().
  simpl.
  intros H a' [ -> | IN ].
  destruct (f a'); auto.
  destruct (f a); auto.
  apply (forallb_forall A f m H a' IN).
  refine match H in _ = x return if x then _ else True with eq_refl => I end.
Qed.

Lemma In_seq x y z :
(x ≤ y → y < x + z → In y (seq x z))%nat.

Proof.

  revert x y. induction z as [ | z IH ].
  intros. zify. Psatz.lia.
  intros x y H H0. simpl.
  assert (x = y ∨ S x ≤ y)%nat as K by (Psatz.lia).
  destruct K; auto.
  right. apply IH; auto. Psatz.lia.
Qed.

Definition all_the_bytes : list byte :=
  List.map (λ n, Byte.repr (Z.of_nat n)) (seq 0 256)%nat.

Definition bytes : list byte := Eval vm_compute in all_the_bytes.

Definition for_all_byte (f: byte → bool) : bool :=
  forallb f bytes.

Lemma for_all_byte_correct f :
  for_all_byte f → ∀ b : byte, f b.

Proof.

  unfold for_all_byte, is_true.
  intros H b.
  apply (forallb_forall _ _ H).
  change (In b all_the_bytes).
  apply in_map_iff.
  exists (Z.to_nat (Byte.unsigned b)).
  pose proof (Byte.unsigned_range b) as R.
  change Byte.modulus with 256 in R.
  rewrite Z2Nat.id, Byte.repr_unsigned.
  split. easy.
  apply In_seq; zify; try Psatz.lia.
  rewrite Z2Nat.id; Psatz.lia.
  Psatz.lia.
Qed.

Lemma z8 x y :
Int.zero_ext 8 (Int.repr x) = Int.zero_ext 8 (Int.repr (x + y * 256)).

Proof.

  Opaque Z.mul.
  rewrite ! Int.zero_ext_and; try Psatz.lia. simpl.
  assert (Int.repr 255 = Int.sub (Int.repr 256) Int.one) as Hff by reflexivity.
  rewrite Hff. clear Hff.
  erewrite <- ! Int.modu_and. 2: reflexivity. 2: reflexivity.
  unfold Int.modu. f_equal.
  change (Int.unsigned (Int.repr 256)) with 256.
  rewrite ! Int.unsigned_repr_eq.
  assert (Int.modulus = 4294967296) as H by reflexivity.
  rewrite H. clear H.
  assert (256 | 4294967296) by (exists (4294967296 / 256); reflexivity).
  rewrite <- ! Znumtheory.Zmod_div_mod; try easy.
  symmetry. apply Z_mod_plus_full.
Qed.

Corollary ze8 x y:
eqm 256 x y →
Int.zero_ext 8 (Int.repr x) = Int.zero_ext 8 (Int.repr y).

Proof.

  intros EQM. apply eqm_congr in EQM. 2: reflexivity.
  destruct EQM as (n & -> ).
  apply z8.
Qed.

Lemma decode_int_1 :
∀ i₀,
decode_int (i₀ :: nil) = Byte.unsigned i₀.

Proof.

intros i₀. unfold decode_int, rev_if_be. destruct Archi.big_endian; simpl; Psatz.lia.
Qed.

Lemma decode_int_LE_2 :
  Archi.big_endian = false →
  ∀ i₀ i₁,
  decode_int (i₀ :: i₁ :: nil) = Byte.unsigned i₀ + 256 * Byte.unsigned i₁.

Proof.

intros LE i₀ i₁. unfold decode_int, rev_if_be. rewrite LE; simpl; Psatz.lia.
Qed.

Lemma decode_int_LE_4 :
  Archi.big_endian = false →
  ∀ i₀ i₁ i₂ i₃,
  decode_int (i₀ :: i₁ :: i₂ :: i₃ :: nil) = Byte.unsigned i₀ + (Byte.unsigned i₁ + (Byte.unsigned i₂ + Byte.unsigned i₃ * 256) * 256) * 256.

Proof.

intros LE i₀ i₁ i₂ i₃. unfold decode_int, rev_if_be. rewrite LE; simpl; Psatz.lia.
Qed.

Lemma decode_shift_1u :
  Archi.big_endian = false →
  ∀ i₀ i₁,
    Int.repr (decode_int (i₁ :: nil)) =
    Int.shru (Int.zero_ext 16 (Int.repr (decode_int (i₀ :: i₁ :: nil)))) (Int.repr (8 * 1)).

Proof.

  intros LE i₀ i₁.
  rewrite decode_int_1, (decode_int_LE_2 LE).
  rewrite (Int.zero_ext_shru_shl 16). 2: exact (conj eq_refl eq_refl).
  rewrite Int.shru_shru; try reflexivity.
  simpl. change (Int.add (Int.repr 16) (Int.repr (8 * 1))) with (Int.repr 24).
  rewrite Int.shl_mul_two_p, Int.shru_div_two_p.
  unfold Int.mul. rewrite Int.unsigned_repr_eq.
  change (Int.unsigned (Int.repr (two_p (Int.unsigned (Int.repr 16))))) with 65536.
  rewrite Int.unsigned_repr_eq.
  change (two_p (Int.unsigned (Int.repr 24))) with 16777216.
  rewrite (Coqlib.Zmod_small (_ + _ * _)).
  2: change Int.modulus with 4294967296;
  generalize (Byte.unsigned_range i₀);
  generalize (Byte.unsigned_range i₁);
  change Byte.modulus with 256;
  Psatz.lia.
  rewrite Coqlib.Zmod_small.
  2: change Int.modulus with 4294967296;
  generalize (Byte.unsigned_range i₀);
  generalize (Byte.unsigned_range i₁);
  change Byte.modulus with 256;
  Psatz.lia.
  replace (((Byte.unsigned i₀ + 256 * Byte.unsigned i₁) * 65536))
  with ((Byte.unsigned i₀ * 65536 + Byte.unsigned i₁ * 16777216)).
  2: Psatz.lia.
  rewrite Z_div_plus_full.
  2: Psatz.lia.
  rewrite Zdiv_small. reflexivity.
  generalize (Byte.unsigned_range i₀);
  change Byte.modulus with 256;
  Psatz.lia.
Qed.

Lemma decode_shift_1s :
  Archi.big_endian = false →
  ∀ i₀ i₁,
    Int.zero_ext 8 (Int.repr (decode_int (i₁ :: nil))) =
    Int.zero_ext 8 (Int.shru (Int.sign_ext 16 (Int.repr (decode_int (i₀ :: i₁ :: nil)))) (Int.repr (8 * 1))).

Proof.

  intros LE i₀ i₁.
  rewrite decode_int_1.
  rewrite (decode_int_LE_2 LE).
  apply int_eq.
  revert i₁. apply (for_all_byte_correct).
  revert i₀. apply (for_all_byte_correct).
  vm_compute.
  exact_no_check (eq_refl true).
Qed.

Lemma NS1 (LE: Archi.big_endian = false) i0 i1 i2 i3 :
  Int.zero_ext 8 (Int.repr (decode_int (i1 :: nil))) =
  Int.zero_ext 8
               (Int.shru (Int.repr (decode_int (i0 :: i1 :: i2 :: i3 :: nil)))
                         (Int.repr (8 * 1))).

Proof.

  rewrite decode_int_1, decode_int_LE_4; auto.
  rewrite Int.shru_div_two_p. simpl.
  change (two_p (Int.unsigned (Int.repr (8 * 1)))) with 256.
  rewrite Int.unsigned_repr_eq.
  rewrite Zmod_small.
  rewrite Z_div_plus_full.
  replace (Byte.unsigned i0 / 256) with 0. simpl.
  apply ze8, congr_eqm. reflexivity.
  eexists. reflexivity.
  clear. generalize (Byte.unsigned_range i0).
  change Byte.modulus with 256. elim_div. Psatz.lia.
  Psatz.lia.
  generalize (Byte.unsigned_range i0).
  generalize (Byte.unsigned_range i1).
  generalize (Byte.unsigned_range i2).
  generalize (Byte.unsigned_range i3).
  change Byte.modulus with 256.
  change Int.modulus with 4294967296.
  Psatz.lia.
Qed.

Lemma NS2 (LE: Archi.big_endian = false) i0 i1 i2 i3 :
  Int.zero_ext 8 (Int.repr (decode_int (i2 :: nil))) =
  Int.zero_ext 8
               (Int.shru (Int.repr (decode_int (i0 :: i1 :: i2 :: i3 :: nil)))
                         (Int.repr (8 * 2))).

Proof.

  rewrite decode_int_1, decode_int_LE_4; auto.
  rewrite Int.shru_div_two_p.
  rewrite Int.unsigned_repr_eq.
  apply ze8, congr_eqm. reflexivity.
  rewrite Zmod_small.
  rewrite ! Z.mul_add_distr_r.
  rewrite Z.add_assoc.
  rewrite <- Z.mul_assoc.
  rewrite <- Z.mul_assoc.
  rewrite <- Z.mul_add_distr_r.
  change (two_p _) with 65536.
  rewrite Z_div_plus_full. 2: Psatz.lia.
  rewrite <- (Z.add_0_l (Byte.unsigned i2)) at 1.
  apply congr_plus_compat.
  exists 0.
  generalize (Byte.unsigned_range i0).
  generalize (Byte.unsigned_range i1).
  change Byte.modulus with 256.
  elim_div. Psatz.lia.
  rewrite <- (Z.add_0_r (Byte.unsigned i2)) at 1.
  apply congr_plus_compat. apply congr_refl.
  eexists. reflexivity.
  generalize (Byte.unsigned_range i0).
  generalize (Byte.unsigned_range i1).
  generalize (Byte.unsigned_range i2).
  generalize (Byte.unsigned_range i3).
  change Byte.modulus with 256.
  change Int.modulus with 4294967296.
  Psatz.lia.
Qed.

Lemma NS3 (LE: Archi.big_endian = false) i0 i1 i2 i3 :
  Int.zero_ext 8 (Int.repr (decode_int (i3 :: nil))) =
  Int.zero_ext 8
               (Int.shru (Int.repr (decode_int (i0 :: i1 :: i2 :: i3 :: nil)))
                         (Int.repr (8 * 3))).

Proof.

  rewrite decode_int_1, decode_int_LE_4; auto.
  rewrite Int.shru_div_two_p.
  rewrite Int.unsigned_repr_eq.
  change (two_p _) with 16777216.
  rewrite Zmod_small.
  rewrite ! Z.mul_add_distr_r.
  rewrite ! Z.add_assoc, <- ! Z.mul_assoc.
  rewrite Z_div_plus_full. 2: Psatz.lia.
  f_equal. f_equal.
  generalize (Byte.unsigned_range i0).
  generalize (Byte.unsigned_range i1).
  generalize (Byte.unsigned_range i2).
  change Byte.modulus with 256.
  elim_div. Psatz.lia.
  generalize (Byte.unsigned_range i0).
  generalize (Byte.unsigned_range i1).
  generalize (Byte.unsigned_range i2).
  generalize (Byte.unsigned_range i3).
  change Byte.modulus with 256.
  change Int.modulus with 4294967296.
  Psatz.lia.
Qed.

Lemma byte_int_range b :
0 <= Byte.unsigned b <= Int.max_unsigned.

Proof.

    generalize (Byte.unsigned_range b).
    change Byte.modulus with 256. change Int.max_unsigned with 4294967295.
    Psatz.lia.
  Qed.

  Lemma unsigned_add x y :
    Int.unsigned x + Int.unsigned y < Int.modulus →
    Int.unsigned (Int.add x y) = Int.unsigned x + Int.unsigned y.

Proof.

    intros H.
    rewrite Int.unsigned_add_carry.
    unfold Int.add_carry. destruct (Coqlib.zlt _ _) as [ X | X ].
    now rewrite Z.sub_0_r.
    rewrite Z.add_0_r in X. Psatz.lia.
  Qed.

Lemma mul_byte0 :
∀ b: byte, Int.unsigned (Int.mul (Int.zero_ext 8 (Int.repr (Byte.unsigned b))) (Int.repr 256)) < 65281.

Proof.

      clear. intros b. apply Z.ltb_lt. revert b.
      apply (for_all_byte_correct). vm_compute. reflexivity.
  Qed.

Lemma mul_byte1 :
∀ b: byte, Int.unsigned (Int.mul (Int.zero_ext 8 (Int.repr (Byte.unsigned b))) (Int.repr 65536)) < 16711681.

Proof.

      clear. intros b. apply Z.ltb_lt. revert b.
      apply (for_all_byte_correct). vm_compute. reflexivity.
  Qed.

Lemma mul_byte2 :
∀ b: byte, Int.unsigned (Int.mul (Int.zero_ext 8 (Int.repr (Byte.unsigned b))) (Int.repr 16777216)) < 4278190081.

Proof.

      clear. intros b. apply Z.ltb_lt. revert b.
      apply (for_all_byte_correct). vm_compute. reflexivity.
  Qed.