From compcert Require Export common.AST cfrontend.Ctypes cfrontend.Clight.
Export Cop.
Require Export VST.floyd.base2.
Require Export VST.floyd.functional_base.
Require Export VST.floyd.client_lemmas.
Require Export VST.floyd.go_lower.
Require Export VST.floyd.closed_lemmas.
Require Export VST.floyd.compare_lemmas.
Require Export VST.floyd.semax_tactics.
Require Export VST.floyd.forward.
Require Export VST.floyd.subsume_funspec.
Require Export VST.floyd.call_lemmas.
Require Export VST.floyd.forward_lemmas.
Require Export VST.floyd.for_lemmas.
Require Export VST.floyd.nested_pred_lemmas.
Require Export VST.floyd.nested_field_lemmas.
Require Export VST.floyd.efield_lemmas.
Require Export VST.floyd.mapsto_memory_block.
Require Export VST.floyd.aggregate_type.
Require VST.floyd.aggregate_pred. Export floyd.aggregate_pred.aggregate_pred.
Require Export VST.floyd.reptype_lemmas.
Require Export VST.floyd.simpl_reptype.
Require Export VST.floyd.data_at_rec_lemmas.
Require Export VST.floyd.field_at.
Require Export VST.floyd.field_at_wand.
Require Export VST.floyd.field_compat.
Require Export VST.floyd.stronger.
Require Export VST.floyd.loadstore_mapsto.
Require Export VST.floyd.loadstore_field_at.
Require Export VST.floyd.nested_loadstore.
Require Export VST.floyd.local2ptree_denote.
Require Export VST.floyd.local2ptree_eval.
Require Export VST.floyd.local2ptree_typecheck.
Require Export VST.floyd.proj_reptype_lemmas.
Require Export VST.floyd.replace_refill_reptype_lemmas.
Require Export VST.floyd.sc_set_load_store.
Require Export VST.floyd.unfold_data_at.
Require Export VST.floyd.entailer.
Require Export VST.floyd.globals_lemmas.
Require Export VST.floyd.diagnosis.
Require Export VST.floyd.freezer.
Require Export VST.floyd.deadvars.
Require Export VST.floyd.hints.
Require Export VST.floyd.Clightnotations.
Require VST.msl.iter_sepcon.
Require VST.msl.wand_frame.
Require VST.msl.wandQ_frame.

Arguments semax {CS} {Espec} Delta Pre%assert cmd%C Post%assert.
Export ListNotations.
Export Clight_Cop2.

Hint Rewrite add_repr mul_repr sub_repr : entailer_rewrite.
Hint Rewrite ptrofs_add_repr ptrofs_mul_repr ptrofs_sub_repr : entailer_rewrite.
Hint Rewrite mul64_repr add64_repr sub64_repr or64_repr and64_repr : entailer_rewrite.
Hint Rewrite neg_repr neg64_repr : entailer_rewrite.
Hint Rewrite ptrofs_to_int_repr: entailer_rewrite norm.

Lemma Vptrofs_unfold_false: 
Archi.ptr64 = false -> Vptrofs = fun x => Vint (Ptrofs.to_int x).
Proof.
(* Goal: forall (x y : Z) (_ : and (Z.le Z0 x) (Z.le x Int.max_unsigned)) (_ : and (Z.le Z0 y) (Z.le y Int.max_unsigned)), @eq Int.int (Int.modu (Int.repr x) (Int.repr y)) (Int.repr (Z.modulo x y)) *)
intros. unfold Vptrofs.
(* Goal: @eq (forall _ : Ptrofs.int, val) (fun n : Ptrofs.int => if Archi.ptr64 then Vlong (Ptrofs.to_int64 n) else Vint (Ptrofs.to_int n)) (fun x : Ptrofs.int => Vlong (Ptrofs.to_int64 x)) *)
extensionality x.
(* Goal: @eq val (if Archi.ptr64 then Vlong (Ptrofs.to_int64 x) else Vint (Ptrofs.to_int x)) (Vlong (Ptrofs.to_int64 x)) *)
rewrite H.
(* Goal: @eq Int.int (Int.repr (Z.modulo x y)) (Int.repr (Z.modulo x y)) *)
auto.
Qed.

Lemma Vptrofs_unfold_true: 
Archi.ptr64 = true -> Vptrofs = fun x => Vlong (Ptrofs.to_int64 x).
Proof.
(* Goal: forall (x y : Z) (_ : and (Z.le Z0 x) (Z.le x Int.max_unsigned)) (_ : and (Z.le Z0 y) (Z.le y Int.max_unsigned)), @eq Int.int (Int.modu (Int.repr x) (Int.repr y)) (Int.repr (Z.modulo x y)) *)
intros. unfold Vptrofs.
(* Goal: @eq (forall _ : Ptrofs.int, val) (fun n : Ptrofs.int => if Archi.ptr64 then Vlong (Ptrofs.to_int64 n) else Vint (Ptrofs.to_int n)) (fun x : Ptrofs.int => Vlong (Ptrofs.to_int64 x)) *)
extensionality x.
(* Goal: @eq val (if Archi.ptr64 then Vlong (Ptrofs.to_int64 x) else Vint (Ptrofs.to_int x)) (Vlong (Ptrofs.to_int64 x)) *)
rewrite H.
(* Goal: @eq Int.int (Int.repr (Z.modulo x y)) (Int.repr (Z.modulo x y)) *)
auto.
Qed.

Lemma modu_repr: forall x y, 
   0 <= x <= Int.max_unsigned ->
   0 <= y <= Int.max_unsigned ->
  Int.modu (Int.repr x) (Int.repr y) = Int.repr (x mod y).
Proof.
(* Goal: forall (x y : Z) (_ : and (Z.le Z0 x) (Z.le x Int.max_unsigned)) (_ : and (Z.le Z0 y) (Z.le y Int.max_unsigned)), @eq Int.int (Int.modu (Int.repr x) (Int.repr y)) (Int.repr (Z.modulo x y)) *)
intros. unfold Int.modu. rewrite !Int.unsigned_repr by auto. auto.
Qed.
Hint Rewrite modu_repr using rep_omega : entailer_rewrite norm.

Hint Rewrite Vptrofs_unfold_false using reflexivity: entailer_rewrite norm.
Hint Rewrite Vptrofs_unfold_true using reflexivity: entailer_rewrite norm.

Hint Extern 1 (Vundef = default_val _) => reflexivity : cancel.
Hint Extern 1 (default_val _ = Vundef) => reflexivity : cancel.
Hint Extern 1 (list_repeat _ Vundef = default_val _) => reflexivity : cancel.
Hint Extern 1 (default_val _ = list_repeat _ Vundef) => reflexivity : cancel.
Hint Extern 1 (Vundef :: _ = default_val _) => reflexivity : cancel.
Hint Extern 1 (default_val _ = Vundef :: _) => reflexivity : cancel.
Hint Extern 1 (@nil _ = default_val _) => reflexivity : cancel.
Hint Extern 1 (default_val _ = @nil _) => reflexivity : cancel.

Instance Inhabitant_mpred : Inhabitant mpred := @FF mpred Nveric.
Instance Inhabitant_share : Inhabitant share := Share.bot.

Arguments deref_noload ty v / .
Arguments nested_field_array_type {cs} t gfs lo hi / .
Arguments nested_field_type {cs} t gfs / .  (* redundant? *)
Arguments nested_field_offset {cs} t gfs / .  (* redundant? *)
Arguments Z.mul !x !y.
Arguments Z.sub !m !n.
Arguments Z.add !x !y.
Global Transparent peq.
Global Transparent Archi.ptr64.

Ltac step :=
first [ progress Intros
       | let x := fresh "x" in Intros x
       | forward
       | forward_if
       | forward_call
       | rep_omega | cstring' | list_solve
       | EExists
       | progress (autorewrite with sublist in *|-)
       | progress (autorewrite with sublist)
       | progress (autorewrite with norm)
       | cstring1
       | deadvars!
       | progress_entailer
       ].


