text:
Require Import compcert.common.Memory.
Require Import compcert.common.AST.     (*for typ*)
Require Import compcert.common.Values. (*for val*)
Require Import compcert.common.Events.
Require Import compcert.common.Globalenvs.
Require Import compcert.lib.Integers.
Require Import compcert.common.Values.

Require Import VST.msl.Axioms.
Require Import Coq.ZArith.ZArith.
Require Import VST.sepcomp.semantics.
Require Import VST.sepcomp.event_semantics.
Require Export VST.concurrency.common.semantics.
Require Export VST.concurrency.common.lksize.
Require Import VST.concurrency.common.threadPool. Export threadPool.

Require Import VST.concurrency.common.machine_semantics.
Require Import VST.concurrency.common.permissions.
Require Import VST.concurrency.common.bounded_maps.
Require Import VST.concurrency.common.addressFiniteMap.

Require Import VST.concurrency.common.scheduler.
Require Import Coq.Program.Program.

Require Import VST.concurrency.compiler.safety.

Require Import VST.concurrency.compiler.coinductive_safety.

Require Import VST.concurrency.common.HybridMachineSig.

Require Import VST.veric.res_predicates.

Require Import VST.concurrency.common.HybridMachine.

Require Import VST.concurrency.compiler.CoreSemantics_sum.

Require Import compcert.common.Smallstep.

Require Import VST.concurrency.common.machine_semantics_lemmas.

Import Events event_semantics Values.

Set Implicit Arguments.

Section HybridSimulation.

  (*
  Variable (Sems Semt : semantics.Semantics).
  Variable (hb1 hb2: option nat).
  (*Variable (Resources : Resources_rec).
  Variable (MatchCAsm: meminj -> corestate -> mem -> Asm_coop.state -> mem -> Prop).*)

  Definition HM1:=HybridMachine hb1 Sems Semt.
  Definition HM2:=HybridMachine hb2 Sems Semt.

  Notation Sem1:=(ConcurMachineSemantics HM1).
  Notation Sem2:=(ConcurMachineSemantics HM2).

  Notation C1:= (MachState HybridMachine.Resources
                          (Sem hb1 Sems Semt) (ThreadPool hb1 Sems Semt)).
  Notation C2:= (MachState HybridMachine.Resources
                          (Sem hb2 Sems Semt) (ThreadPool hb2 Sems Semt)).
  Notation G1:= (semG (Sem hb1 Sems Semt)).
  Notation G2:= (semG (Sem hb2 Sems Semt)).
  Variable ge1:G1.
  Variable ge2:G2.
  Variable (ge_inv: G1 -> G2 -> Prop). *)

  Context (SG TG TID SCH SC TC R1 R2 (*s_thread_type t_thread_type*): Type).
  Variable SourceHybridMachine: @ConcurSemantics SG TID SCH (list machine_event) SC mem R1.
  Variable TargetHybridMachine: @ConcurSemantics TG TID SCH (list machine_event) TC mem R2.
  (*
     Variable opt_init_mem_source : option Memory.Mem.mem.
     Variable opt_init_mem_target : option Memory.Mem.mem.
  *)

  (* Inductive inject_address (f : meminj) : address -> address -> Prop :=
  | inj_addr : forall b1 delt b2 ofs, f b1 = Some (b2, ofs) ->
      inject_address f (b1, ofs) (b2, ofs + delt). *)

  Inductive inject_address f: address -> address -> Prop :=
  | build_inject_address:
      forall b1 b2 ofs1 ofs2 delt,
        f b1 = Some (b2, delt) ->
        ofs2 = ofs1 + delt ->
        inject_address f (b1, ofs1) (b2,ofs2).
  Lemma inject_address_incr:
    forall f f' l1 l2,
      inject_incr f f' ->
      inject_address f l1 l2 ->
      inject_address f' l1 l2.
  Proof.
    intros * Hincr Hinj. inv Hinj.
    econstructor; auto.
    eapply Hincr; assumption.
  Qed.
  Definition inject_delta_content: meminj -> delta_content -> delta_content -> Prop:=
    fun f dc1 dc2 =>
    True.
  (* Same as memories that are injected...
     but, we should reconsider if we really want sync_events.
   *)

  Inductive inject_sync_event (f : meminj) : sync_event -> sync_event -> Prop :=
  | inj_release : forall l1 l2 r1 r2, inject_address f l1 l2 ->
      match r1, r2 with
      | Some (a1), Some (a2) => inject_delta_content f a1 a2
      | None, None => True
      | _, _ => False
      end ->
      inject_sync_event f (release l1 r1) (release l2 r2)
  | inj_acquire : forall l1 l2 r1 r2, inject_address f l1 l2 ->
      match r1, r2 with
      | Some (a1), Some (a2) => inject_delta_content f a1 a2
      | None, None => True
      | _, _ => False
      end ->
      inject_sync_event f (acquire l1 r1) (acquire l2 r2)
  | inj_mklock : forall l1 l2, inject_address f l1 l2 ->
      inject_sync_event f (mklock l1) (mklock l2)
  | inj_freelock : forall l1 l2, inject_address f l1 l2 ->
      inject_sync_event f (freelock l1) (freelock l2)
  | inj_spawn : forall l1 l2 r1 r1' r2 r2', inject_address f l1 l2 ->
      match r1, r2 with
      | Some a1, Some a2 =>
          inject_delta_content f a1 a2
      | None, None => True
      | _, _ => False
      end ->
      match r1', r2' with
      | Some a1', Some a2' =>
          inject_delta_content f a1' a2'
      | None, None => True
      | _, _ => False
      end ->
      inject_sync_event f (spawn l1 r1 r1') (spawn l2 r2 r2')
  | inj_failacq : forall l1 l2, inject_address f l1 l2 ->
      inject_sync_event f (failacq l1) (failacq l2).
  Inductive inj_free (f:meminj): block * Z * Z -> block * Z * Z -> Prop:=
  | build_inj_free:  forall b1 b2 lo1 lo2 hi1 hi2 delt,
      f b1 = Some (b2, delt) ->
      lo2 = lo1 + delt ->
      hi2 = hi1 + delt ->
      inj_free f (b1,lo1,hi1) (b2,lo2,hi2).
  Lemma inj_free_incr:
    forall f f' ls1 ls2,
      inject_incr f f' ->
      inj_free f  ls1 ls2 ->
      inj_free f' ls1 ls2.
  Proof. intros; inv H0; econstructor; eauto. Qed.

  Inductive inject_mem_event : meminj -> mem_event -> mem_event -> Prop:=
  | inject_Write: forall f b1 b2 ofs1 ofs2 delt ls1 ls2,
      f b1 = Some (b2, delt) ->
      ofs2 = ofs1 + delt ->
      list_memval_inject f ls1 ls2 ->
      inject_mem_event f (Write b1 ofs1 ls1) (Write b2 ofs2 ls2)
  | inject_Read: forall f b1 b2 ofs1 ofs2 delt ls1 ls2 n,
      f b1 = Some (b2, delt) ->
      ofs2 = ofs1 + delt ->
      list_memval_inject f ls1 ls2 ->
      inject_mem_event f (Read b1 ofs1 n ls1)(Read b2 ofs2 n ls2)
  | inject_Alloc: forall f b1 b2 lo1 lo2 hi1 hi2 delt,
      f b1 = Some (b2, delt) ->
      lo2 = lo1 + delt ->
      hi2 = hi1 + delt ->
      inject_mem_event f (Alloc b1 lo1 hi1) (Alloc b2 lo2 hi2)
  | inject_Free: forall f ls1 ls2,
      List.Forall2 (inj_free f) ls1 ls2 ->
      inject_mem_event f (Free ls1) (Free ls2).
  Lemma list_memval_inject_incr:
        forall f f' ls1 ls2,
          inject_incr f f' ->
          list_memval_inject f  ls1 ls2 ->
          list_memval_inject f' ls1 ls2.
  Proof.
    intros.
    eapply list_map_rel_ind; eauto.
    - constructor.
    - constructor; eauto.
      eapply memval_inject_incr; eassumption.
  Qed.

  Lemma Forall2_impl: forall {A B} (P Q : A -> B -> Prop) l1 l2,
      (forall a b, P a b -> Q a b) -> List.Forall2 P l1 l2 -> List.Forall2 Q l1 l2.
  Proof.
    induction 2; constructor; auto.
  Qed.
  Lemma inject_mem_event_incr:
    forall f f' a b,
      inject_incr f f' ->
      inject_mem_event f a b ->
      inject_mem_event f' a b.
  Proof.
    intros.
    inv H0; [econstructor 1
            |econstructor 2
            |econstructor 3
            |econstructor 4]; eauto.
    - eapply list_memval_inject_incr; eauto.
    - eapply list_memval_inject_incr; eauto.
    - eapply Forall2_impl.
      2: apply H1.
      intros. eapply inj_free_incr; eauto.
  Qed.

  Inductive inject_mevent (f : meminj) : machine_event -> machine_event -> Prop :=
  | inj_internal : forall n me1 me2, inject_mem_event f me1 me2 ->
      inject_mevent f (internal n me1) (internal n me2)
  | inj_external : forall n se1 se2, inject_sync_event f se1 se2 ->
                                inject_mevent f (external n se1) (external n se2).

  Lemma inject_sync_event_incr:
    forall f f' a b,
      inject_incr f f' ->
      inject_sync_event f a b ->
      inject_sync_event f' a b.
  Proof.
    intros. inv H0;
              [constructor 1
              |constructor 2
              |constructor 3
              |constructor 4
              |constructor 5
              |constructor 6]; auto;
                eapply inject_address_incr; eassumption.
  Qed.

  Lemma inject_mevent_incr:
        forall f f' a b,
          inject_incr f f' ->
          inject_mevent f a b ->
          inject_mevent f' a b.
      Proof.
        intros.
        inv H0; simpl; [left | right].
        - eapply inject_mem_event_incr; eauto.
        - eapply inject_sync_event_incr; eauto.
      Qed.
  Lemma inject_incr_trace:
    forall (tr1 tr2 : list Events.machine_event) (mu f' : meminj),
      inject_incr mu f' ->
      List.Forall2 (inject_mevent mu) tr1 tr2 ->
      List.Forall2 (inject_mevent f') tr1 tr2.
  Proof.
    intros. eapply Forall2_impl; try eassumption.
    - intros; eapply inject_mevent_incr; eassumption.
  Qed.

  Record HybridMachine_simulation_properties
         (index: Type)(match_state : index -> meminj -> SC -> mem -> TC -> mem -> Prop) :=
    { core_ord : index -> index -> Prop
      ; core_ord_wf : well_founded core_ord

      (* This is the match relation for initial state of the initial core:*)
      (* That is property given by sequential theorem about inital_states *)
      (*; initial_source_thread:
          mem -> s_thread_type -> val -> seq.seq val -> Prop
      ; initial_target_thread:
          mem -> t_thread_type -> val -> seq.seq val -> Prop *)
      ; initial_setup :
          forall (*s_init_thread*) s_mem s_mem' main main_args s_mach_state r1,
            (*initial_source_thread s_mem s_init_thread main main_args -> *)
            machine_semantics.initial_machine SourceHybridMachine r1 s_mem s_mach_state s_mem' main main_args ->
            exists j cd t_mach_state t_mem t_mem' r2,
              machine_semantics.initial_machine TargetHybridMachine r2 t_mem t_mach_state t_mem' main main_args
           /\ match_state cd j s_mach_state s_mem' t_mach_state t_mem'
      ; thread_diagram :
          forall sge tge U tr1 st1 m1 st1' m1',
            thread_step SourceHybridMachine sge U st1 m1 st1' m1' ->
            forall cd tr2 st2 mu m2,
              match_state cd mu st1 m1 st2 m2 ->
              Forall2 (inject_mevent mu) tr1 tr2 ->
              exists st2', exists m2', exists cd', exists mu',
                      match_state cd' mu' st1' m1' st2' m2'
                      /\ Forall2 (inject_mevent mu') tr1 tr2
                      /\ (thread_step_plus (TargetHybridMachine) tge U st2 m2 st2' m2'
               \/ (thread_step_star (TargetHybridMachine) tge U st2 m2 st2' m2' /\ core_ord cd' cd))
      ; machine_diagram :
          forall sge tge U tr1 st1 m1 U' tr1' st1' m1',
            machine_step SourceHybridMachine sge U tr1 st1 m1 U' tr1' st1' m1' ->
            forall cd tr2 st2 mu m2,
              match_state cd mu st1 m1 st2 m2 ->
              Forall2 (inject_mevent mu) tr1 tr2 ->
              exists tr2', exists st2', exists m2', exists cd', exists mu',
                      match_state cd' mu' st1' m1' st2' m2'
                      /\ Forall2 (inject_mevent mu') tr1' tr2'
                      /\ machine_step (TargetHybridMachine) tge U tr2 st2 m2 U' tr2' st2' m2'
      ; thread_halted :
          forall cd mu U c1 m1 c2 m2 v1,
            match_state cd mu c1 m1 c2 m2 ->
            conc_halted SourceHybridMachine U c1 = Some v1 ->
            exists v2,
              conc_halted TargetHybridMachine U c2 = Some v2
      ; thread_running:
          forall cd mu c1 m1 c2 m2 ,
            match_state cd mu c1 m1 c2 m2 ->
            forall i, running_thread SourceHybridMachine c1 i <-> running_thread TargetHybridMachine c2 i
    }.

  Record HybridMachine_simulation:=
    { index: Type
      ; match_state : index -> meminj -> SC -> mem -> TC -> mem -> Prop
      ; SIM:> @HybridMachine_simulation_properties index match_state}.

End HybridSimulation.

author: PrincetonUniversity

repo: VST


text:
Require Import
  MathClasses.interfaces.abstract_algebra MathClasses.theory.categories MathClasses.orders.maps MathClasses.interfaces.orders MathClasses.orders.orders
  MathClasses.interfaces.functors.
Require MathClasses.categories.setoids.

Inductive Object := object { T:> Type; e: Equiv T; le: Le T; setoid_proof: Setoid T;  po_proof: PartialOrder le }.
Existing Instance e.
Existing Instance le.
Existing Instance setoid_proof.
Existing Instance po_proof.
Implicit Arguments object [[e] [le] [setoid_proof] [po_proof]]
                          [[e] [setoid_proof] [po_proof]]
                          [[setoid_proof] [po_proof]].

Section contents.
  Global Instance Arrow: Arrows Object := λ A B, sig (@OrderPreserving A B _ _ _ _).

  Global Program Instance: ∀ x y: Object, Equiv (x ⟶ y) := λ _ _, respectful (=) (=).

  Existing Instance order_morphism_mor.
  Global Instance: ∀ x y: Object, Setoid (x ⟶ y).
  Proof with intuition.
   intros x y.
   constructor.
     intros [? ?] ? ? E. now rewrite E.
    intros ? ? E ? ? ?. symmetry...
   intros [f Pf] [g Pg] [h Ph] E1 E2 a b E3. simpl.
   transitivity (g a)...
  Qed.

  Global Program Instance: CatId Object := λ _, id.

  Local Obligation Tactic := idtac.
  Global Program Instance: CatComp Object := λ _ _ _, compose.

  Instance: ∀ x y z: Object, Proper ((=) ==> (=) ==> (=)) (comp x y z).
  Proof. repeat intro. simpl. firstorder. Qed.

  Global Instance: Category Object.
  Proof.
   constructor; try apply _.
     intros ? ? ? ? [??] [??] [??] ? ? E. simpl. now rewrite E.
    intros ? ? [??] ? ? E. simpl. now rewrite E.
   intros ? ? [??] ? ? E. simpl. now rewrite E.
  Qed.

  Definition forget (O: Object) : setoids.Object := setoids.object O.
  Global Program Instance: Fmap forget := λ x y f, f.

  Global Instance: Functor forget _ := {}.
  Proof.
    * constructor; try typeclasses eauto.
      intros ???. assumption.
    * intros ????. assumption.
    * intros ? ? [] ? [] ? ? ?.
    simpl. rewrite H.
    reflexivity.
  Qed.
End contents.

author: agumonkey

repo: cats

save_path: github-repos/coq/agumonkey-cats


Require Import Recdef.
Require Import floyd.proofauto.
Local Open Scope logic.
Require Import Coq.Lists.List. Import ListNotations.
Require Import sha.general_lemmas.

Require Import tweetnacl20140427.split_array_lemmas.
Require Import ZArith.
Require Import tweetnacl20140427.Salsa20.
Require Import tweetnacl20140427.tweetnaclVerifiableC.
Require Import tweetnacl20140427.tweetNaclBase.
Instance CompSpecs : compspecs.
Proof. make_compspecs prog. Defined.

Lemma data_at_ext sh t v v' p: v=v' -> data_at sh t v p |-- data_at sh t v' p.
Proof. intros; subst. trivial. Qed.

(*
Definition EightWord (q:QuadWord * QuadWord) (v:val) : mpred :=
  match q with ((q0, q1, q2, q3),(q4, q5, q6, q7)) =>
    data_at Tsh (Tarray tuchar 4 noattr) (map Vint [q0; q1; q2; q3; q4; q5; q6; q7]) v
  end.*)
Definition QuadByte2ByteList (B:QuadByte) : list byte :=
  match B with (b0, b1, b2, b3) => [b0; b1; b2; b3]
  end.

Definition QuadByte2ValList (B:QuadByte) : list val :=
   map Vint (map Int.repr (map Byte.unsigned (QuadByte2ByteList B))).

Lemma QuadByteValList_length q: length (QuadByte2ValList q) = 4%nat.
  destruct q as [[[? ?] ?] ?]. reflexivity. Qed.

Definition EightByte (q:QuadByte * QuadByte) (v:val) : mpred :=
  match q with (q1, q2) =>
    data_at Tsh (Tarray tuchar 8 noattr) ((QuadByte2ValList q1) ++ (QuadByte2ValList q2)) v
  end.

Definition SixteenByte2ByteList (B:SixteenByte) : list byte :=
  match B with (q0, q1, q2, q3) =>
   QuadByte2ByteList q0 ++ QuadByte2ByteList q1 ++ QuadByte2ByteList q2 ++ QuadByte2ByteList q3
  end.

Definition SixteenByte2ValList (B:SixteenByte) : list val :=
   map Vint (map Int.repr (map Byte.unsigned (SixteenByte2ByteList B))).

Lemma SixteenByte2ValList_char B: SixteenByte2ValList B =
  match B with (q0, q1, q2, q3) =>
   QuadByte2ValList q0 ++ QuadByte2ValList q1 ++ QuadByte2ValList q2 ++ QuadByte2ValList q3
  end.
Proof. unfold SixteenByte2ValList, QuadByte2ValList .
 destruct B as [[[? ?] ?] ?]. simpl. repeat rewrite map_app. trivial.
Qed.

Definition ThirtyTwoByte (q:SixteenByte * SixteenByte) (v:val) : mpred :=
  match q with (q1, q2) =>
    @data_at CompSpecs Tsh (Tarray tuchar 32 noattr) ((SixteenByte2ValList q1) ++ (SixteenByte2ValList q2)) v
  end.

Definition QByte (q:QuadByte) (v:val) : mpred :=
  data_at Tsh (Tarray tuchar 4 noattr) (QuadByte2ValList q) v.

Definition QuadChunks2ValList (l: list QuadByte) : list val :=
  List.fold_right (fun q vals => QuadByte2ValList q ++ vals) nil l.

Definition flatten16 (B:SixteenByte) : list QuadByte :=
  match B with (q0, q1, q2, q3) => [q0; q1; q2; q3] end.
Lemma SixteenByte2ValList_flatten B:
  QuadChunks2ValList (flatten16 B) = SixteenByte2ValList B.
  destruct B as (((q0, q1), q2), q3). simpl.
  rewrite SixteenByte2ValList_char, app_nil_r. trivial.
Qed.

Lemma QuadByteByteList_ZLength q: 4 = Zlength (QuadByte2ByteList q).
  destruct q as (((q0, q1), q2), q3). simpl. reflexivity. Qed.
Lemma QuadByteValList_ZLength q: 4 = Zlength (QuadByte2ValList q).
  destruct q as (((q0, q1), q2), q3). simpl. reflexivity. Qed.

Lemma SixteenByte2ValList_Zlength C: 16 = Zlength (SixteenByte2ValList C).
  destruct C as (((q0, q1), q2), q3). unfold SixteenByte2ValList.
  repeat rewrite Zlength_map.  simpl.
  repeat rewrite Zlength_app. repeat rewrite <- QuadByteByteList_ZLength.
  reflexivity. Qed.

Definition SByte (q:SixteenByte) (v:val) : mpred :=
  @data_at CompSpecs Tsh (Tarray tuchar 16 noattr) (SixteenByte2ValList q) v.

Lemma ThirtyTwoByte_split16 q v:
  field_compatible (Tarray tuchar 32 noattr) [] v ->
  ThirtyTwoByte q v =
  (SByte (fst q) v * SByte (snd q) (offset_val 16 v))%logic.
Proof. destruct q as [s1 s2]. simpl; intros. unfold SByte.
  rewrite split2_data_at_Tarray_tuchar with (n1:= Zlength (SixteenByte2ValList s1));
     try rewrite Zlength_app; repeat rewrite <- SixteenByte2ValList_Zlength; try omega.
  unfold offset_val. red in H. destruct v; intuition.
  rewrite field_address0_offset. simpl.
  rewrite sublist_app1; try rewrite <- SixteenByte2ValList_Zlength; try omega.
  rewrite sublist_app2; try rewrite <- SixteenByte2ValList_Zlength; try omega.
  rewrite sublist_same; try rewrite <- SixteenByte2ValList_Zlength; trivial.
  rewrite sublist_same; try rewrite <- SixteenByte2ValList_Zlength; trivial.
  red; intuition.
Qed.

Lemma QuadByte2ValList_firstn4 q l:
         firstn 4 (QuadByte2ValList q ++ l) = QuadByte2ValList q.
   Proof. destruct q as (((b0, b1), b2), b3); trivial. Qed.

Lemma QuadByte2ValList_skipn4 q l:
         skipn 4 (QuadByte2ValList q ++ l) = l.
   Proof. destruct q as (((b0, b1), b2), b3); trivial. Qed.

Definition Select16Q (Q:SixteenByte) i :QuadByte :=
  match Q with (((b0, b1), b2), b3) =>
    if zeq i 0 then b0 else
    if zeq i 1 then b1 else
    if zeq i 2 then b2 else b3
  end.
Definition UnSelect16Q (Q:SixteenByte) i : list QuadByte :=
  match Q with (((b0, b1), b2), b3) =>
    if zeq i 0 then [b1;b2;b3] else
    if zeq i 1 then [b0;b2;b3] else
    if zeq i 2 then [b0;b1;b3] else [b0;b1;b2]
  end.
Definition SplitSelect16Q (Q:SixteenByte) i : (list QuadByte * list QuadByte) :=
  match Q with (((b0, b1), b2), b3) =>
    if zeq i 0 then ([], [b1;b2;b3]) else
    if zeq i 1 then ([b0], [b2;b3]) else
    if zeq i 2 then ([b0;b1], [b3]) else ([b0;b1;b2], [])
  end.
Lemma Select_SplitSelect16Q Q i front back:
    (front, back) = SplitSelect16Q Q i ->
    SixteenByte2ValList Q =
    QuadChunks2ValList front ++ QuadChunks2ValList [Select16Q Q i] ++ QuadChunks2ValList back.
Proof.
  unfold Select16Q, SplitSelect16Q; intros.
  destruct Q as (((q0, q1), q2), q3). simpl.
  destruct (zeq i 0); simpl. inv H; simpl. repeat rewrite app_nil_r. apply SixteenByte2ValList_char.
  destruct (zeq i 1); simpl. inv H; simpl. repeat rewrite app_nil_r. apply SixteenByte2ValList_char.
  destruct (zeq i 2); simpl. inv H; simpl. repeat rewrite app_nil_r. repeat rewrite <- app_assoc. apply SixteenByte2ValList_char.
  destruct (zeq i 3); simpl; inv H; simpl. repeat rewrite app_nil_r. repeat rewrite <- app_assoc. apply SixteenByte2ValList_char.
  repeat rewrite app_nil_r. repeat rewrite <- app_assoc. apply SixteenByte2ValList_char.
Qed.

Lemma QuadChunk2ValList_ZLength: forall l, Zlength (QuadChunks2ValList l) = (4 * Zlength l)%Z.
Proof.
  unfold QuadChunks2ValList. induction l; simpl. reflexivity.
  rewrite Zlength_app, IHl, <- QuadByteValList_ZLength.
  rewrite Zlength_cons; omega.
Qed.

Lemma Select_SplitSelect16Q_Zlength Q i front back:
    (front, back) = SplitSelect16Q Q i -> 0<= i < 4 ->
    Zlength front = i /\ Zlength back = 3-i.
Proof.
  unfold SplitSelect16Q; intros.
  destruct Q as (((q0, q1), q2), q3).
  destruct (zeq i 0). inv H. split; reflexivity.
  destruct (zeq i 1). inv H. split; reflexivity.
  destruct (zeq i 2). inv H. split; reflexivity.
  destruct (zeq i 3). inv H. split; reflexivity. omega.
Qed.

Definition QBytes (l:list QuadByte) (v:val) : mpred :=
  data_at Tsh (Tarray tuchar (4*Zlength l) noattr) (QuadChunks2ValList l) v.

Lemma QBytes16 s: SByte s = QBytes (flatten16 s).
Proof.
  destruct s as (((q0, q1), q2), q3). simpl.
  unfold SByte, QBytes. extensionality v. simpl. rewrite app_nil_r.
  rewrite SixteenByte2ValList_char. trivial.
Qed.

Definition QuadWordRep (q:QuadWord):list val :=
  match q with (q0, q1, q2, q3) => map Vint [q0;q1;q2;q3] end.
Definition SixteenWordRep (w:SixteenWord):list val :=
  match w with (q0, q1, q2, q3) => QuadWordRep q0 ++ QuadWordRep q1 ++ QuadWordRep q2 ++ QuadWordRep q3 end.

Definition littleendian_of_SixteenByte (x:SixteenByte): QuadWord :=
  match x with (q0, q1, q2, q3) => (littleendian q0, littleendian q1, littleendian q2, littleendian q3) end.

     Lemma QuadWR_length q: length (QuadWordRep q) = 4%nat.
        destruct q as [[[? ?] ?] ?]. simpl. reflexivity. Qed.
     Lemma QuadWR_zlength q: Zlength (QuadWordRep q) = 4.
        rewrite Zlength_correct, QuadWR_length. trivial. Qed.
     Lemma SixteenWR_length s: length (SixteenWordRep s) = 16%nat.
        destruct s as [[[? ?] ?] ?]. simpl.
        repeat rewrite app_length. repeat rewrite  QuadWR_length. reflexivity. Qed.
     Lemma SixteenWR_zlength s: Zlength (SixteenWordRep s) = 16.
        rewrite Zlength_correct, SixteenWR_length. trivial. Qed.

Lemma QuadWR_int q i: (0<=i<4)%nat -> exists ii, nth i (QuadWordRep q) Vundef = Vint ii.
  intros. destruct q as [[[? ?] ?] ?]. simpl.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity. omega. Qed.

Lemma SixteenWR_int s i: (0<=i<16)%nat -> exists ii, nth i (SixteenWordRep s) Vundef = Vint ii.
  intros. destruct s as [[[? ?] ?] ?]. simpl.
  destruct q as [[[? ?] ?] ?]. destruct q0 as [[[? ?] ?] ?].
  destruct q1 as [[[? ?] ?] ?]. destruct q2 as [[[? ?] ?] ?]. simpl.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity.
  destruct i. eexists; reflexivity. omega.
Qed.

Lemma SixteenWR_Znth_int i s: (0 <= i < 16) ->
       exists ii : int, Znth i (SixteenWordRep s) Vundef = Vint ii.
Proof. intros. unfold Znth. if_tac; try omega.
   apply SixteenWR_int. destruct H. apply Z2Nat.inj_lt in H1; simpl in *; omega.
Qed.

Lemma QuadWR_Z_int: forall (q : QuadWord) (i : Z),
               0 <= i < 4 -> exists ii : int, Znth i (QuadWordRep q) Vundef = Vint ii.
Proof. intros. unfold Znth. if_tac. omega.
       apply QuadWR_int. destruct H.
       split.
         apply Z2Nat.inj_le in H. apply H. omega. omega.
         apply Z2Nat.inj_lt in H1. apply H1. omega. omega.
Qed.

Lemma SixteenWordRep_MapVint ss: exists l, SixteenWordRep ss = map Vint l.
Proof.
destruct ss as [[[s0 s1] s2] s3].
destruct s0 as [[[x0 x1] x2] x3].
destruct s1 as [[[x4 x5] x6] x7].
destruct s2 as [[[x8 x9] x10] x11].
destruct s3 as [[[x12 x13] x14] x15]. simpl.
exists [x0; x1; x2; x3; x4; x5; x6; x7;
    x8; x9; x10; x11; x12; x13; x14; x15].
reflexivity.
Qed.

Definition QuadWordRepI (q : QuadWord) :=
  match q with (q0, q1, q2, q3) => [q0; q1; q2; q3] end.
Lemma QuadWordRepI_QuadWordRep q: QuadWordRep q = map Vint  (QuadWordRepI q).
Proof. destruct q as [[[q0 q1] q2] q3]. reflexivity. Qed.

Definition SixteenWordRepI (w : SixteenWord) :=
  match w with (q0, q1, q2, q3) =>
    QuadWordRepI q0 ++ QuadWordRepI q1 ++ QuadWordRepI q2 ++ QuadWordRepI q3
  end.
Lemma SixteenWordRepI_SixteenWordRep w: SixteenWordRep w = map Vint (SixteenWordRepI w).
Proof. destruct w as [[[q0 q1] q2] q3]. simpl.
   repeat rewrite QuadWordRepI_QuadWordRep. repeat rewrite map_app. reflexivity.
Qed.

    Lemma QuadWordRepI_length s: length (QuadWordRepI s) = 4%nat.
    Proof. destruct s as [[[q0 q1] q2] q3]. reflexivity. Qed.
    Lemma SixteenWordRepI_length s: length (SixteenWordRepI s) = 16%nat.
    Proof. destruct s as [[[q0 q1] q2] q3]. simpl.
      repeat rewrite app_length. repeat rewrite QuadWordRepI_length. reflexivity.
    Qed.

Lemma QuadByte2ValList_bytes q: exists bytes, length bytes = 4%nat /\
      QuadByte2ValList q = map Vint (map Int.repr (map Byte.unsigned bytes)).
Proof. destruct q as [[[b0 b1] b2] b3]. unfold QuadByte2ValList; simpl.
  exists [b0;b1;b2;b3]. split; trivial.
Qed.

Lemma SixteenByte2ValList_bytes N: exists bytes, length bytes = 16%nat /\
      SixteenByte2ValList N =  map Vint (map Int.repr (map Byte.unsigned bytes)).
Proof. destruct N as [[[q0 q1] q2] q3]. rewrite SixteenByte2ValList_char.
  destruct (QuadByte2ValList_bytes q0) as [bytes0 [L0 Q0]]. rewrite Q0.
  destruct (QuadByte2ValList_bytes q1) as [bytes1 [L1 Q1]]; rewrite Q1.
  destruct (QuadByte2ValList_bytes q2) as [bytes2 [L2 Q2]]; rewrite Q2.
  destruct (QuadByte2ValList_bytes q3) as [bytes3 [L3 Q3]]; rewrite Q3.
  exists (bytes0 ++ bytes1 ++ bytes2 ++ bytes3).
  repeat rewrite map_app. repeat rewrite app_length. rewrite L0, L1, L2, L3.
  split; trivial.
Qed.

Lemma QuadByte2ValList_ints q: exists ints, length ints = 4%nat /\
      QuadByte2ValList q = map Vint ints.
Proof. destruct q as [[[b0 b1] b2] b3]. unfold QuadByte2ValList; simpl.
  exists [Int.repr (Byte.unsigned b0); Int.repr (Byte.unsigned b1);
          Int.repr (Byte.unsigned b2); Int.repr (Byte.unsigned b3)].
  split; trivial.
Qed.

Lemma SixteenByte2ValList_ints N: exists ints, length ints = 16%nat /\
      SixteenByte2ValList N = map Vint ints.
Proof. destruct N as [[[q0 q1] q2] q3]. rewrite SixteenByte2ValList_char.
  destruct (QuadByte2ValList_ints q0) as [ints0 [L0 Q0]]; rewrite Q0.
  destruct (QuadByte2ValList_ints q1) as [ints1 [L1 Q1]]; rewrite Q1.
  destruct (QuadByte2ValList_ints q2) as [ints2 [L2 Q2]]; rewrite Q2.
  destruct (QuadByte2ValList_ints q3) as [ints3 [L3 Q3]]; rewrite Q3.
  exists (ints0 ++ ints1 ++ ints2 ++ ints3).
  repeat rewrite map_app. repeat rewrite app_length. rewrite L0, L1, L2, L3.
  split; trivial.
Qed.

Lemma QuadChunks2ValList_bytes: forall l,
        exists bytes, length bytes = (4*length l)%nat /\
        QuadChunks2ValList l = map Vint (map Int.repr (map Byte.unsigned bytes)).
  Proof. unfold QuadChunks2ValList.
    induction l; simpl; intros. exists nil; split; trivial.
    destruct IHl as [? [X1 X2]]; rewrite X2; clear X2.
    destruct (QuadByte2ValList_bytes a) as [? [Y1 Y2]]; rewrite Y2; clear Y2.
    repeat rewrite <- map_app. exists (x0 ++ x); split; trivial.
    rewrite app_length, X1, Y1. omega.
  Qed.

Fixpoint upd_upto (x: SixteenByte * SixteenByte * (SixteenByte * SixteenByte)) i (l:list val):list val :=
  match i with
    O => l
  | S n =>
     match x with (Nonce, C, (Key1, Key2)) =>
     ((upd_Znth (11 + (Z.of_nat n))
     (upd_Znth(6 + (Z.of_nat n))
        (upd_Znth (1 + (Z.of_nat n))
           (upd_Znth (5 * (Z.of_nat n)) (upd_upto x n l)
              (Vint (littleendian (Select16Q C (Z.of_nat n)))))
           (Vint (littleendian (Select16Q Key1 (Z.of_nat n)))))
        (Vint (littleendian (Select16Q Nonce (Z.of_nat n)))))
     (Vint (littleendian (Select16Q Key2 (Z.of_nat n))))))
     end
  end.

Lemma upd_upto_Sn Nonce C Key1 Key2 n l: upd_upto (Nonce, C, (Key1, Key2)) (S n) l =
     ((upd_Znth (11 + (Z.of_nat n))
     (upd_Znth (6 + (Z.of_nat n))
        (upd_Znth (1 + (Z.of_nat n))
           (upd_Znth (5 * (Z.of_nat n)) (upd_upto (Nonce, C, (Key1, Key2))  n l)
              (Vint (littleendian (Select16Q C (Z.of_nat n)))))
           (Vint (littleendian (Select16Q Key1 (Z.of_nat n)))))
        (Vint (littleendian (Select16Q Nonce (Z.of_nat n)))))
     (Vint (littleendian (Select16Q Key2 (Z.of_nat n)))))).
 reflexivity. Qed.

Lemma upd_upto_Zlength data l (H: Zlength l = 16): forall i (I:(0<=i<=4)%nat),
      Zlength (upd_upto data i l) = 16.
  Proof. apply Zlength_length in H. 2: omega. simpl in H.
    destruct l; simpl in H. exfalso; omega.
    destruct l; simpl in H. intros; omega. destruct l; simpl in H. intros; omega.
    destruct l; simpl in H. intros; omega. destruct l; simpl in H. intros; omega.
    destruct l; simpl in H. intros; omega. destruct l; simpl in H. intros; omega.
    destruct l; simpl in H. intros; omega. destruct l; simpl in H. intros; omega.
    destruct l; simpl in H. intros; omega. destruct l; simpl in H. intros; omega.
    destruct l; simpl in H. intros; omega. destruct l; simpl in H. intros; omega.
    destruct l; simpl in H. intros; omega. destruct l; simpl in H. intros; omega.
    destruct l; simpl in H. intros; omega. destruct l; simpl in H. 2: intros; omega. clear H.
    intros.
    induction i; destruct data as [[N C] [K1 K2]]. reflexivity.
    rewrite upd_upto_Sn. remember (11 + Z.of_nat i) as z1. remember (6 + Z.of_nat i) as z2.
    remember (1 + Z.of_nat i) as z3. remember (5 * Z.of_nat i)%Z as z4.
    remember (Vint (littleendian (Select16Q C (Z.of_nat i)))) as u4.
    remember (Vint (littleendian (Select16Q K1 (Z.of_nat i)))) as u3.
    remember (Vint (littleendian (Select16Q N (Z.of_nat i)))) as u2.
    remember (Vint (littleendian (Select16Q K2 (Z.of_nat i)))) as u1.
    assert ((0 <= i <= 4)%nat).
      split. omega. omega. (*rewrite Nat2Z.inj_succ in I. omega.*)
    repeat rewrite upd_Znth_Zlength; rewrite (IHi H); intros; try omega.
Qed.

Lemma upd_upto_Vint data: forall n, 0<=n<16 ->
      forall d, exists i, Znth n (upd_upto data 4 (list_repeat 16 Vundef)) d = Vint i.
  Proof. unfold upd_upto; intros. destruct data as [[N C] [K1 K2]].
   repeat rewrite (upd_Znth_lookup' 16); trivial; simpl; try omega.
   if_tac. eexists; reflexivity.   if_tac. eexists; reflexivity.
   if_tac. eexists; reflexivity.
   if_tac. eexists; reflexivity.
   if_tac. eexists; reflexivity.
   if_tac. eexists; reflexivity.
   if_tac. eexists; reflexivity.
   if_tac. eexists; reflexivity.
   if_tac. eexists; reflexivity.
   if_tac. eexists; reflexivity.
   if_tac. eexists; reflexivity.
   if_tac. eexists; reflexivity.
   if_tac. eexists; reflexivity.
   if_tac. eexists; reflexivity.
   if_tac. eexists; reflexivity.
   if_tac. eexists; reflexivity. omega.
Qed.

(*cf xsalsa-paper, beginning of Section 2*)
Lemma upd_upto_char data l: Zlength l = 16 ->
      upd_upto data 4 l = match data with ((Nonce, C), (Key1, Key2)) =>
          match Nonce with (N1, N2, N3, N4) =>
          match C with (C1, C2, C3, C4) =>
          match Key1 with (K1, K2, K3, K4) =>
          match Key2 with (L1, L2, L3, L4) =>
      map Vint (map littleendian [C1; K1; K2; K3;
                                  K4; C2; N1; N2;
                                  N3; N4; C3; L1;
                                  L2; L3; L4; C4]) end end end end end.
Proof. intros. apply Zlength_length in H. 2: omega.
   destruct data as [[Nonce C] [Key1 Key2]].
   destruct Nonce as [[[N1 N2] N3] N4].
   destruct C as [[[C1 C2] C3] C4].
   destruct Key1 as [[[K1 K2] K3] K4].
   destruct Key2 as [[[L1 L2] L3] L4].
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. omega.
   destruct l; simpl in H. 2: omega. clear H. reflexivity.
Qed.


text:
Require Import
  Coq.setoid_ring.Ring Coq.setoid_ring.Field MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders
  MathClasses.interfaces.naturals MathClasses.interfaces.rationals MathClasses.interfaces.integers
  MathClasses.implementations.natpair_integers MathClasses.theory.rationals MathClasses.theory.dec_fields MathClasses.theory.rings
  MathClasses.orders.integers MathClasses.orders.dec_fields.

Section rationals_and_integers.
  Context `{Rationals Q} `{!SemiRingOrder Qle}
    Z `{Integers Z} `{Apart Z} `{!TrivialApart Z} `{!FullPseudoSemiRingOrder (A:=Z) Zle Zlt}
    {f : Z → Q} `{!SemiRing_Morphism f}.
  Add Field Q : (stdlib_field_theory Q).

  Lemma rationals_decompose_pos_den x :
    ∃ num, ∃ den, 0 < den ∧ x = f num / f den.
  Proof.
    destruct (rationals_decompose x) as [num [den [E1 E2]]].
    destruct (total (≤) den 0).
     exists (-num), (-den). split.
      apply lt_iff_le_ne. split.
       now apply rings.flip_nonpos_negate.
      apply not_symmetry. now apply flip_negate_ne_0.
     rewrite 2!preserves_negate. rewrite E2. field.
     split.
      apply flip_negate_ne_0. now apply injective_ne_0.
     now apply injective_ne_0.
    exists num. exists den. split; try assumption.
    apply lt_iff_le_ne. split. assumption. now apply not_symmetry.
  Qed.
End rationals_and_integers.

(* A PseudoRingOrder uniquely specifies the orders on the rationals *)
Section rationals_and_another_rationals.
  Context `{Rationals Q1} `{Apart Q1} `{!TrivialApart Q1} `{!FullPseudoSemiRingOrder (A:=Q1) Q1le Q1lt}.
  Context `{Rationals Q2} `{Apart Q2} `{!TrivialApart Q2} `{!FullPseudoSemiRingOrder (A:=Q2) Q2le Q2lt}
     {f : Q1 → Q2} `{!SemiRing_Morphism f}.

  Add Field Q1 : (stdlib_field_theory Q1).

  Notation i_to_r := (integers.integers_to_ring (SRpair nat) Q1).

  Let f_preserves_nonneg x : 0 ≤ x → 0 ≤ f x.
  Proof.
    intros E.
    destruct (rationals_decompose_pos_den (SRpair nat) x) as [num [den [E1 E2]]].
    rewrite E2 in E |- *. clear E2.
    rewrite preserves_mult, preserves_dec_recip.
    apply (order_reflecting_pos (.*.) (f (i_to_r den))).
     change (0 < (f ∘ i_to_r) den).
     rewrite (integers.to_ring_unique _).
     apply semirings.preserves_pos. unfold lt in *. apply E1.
    apply (order_preserving_nonneg (.*.) (i_to_r den)) in E.
     rewrite right_absorb. rewrite right_absorb in E.
     rewrite (commutativity (f (i_to_r num))), associativity, dec_recip_inverse, left_identity.
      rewrite (commutativity (i_to_r num)), associativity, dec_recip_inverse, left_identity in E.
       change (0 ≤ (f ∘ i_to_r) num).
       rewrite (integers.to_ring_unique _).
       rewrite <-(preserves_0 (f:=integers_to_ring (SRpair nat) Q2)).
       apply (order_preserving _).
       apply (order_reflecting i_to_r).
       now rewrite preserves_0.
      apply injective_ne_0. now apply lt_ne_flip.
     change ((f ∘ i_to_r) den ≠ 0).
     apply injective_ne_0. now apply lt_ne_flip.
    apply semirings.preserves_nonneg.
    now apply lt_le.
  Qed.

  Instance morphism_order_preserving: OrderPreserving f.
  Proof. apply semirings.preserving_preserves_nonneg. apply f_preserves_nonneg. Qed.
End rationals_and_another_rationals.

Section rationals_order_isomorphic.
  Context `{Rationals Q1} `{Apart Q1} `{!TrivialApart Q1} `{!FullPseudoSemiRingOrder (A:=Q1) Q1le Q1lt}
    `{Rationals Q2} `{Apart Q2} `{!TrivialApart Q2} `{!FullPseudoSemiRingOrder (A:=Q2) Q2le Q2lt}
     {f : Q1 → Q2} `{!SemiRing_Morphism f}.

  Global Instance: OrderEmbedding f.
  Proof.
    split.
     apply morphism_order_preserving.
    repeat (split; try apply _).
    intros x y E.
    rewrite <-(to_rationals_involutive x (Q2:=Q2)), <-(to_rationals_involutive y (Q2:=Q2)).
    rewrite <-2!(to_rationals_unique f).
    now apply (morphism_order_preserving (f:=rationals_to_rationals Q2 Q1)).
  Qed.
End rationals_order_isomorphic.

#[global]
Instance rationals_le `{Rationals Q} : Le Q | 10 := λ x y,
  ∃ num, ∃ den, y = x + naturals_to_semiring nat Q num / naturals_to_semiring nat Q den.
#[global]
Instance rationals_lt  `{Rationals Q} : Lt Q | 10 := dec_lt.

Section default_order.
  Context `{Rationals Q} `{Apart Q} `{!TrivialApart Q}.

  Add Field F: (stdlib_field_theory Q).
  Notation n_to_sr := (naturals_to_semiring nat Q).

  Instance: Proper ((=) ==> (=) ==> iff) rationals_le.
  Proof.
    intros x x' E y y' E'. unfold rationals_le.
    split; intros [n [d d_nonzero]]; exists n, d.
     now rewrite <-E, <-E'.
    now rewrite E, E'.
  Qed.

  Instance: Reflexive rationals_le.
  Proof. intro. exists (0:nat), (0:nat). rewrite preserves_0. ring. Qed.

  (* rationals_le can actually only happen if the denominator is nonzero: *)
  Lemma rationals_decompose_le (x y: Q) :
    x ≤ y → ∃ num, ∃ den, den ≠ 0 ∧ y = x + n_to_sr num * / n_to_sr den.
  Proof with eauto.
    intros [n [d E]].
    destruct (decide (d = 0)) as [A|A]...
    exists (0:nat), (1:nat).
    split. discriminate.
    rewrite E, A, preserves_0, preserves_1, dec_recip_0.
    ring.
  Qed.

  Instance: Transitive rationals_le.
  Proof with auto.
    intros x y z E1 E2.
    destruct (rationals_decompose_le x y) as [n1 [d1 [A1 B1]]]...
    destruct (rationals_decompose_le y z) as [n2 [d2 [A2 B2]]]...
    exists (n1 * d2 + n2 * d1), (d1 * d2).
    rewrite B2, B1.
    rewrite preserves_plus.
    rewrite ?preserves_mult.
    field. split; now apply injective_ne_0.
  Qed.

  Instance: AntiSymmetric rationals_le.
  Proof with auto.
    intros x y E1 E2.
    destruct (rationals_decompose_le x y) as [n1 [d1 [A1 B1]]]...
    destruct (rationals_decompose_le y x) as [n2 [d2 [A2 B2]]]...
    rewrite B1 in B2 |- *.
    clear E1 E2 B1 y.
    rewrite <-associativity in B2. rewrite <-(plus_0_r x) in B2 at 1.
    apply (left_cancellation (+) x) in B2.
    destruct (zero_product n1 d2) as [F|F]...
      apply naturals.zero_sum with (d1 * n2).
      apply (injective n_to_sr).
      rewrite preserves_plus, preserves_mult, preserves_mult, preserves_0.
      apply (left_cancellation_ne_0 (.*.) (/n_to_sr d1)).
       apply dec_recip_ne_0. apply injective_ne_0...
      apply (left_cancellation_ne_0 (.*.) (/n_to_sr d2)).
       apply dec_recip_ne_0. apply injective_ne_0...
      ring_simplify.
      etransitivity.
       2: now symmetry; eauto.
      field.
      split; apply injective_ne_0...
     rewrite F. rewrite preserves_0. ring.
    contradiction.
  Qed.

  Instance: PartialOrder rationals_le.
  Proof. repeat (split; try apply _). Qed.

  Instance: SemiRingOrder rationals_le.
  Proof.
    apply from_ring_order.
     repeat (split; try apply _).
     intros x y [n [d E]]. exists n, d. rewrite E. ring.
    intros x y [n1 [d1 E1]] [n2 [d2 E2]].
    exists (n1 * n2), (d1 * d2).
    rewrite 2!preserves_mult.
    rewrite E1, E2, dec_recip_distr. ring.
  Qed.

  Notation i_to_r := (integers_to_ring (SRpair nat) Q).
  Instance: TotalRelation rationals_le.
  Proof with auto.
    assert (∀ xn xd yn yd, 0 < xd → 0 < yd → xn * yd ≤ yn * xd → i_to_r xn / i_to_r xd ≤ i_to_r yn / i_to_r yd) as P.
     intros xn xd yn yd.
     rewrite !lt_iff_le_apart.
     intros [xd_ge0 xd_ne0] [yd_ge0 yd_ne0] E.
     destruct (semirings.decompose_le E) as [z [Ez1 Ex2]].
     apply nat_int_le_plus in xd_ge0. apply nat_int_le_plus in yd_ge0. apply nat_int_le_plus in Ez1.
     destruct xd_ge0 as [xd' xd_ge0], yd_ge0 as [yd' yd_ge0], Ez1 as [z' Ez1].
     rewrite left_identity in xd_ge0, yd_ge0, Ez1.
     exists z'. exists (xd' * yd').
     assert (∀ a, (i_to_r ∘ naturals_to_semiring nat (SRpair nat)) a = n_to_sr a) as F.
      intros a. apply (naturals.to_semiring_unique _).
     rewrite preserves_mult, <-F, <-F, <-F.
     unfold compose. rewrite <-xd_ge0, <-yd_ge0, <-Ez1.
     transitivity ((i_to_r yn * i_to_r xd) / (i_to_r yd * i_to_r xd)).
      field. split; apply injective_ne_0; apply not_symmetry...
     rewrite <-preserves_mult, Ex2, preserves_plus, preserves_mult.
     field. split; apply injective_ne_0; apply not_symmetry...
    intros x y.
    destruct (rationals_decompose_pos_den (SRpair nat) x) as [xn [xd [E1x E2x]]].
    destruct (rationals_decompose_pos_den (SRpair nat) y) as [yn [yd [E1y E2y]]].
    rewrite E2x, E2y.
    destruct (total (≤) (xn * yd) (yn * xd)); [left | right]; now apply P.
  Qed.

  Global Instance: FullPseudoSemiRingOrder rationals_le rationals_lt.
  Proof. now apply dec_full_pseudo_srorder. Qed.
End default_order.

author: coq-community

repo: math-classes


text:
(* Cyclone Semantics using TLC/LN in Coq Version 4 *)
(* "SAFE PROGRAMMING AT THE C LEVEL OF ABSTRACTION".   Daniel Grossman, August 2003 *)
(* Lemmas from the Lambda JAR paper, comments/theorems from Arthur Chargeuraud. *)
(* Brian Milnes 2016 *)

Set Implicit Arguments.
Require Export Cyclone_LN_Types Cyclone_LN_Tactics.
Open Scope cyclone_scope.
Open Scope nat_scope.
Import T.

(* This is the version just for the lemmas about types. *)

(* ====================================================================== *)
(** ** Proofs *)

(* ********************************************************************** *)
(** Variable closing and variable opening are reciprocal of one another *)

(** Showing that [close_var] after [open_var] is the identity is easy *)

Module TP. (* T = Type P = Proof. *)

Lemma close_open : forall alpha t,
  alpha \notin fv t ->
  close alpha (open (ftvar alpha) t ) = t.
Proof.
  introv. unfold close, open. generalize 0.
  induction t; simpl; introv Fr; fequals~.
  case_nat~. simpl.
  case_var~.
  case_var~.
Qed.

(** The other direction is much harder; First, we first need
    to establish the injectivity of [open_var] *)

Lemma open_var_inj :
  forall alpha t1 t2,
    alpha \notin (fv t1) ->
    alpha \notin (fv t2) ->
    open (ftvar alpha) t1 = open (ftvar alpha) t2 ->
    (t1 = t2).
Proof.
  introv Fr1 Fr2 Eq.
  rewrite~ <- (@close_open alpha t1).
  rewrite~ <- (@close_open alpha t2).
  fequals~.
Qed.

(** We also need one (tricky) auxiliary lemma to handle the binder case *)

Lemma open_close_var_on_open_var :
  forall alpha beta gamma t i j,
    i <> j ->
    beta <> alpha ->
    beta \notin (fv t) ->
    open_rec i (ftvar beta) (open_rec j (ftvar gamma) (close_rec j alpha t))
  = open_rec j (ftvar gamma) (close_rec j alpha (open_rec i (ftvar beta) t)).
Proof.
  induction t; try solve[simpl; intros; try solve [ fequals~ ]];
  intros;
  do 4 (simpl; try case_nat~; try case_nat~; try case_var~).
Qed.

(** Now we can prove that [open_var] after [close_var] is the identity *)

Lemma open_close_var : forall alpha t,
  lc t ->
  forall n, open_rec n (ftvar alpha) (close_rec n alpha t)  = t.
Proof.
  introv T.
  induction T; try solve[intros; simpl; introv; fequals~];
  try solve[intros; simpl; case_var~; simpl; case_nat~];
  intros;
  simpl;
  fequals~;
  match goal with
   |- ?t = _ => pick_fresh y from (fv t)
  end;
  apply~ (@open_var_inj y);
  lets M: open_close_var_on_open_var;
  unfold open in M;
  unfold open;
  rewrite~ M.
Qed.

(** As a bonus, we get the injectivity of [close_var] *)

Lemma close_var_inj : forall alpha t1 t2,
  lc t1 -> lc t2 ->
  forall n,
    close_rec n alpha t1 = close_rec n alpha t2 ->
    (t1 = t2).
Proof.
  introv T1 T2 Eq.
  rewrite~ <- (@open_close_var alpha t1 T1 n).
  rewrite~ <- (@open_close_var alpha t2 T2 n).
  fequals~.
Qed.

(* ********************************************************************** *)
(** Properties of [body] *)

(** An abstraction is locally closed iff it satifies the predicate [body] *)

Lemma lc_utype_iff_body : forall k t,
  lc (utype k t) <-> body t.
Proof.
  intros.
  unfold body, open.
  iff H;
  inversions* H.
Qed.

Lemma lc_etype_iff_body : forall p k t,
  lc (etype p k t) <-> body t.
Proof.
  intros.
  unfold body, open.
  iff H; inversions* H.
Qed.

(* ********************************************************************** *)
(** Interaction of [fv] with [open_var] and [close_var] *)

(** Opening with [u] adds [fv u] to the set of free variables *)

Lemma fv_open : forall t u n,
  fv (open_rec n u t) \c fv t \u fv u.
Proof.
  intros t u.
  induction t; intros; simpl; try case_nat; try fset.
Qed.

(** In particular, opening with variable [x] adds [x] to the set
    of free variables *)

Lemma open_var_fv : forall x t n,
  fv (open_rec n (ftvar x) t) \c (fv t \u \{x}).
Proof. intros. apply fv_open. Qed.

(** Closing w.r.t variable [x] removes [x] from the set of free variables *)

Lemma close_fv : forall x t n,
  fv (close_rec n x t) \c (fv t \- \{x}).
Proof.
  intros x t.
  induction t; intros l; simpl; try fset.
  case_var; simpl; fset.
Qed.

(* ********************************************************************** *)
(** Properties of substitution *)

(** Distributivity of [subst] on [open].
    Two (tricky) intermediate lemmas are required *)

Lemma open_rec_lc_ind :
  forall t j v i u,
    i <> j ->
    open_rec i u (open_rec j v t) = open_rec j v t ->
    open_rec i u t = t.
Proof.
  induction t; introv Nq Eq;
   simpls; inversions~ Eq; fequals*.
  case_nat~. case_nat~.
Qed.

Lemma open_rec_lc : forall u t k,
  lc t -> open_rec k u t = t.
Proof.
  introv T. gen k.
  induction T; intros; simpl; fequals~;
  pick_fresh alpha;
  apply~ (@open_rec_lc_ind t0 0 (ftvar alpha));
  apply~ H0.
Qed.

Lemma subst_open_rec :
  forall alpha u t v n,
    lc u ->
    subst u alpha (open_rec n v t) =
    open_rec n (subst u alpha v) (subst u alpha t).
Proof.
  intros. generalize n.
  induction t; intros; simpl; fequals~.
  case_nat~.
  case_var~.
  rewrite~ open_rec_lc.
Qed.

(** In particular, we can distribute [subst] on [open_var] *)

Lemma subst_open_var:
  forall alpha beta u t n,
    alpha <> beta ->
    lc u ->
    subst u alpha (open_rec n (ftvar beta) t) =
    open_rec n (ftvar beta) (subst u alpha t).
Proof.
  introv N U.
  rewrite~ subst_open_rec.
  fequals.
  simpl.
  case_if~.
Qed.

(** For the distributivity of [subst] on [close_var],
    one simple intermediate lemmas is required to
    say that closing on a fresh name is the identity *)

Lemma close_rec_fresh : forall k alpha t,
  alpha \notin fv t -> close_rec k alpha t = t.
Proof.
  introv. gen k. induction t; simpl; intros; fequals*.
  case_var~.
Qed.

(** Distributivity of [subst] on [close_var] *)

Lemma subst_close_rec:
  forall alpha beta u t n,
    alpha <> beta ->
    beta \notin fv u ->
    subst u alpha (close_rec n beta t) = close_rec n beta (subst u alpha t).
Proof.
  introv N F. generalize n.
  induction t; intros l; simpl; fequals~.
  case_var~; simpl.
  case_var~; simpl. case_var~.
  case_var~; simpl.
  rewrite~ close_rec_fresh.
  case_var~.
Qed.

(** Substitution for a fresh name is the identity *)

Lemma subst_fresh : forall alpha t u,
  alpha \notin fv t -> subst u alpha t = t.
Proof.
  intros.
  induction t; simpls; fequals~. case_var~.
Qed.

(** Substitution can be introduced to decompose an opening *)

Lemma subst_intro :
  forall alpha t u,
    alpha \notin (fv t) ->
    lc u ->
    open_rec 0 u t = subst u alpha (open_rec 0 (ftvar alpha) t).
Proof.
  introv F U.
  rewrite~ subst_open_rec.
  fequals.
  simpl.
  case_var~.
  rewrite~ subst_fresh.
Qed.

(** An alternative, longer proof, but with fewer hypotheses *)

Lemma subst_intro_alternative : forall alpha t u n,
  alpha \notin (fv t) ->
  open_rec n u t = subst u alpha (open_rec n (ftvar alpha) t).
Proof.
  introv H. generalize n. gen H.
  induction t; simpl; intros; fequals*.
  case_nat*.
  simpl. case_var*.
  case_var*.
Qed.

(** Substitution can be introduced to decompose a variable
    closing in terms of another one using a different name *)

Lemma close_rename : forall alpha beta t n,
  alpha \notin fv t ->
  close_rec n beta t =
  close_rec n alpha (subst (ftvar alpha) beta t).
Proof.
  introv.  generalize n.
  induction t; simpl; intros l F; fequals~.
  case_var~; case_var~; simpl; case_var~.
Qed.

(* ********************************************************************** *)
(** Preservation of local closure through substitution and opening *)

(** Substitution of a locally closed terms into another one produces
    a locally closed term *)

Lemma subst_lc : forall alpha u t,
  lc u -> lc t -> lc (subst u alpha t).
Proof.
  introv U T. induction T; simple~;
  try case_var~;
  try apply_fresh lc_utype;
  try apply_fresh lc_etype;
  rewrite~ <- subst_open_var.
Qed.

(* ====================================================================== *)
(** ** An induction principle for locally closed terms *)

(** Interaction of [size] with [open_var] *)

Lemma size_open_var : forall alpha t n,
  size (open_rec n (ftvar alpha) t) = size t.
Proof.
  intros. generalize n.
  induction t; intros; simple~. case_nat~.
Qed.

(** Interaction of [size] with [close_var] *)

Lemma size_close_var : forall alpha t n,
  size (close_rec n alpha t) = size t.
Proof.
  intros. generalize n.
  induction t; intros; simple~. case_var~.
Qed.

(** The induction principle *)

(* Although Dan uses only induction on the size of \Gamma,
 I may find this useful in an LN style proof. *)

Lemma lc_induct_size :
  forall P : Tau -> Prop,
    (forall alpha,  P (ftvar alpha)) ->
    (P cint) ->
    (forall t1 t2, (lc t1) -> (P t1) -> (lc t2) -> (P t2) ->
                   P (cross t1 t2)) ->
    (forall t1 t2, (lc t1) -> (P t1) -> (lc t2) -> (P t2) ->
                   P (arrow t1 t2)) ->
    (forall t1, (lc t1) -> (P t1) -> P (ptype t1)) ->

    (forall k t1,
       body t1 ->
       (forall t2 alpha,
          alpha \notin fv t2 ->
          size t2 = size t1 ->
          lc (open_rec 0 (ftvar alpha) t2) ->
          P (open_rec 0 (ftvar alpha) t2)) ->
       P (utype k t1)) ->

    (forall p k t1,
       body t1 ->
       (forall t2 alpha,
          alpha \notin fv t2 ->
          size t2 = size t1 ->
          lc (open_rec 0 (ftvar alpha) t2) ->
          P (open_rec 0 (ftvar alpha) t2)) ->
       P (etype p k t1)) ->

    (forall t, lc t -> P t).
Proof.
  intros P Hvar Hcint Hcross Harrow Hptype Hutype Hetype t.
  induction t using (@measure_induction _ size).
  introv T.
  inverts T; simpl in H; auto.

  apply~ Hutype.
  try exists_fresh; auto.
  try introv Fr Eq T.
  apply~ H.
  try rewrite~ size_open_var.

  apply~ Hetype.
  try exists_fresh; auto.
  try introv Fr Eq T.
  apply~ H.
  try rewrite~ size_open_var.

Qed.

(* ====================================================================== *)
(** ** Alternative definition for local closure *)

(* ********************************************************************** *)
(** Equivalence of [lc] and [lc'] *)

Lemma lc_rec_open_var_rec : forall x t k,
  lc_at k (open_rec k (ftvar x) t) -> lc_at (S k) t.
Proof.
  induction t; simpl; introv H; autos*.
  case_nat; simpls~.
Qed.

Lemma lc_to_lc' : forall t,
  lc t -> lc' t.
Proof.
  introv T. induction T; unfold lc'; simple~;
  do 2 try solve [pick_fresh x; apply~ (@lc_rec_open_var_rec x); apply~ H0].
Qed.

Lemma lc_at_open_var_rec : forall x t k,
  lc_at (S k) t -> lc_at k (open_rec k (ftvar x) t).
Proof.
  induction t; simpl; introv H; autos*. case_nat; simple~.
Qed.

Lemma lc'_to_lc : forall t,
  lc' t -> lc t.
Proof.
  introv. unfold lc'.
  induction t using (@measure_induction _ size).
  destruct t; simpl; introv T'; simpl in H; autos*.
  apply_fresh lc_utype. apply H. rewrite~ size_open_var.
   apply~ lc_at_open_var_rec.
  apply_fresh lc_etype. apply H. rewrite~ size_open_var.
   apply~ lc_at_open_var_rec.
Qed.

Lemma lc_eq_lc' : lc = lc'.
Proof. extens. split. applys lc_to_lc'. applys lc'_to_lc. Qed.

(** Substitution of a locally closed terms into a body one produces
    another body *)

(* We need a lemma that Arthur only proved for his alternate inductive lc. *)

Lemma open_rec_lc'_ind : forall u t k,
  lc_at k t -> open_rec k u t = t.
Proof.
  introv. gen k. induction t; simpl; introv F; fequals*.
  case_nat~. false. nat_math.
Qed.

Lemma lc'_open_var_rec:
  forall alpha t,
    lc' t -> lc (open_rec 0 (ftvar alpha) t).
Proof.
  introv lct.
  assert(lc' t); auto.
  unfold lc' in *.
  apply open_rec_lc'_ind with (u:= ftvar alpha) in lct.
  rewrite lct.
  apply lc'_to_lc in H.
  assumption.
Qed.

Lemma lc_open_var_rec:
  forall alpha t,
    lc t -> lc (open_rec 0 (ftvar alpha) t).
Proof.
  intros.
  apply lc_to_lc' in H.
  applys~ lc'_open_var_rec.
Qed.

Lemma subst_body :
  forall alpha t u,
    lc u -> body t -> body (subst u alpha t).
Proof.
  introv U [L H].
  exists_fresh.
  unfold open.
  rewrite~ <- subst_open_var.
  apply~ subst_lc.
Qed.

(** Opening of a body with a locally closed terms produces a
    locally closed term *)

Lemma open_rec_preserves_lc : forall t u,
  body t -> lc u -> lc (open_rec 0 u t).
Proof.
  introv [L H] U.
  pick_fresh alpha.
  rewrite~ (@subst_intro alpha).
  apply~ subst_lc.
Qed.

End TP.

author: briangmilnes

repo: CycloneCoqSemantics


text:
Require Import Coqlib.
Require Export liblayers.compcertx.CompcertStructures.
Require Export compcertx.common.MemoryX. (* for storebytes_empty *)
Require Import LogicalRelations.
Require Import PTrees.
Require Import SimulationRelation.
Require Import Ctypes.
Require Import Clight.

Require Import Globalenvs.
Require Import Events.
Require Import OptionOrders.
Require Import SimEvents.
Require Import SimCompCertBuiltins.
Require Import SimCop.

Require Import Program.Basics.

Local Opaque mwd_ops.

(** Framing over a control stack *)

Function frame_cont (kframe: cont) (k: cont) :=
  match k with
    | Kstop => kframe
    | Kseq s k => Kseq s (frame_cont kframe k)
    | Kloop1 s1 s2 k => Kloop1 s1 s2 (frame_cont kframe k)
    | Kloop2 s1 s2 k => Kloop2 s1 s2 (frame_cont kframe k)
    | Kswitch k => Kswitch (frame_cont kframe k)
    | Kcall oi f e t k => Kcall oi f e t (frame_cont kframe k)
  end.

Lemma call_cont_is_call_cont_id:
  forall kframe, is_call_cont kframe ->
                 call_cont kframe = kframe.
Proof.
  induction kframe; eauto; inversion 1; subst; eauto.
Qed.

Lemma call_cont_frame:
  forall kframe, is_call_cont kframe ->
                 forall k, call_cont (frame_cont kframe k) = frame_cont kframe (call_cont k).
Proof.
  induction k; simpl; eauto using call_cont_is_call_cont_id.
Qed.

Lemma is_call_cont_frame:
  forall kframe, is_call_cont kframe ->
                 forall k, is_call_cont k ->
                           is_call_cont (frame_cont kframe k).
Proof.
  induction k; simpl; eauto.
Qed.

Section WITHKFRAME.
  Variables (kframe: cont).

Lemma find_label_frame:
  forall s l k,
    (forall s' k',
       find_label l s k = Some (s', k') ->
       find_label l s (frame_cont kframe k) = Some (s', frame_cont kframe k'))
    /\
    (find_label l s k = None ->
     find_label l s (frame_cont kframe k) = None)
with find_label_ls_frame:
  forall ls l k,
    (forall s' k',
       find_label_ls l ls k = Some (s', k') ->
       find_label_ls l ls (frame_cont kframe k) = Some (s', frame_cont kframe k'))
    /\ (
      find_label_ls l ls k = None ->
      find_label_ls l ls (frame_cont kframe k) = None
    ).
Proof with (try discriminate;
            try (
                try (apply find_label_frame in Heqo;
                     simpl in Heqo;
                     rewrite Heqo);
                try (apply find_label_ls_frame in Heqo;
                     simpl in Heqo;
                     rewrite Heqo);
                try reflexivity;
                try apply find_label_frame;
                try apply find_label_ls_frame
              )
           ).
  {
    destruct s; simpl; split; try discriminate; eauto...
    * destruct (find_label l s1 (Kseq s2 k)) eqn:Heqo...
      inversion 1; subst...
    * destruct (find_label l s1 (Kseq s2 k)) eqn:Heqo...
    * destruct (find_label l s1 k) eqn:Heqo...
      inversion 1; subst...
    * destruct (find_label l s1 k) eqn:Heqo...
    * destruct (find_label l s1 (Kloop1 s1 s2 k)) eqn:Heqo...
      inversion 1; subst...
    * destruct (find_label l s1 (Kloop1 s1 s2 k)) eqn:Heqo...
    * destruct (AST.ident_eq l0 l); try congruence...
    * destruct (AST.ident_eq l0 l); try congruence...
  }
  destruct ls; simpl; split; try discriminate; eauto.
  * destruct (find_label l s (Kseq (seq_of_labeled_statement ls) k)) eqn:Heqo...
    inversion 1; subst...
  * destruct (find_label l s (Kseq (seq_of_labeled_statement ls) k)) eqn:Heqo...
Qed.

End WITHKFRAME.

Section WITHCONFIGOPS.

Context {mem} `{ec_ops: ExternalCallsOps mem}.
Context `{eb_ops: !EnableBuiltins mem}.

Function state_cont (s: state) :=
  match s with
    | State _ _ k _ _ _ => k
    | Callstate _ _ k _ => k
    | Returnstate _ k _ => k
  end.

Function frame_state_cont  (kframe: cont) (s: state) :=
  match s with
    | State f s k e t m => State f s (frame_cont kframe k) e t m
    | Callstate fd args k m => Callstate fd args (frame_cont kframe k) m
    | Returnstate v k m => Returnstate v (frame_cont kframe k) m
  end.

Lemma frame_state_cont_frame_cont:
  forall kframe s,
    state_cont (frame_state_cont kframe s) = frame_cont kframe (state_cont s).
Proof.
  destruct s; reflexivity.
Qed.

Theorem step_frame_cont:
  forall kframe,
    is_call_cont kframe ->
  forall ge fe s t s',
    step ge fe s t s' ->
    step ge fe (frame_state_cont kframe s) t (frame_state_cont kframe s').
Proof.
  inversion 2; subst; simpl; try rewrite <- call_cont_frame; eauto; try (econstructor; eauto using is_call_cont_frame; fail).
  (* goto *)
  econstructor. rewrite call_cont_frame; eauto. eapply find_label_frame; eauto.
Qed.

Corollary star2_frame_cont:
  forall kframe,
    is_call_cont kframe ->
    forall ge s t s',
      Smallstep.star step2 ge s t s' ->
      Smallstep.star step2 ge (frame_state_cont kframe s) t (frame_state_cont kframe s').
Proof.
  induction 2; econstructor; eauto.
  eapply step_frame_cont; eauto.
Qed.

Corollary plus2_frame_cont:
  forall kframe,
    is_call_cont kframe ->
    forall ge s t s',
      Smallstep.plus step2 ge s t s' ->
      Smallstep.plus step2 ge (frame_state_cont kframe s) t (frame_state_cont kframe s').
Proof.
  inversion 2; subst; econstructor; eauto using star2_frame_cont.
  apply step_frame_cont; auto.
Qed.

End WITHCONFIGOPS.

Section CLIGHT_REL.
  Context `{Hmem: BaseMemoryModel}.
  Context {D1 D2} (R: simrel D1 D2).

  Inductive clight_genv_le Rf: rel genv genv :=
    | Build_genv_le:
        Monotonic
          (@Build_genv)
          (genv_le Rf ++> - ==> clight_genv_le Rf).

  Global Existing Instance Build_genv_le.

  Global Instance genv_genv_le Rf:
    Monotonic
      (@genv_genv)
      (clight_genv_le Rf ++> genv_le Rf).
  Proof.
    unfold genv_genv.
    rauto.
  Qed.

  Global Instance genv_cenv_le Rf:
    Monotonic
      (@genv_cenv)
      (clight_genv_le Rf ++> eq).
  Proof.
    unfold genv_cenv.
    rauto.
  Qed.

  (* May be needed:
  Global Instance clight_globalenv_le Rf:
    Monotonic
      (@globalenv)
      (program_le Rf ==> clight_genv_le Rf).
  *)

  (** NB: we have to use [option_rel] here not [option_le], because
    otherwise it is difficult to state the monotonicity property of
    [blocks_of_env] (we would have to introduce some kind of "subset"
    list relator) *)
  Definition env_match p: rel env env :=
    ptree_rel (option_rel (match_block_sameofs R p * @eq type))%rel.

  (** FIXME: need general theorem about ptree_rel *)
  Global Instance empty_env_match p:
    Monotonic (@empty_env) (env_match p).
  Proof.
    solve_monotonic.
    unfold env_match, empty_env.
    intros i.
    rewrite PTree.gempty.
    constructor.
  Qed.

  Global Instance env_match_le:
    Monotonic
      (@env_match)
      ((≤) ++> subrel).
  Proof.
    unfold env_match.
    solve_monotonic.
  Qed.

  Definition temp_env_match p: rel temp_env temp_env :=
    ptree_rel (option_le (match_val R p)).

  Global Instance temp_env_match_le:
    Monotonic
      temp_env_match
      ((≤) ++> subrel).
  Proof.
    unfold temp_env_match.
    solve_monotonic.
  Qed.

  Global Instance: Params (@temp_env_match) 3.

  Global Instance deref_loc_match p:
    Monotonic
      deref_loc
      (- ==> match_mem R p ++> % match_ptrbits R p ++> set_rel (match_val R p)).
  Proof.
    solve_monotonic.
    intros a H1.
    assert (match_val R p (Vptr (fst x1) (snd x1)) (Vptr (fst y0) (snd y0))) as VAL.
    {
      econstructor.
      destruct x1; destruct y0; assumption.
    }
    inversion H0; subst.
    repeat red.
    simpl in * |- * .
    inversion H1; subst; eauto using @deref_loc_reference, @deref_loc_copy.
    generalize (simrel_loadv _ chunk _ _ H _ _ VAL).
    rewrite H4.
    inversion 1; subst.
    symmetry in H7.
    eauto using @deref_loc_value.
  Qed.

  Global Instance: Params (@deref_loc) 5.

  Hint Extern 1 (Transport _ _ _ _ _) =>
    set_rel_transport @deref_loc : typeclass_instances.

  (** [assign_loc] is somewhat involved. *)

  Lemma assign_loc_match_alignof_blockcopy p m1 m2 b1 ofs1 b2 ofs2 env ty:
    match_mem R p m1 m2 ->
    match_ptrbits R p (b1, ofs1) (b2, ofs2) ->
    sizeof env ty > 0 ->
    Mem.range_perm m1 b1 (Ptrofs.unsigned ofs1) (Ptrofs.unsigned ofs1 + sizeof env ty) Cur Nonempty ->
    (alignof_blockcopy env ty | Ptrofs.unsigned ofs1) ->
    (alignof_blockcopy env ty | Ptrofs.unsigned ofs2).
  Proof.
    intros Hm Hptr Hsz Hperm H.
    inv Hptr.
    erewrite (simrel_address_inject p); eauto.
    eapply (simrel_aligned_area_inject p); eauto.
    + eapply alignof_blockcopy_1248.
    + eapply sizeof_alignof_blockcopy_compat.
    + eapply Hperm.
      omega.
  Qed.

  Global Instance assign_loc_match Rf p:
    @Monotonic
      (forall ge : genv, let ce := genv_cenv ge in _)
      assign_loc
      (clight_genv_le Rf ++>
       - ==> match_mem R p ++> % match_ptrbits R p ++> match_val R p ++>
       set_rel (incr p (match_mem R p))).
  Proof.
    intros ge1 ge2 Hge ty m1 m2 Hm [b1 ofs1] [b2 ofs2] Hptr v1 v2 Hv m1' Hm1'.
    destruct Hm1' as [b1 ofs1 v1 m1' | b1 ofs1 b1' ofs1' bytes1 m1'].
    - transport_hyps.
      eexists; split; [ | rauto].
      eapply assign_loc_value; eauto.
    - assert
        (sizeof ge1 ty > 0 ->
         Mem.range_perm m1 b1
           (Ptrofs.unsigned ofs1)
           (Ptrofs.unsigned ofs1 + sizeof ge1 ty)
           Cur Nonempty).
      {
        intro.
        eapply Mem.range_perm_implies.
        + replace (sizeof _ _) with (Z.of_nat (length bytes1)).
          * eapply Mem.storebytes_range_perm; eauto.
          * erewrite (Mem.loadbytes_length m1) by eauto.
            apply nat_of_Z_eq.
            omega.
        + constructor.
      }
      assert
        (sizeof ge1 ty > 0 ->
         Mem.range_perm m1 b1'
           (Ptrofs.unsigned ofs1')
           (Ptrofs.unsigned ofs1' + sizeof ge1 ty)
           Cur Nonempty).
      {
        intro.
        eapply Mem.range_perm_implies.
        + eapply Mem.loadbytes_range_perm; eauto.
        + constructor.
      }
      simpl.
      destruct Hge; simpl in *.
      inv Hv.
      change (Mem.loadbytesv m1 (Vptr b1' ofs1') (sizeof a ty) = Some bytes1) in H3.
      change (Mem.storebytesv m1 (Vptr b1 ofs1) bytes1 = Some m1') in H4.
      transport_hyps.
      eexists; split; [eapply assign_loc_copy | ]; simpl.
      + assumption.
      + eauto using assign_loc_match_alignof_blockcopy.
      + eauto using assign_loc_match_alignof_blockcopy.
      + destruct (decide (sizeof a ty = 0)) as [Hsz | Hsz].
        {
          rewrite Hsz.
          right.
          omega.
        }
        assert (Hsz' : sizeof a ty > 0).
        {
          pose proof (sizeof_pos a ty).
          omega.
        }
        inv Hptr.
        inv H11.
        erewrite !(simrel_address_inject p); eauto.
        eapply (simrel_disjoint_or_equal_inject p); eauto.
        * intros ofs Hofs.
          eapply Mem.perm_cur_max.
          eapply H6; eauto.
        * intros ofs Hofs.
          eapply Mem.perm_cur_max.
          eapply H5; eauto.
        * eapply H5; eauto.
          omega.
        * eapply H6; eauto.
          omega.
      + eassumption.
      + eassumption.
      + rauto.
  Qed.

  Global Instance: Params (@assign_loc) 7.

  Hint Extern 1 (Transport _ _ _ _ _) =>
    set_rel_transport @assign_loc : typeclass_instances.

  Global Instance alloc_variables_match Rf p:
    Monotonic
      alloc_variables
      (clight_genv_le Rf ++>
       env_match p ++>
       match_mem R p ++>
       - ==>
       % set_rel (incr p (env_match p * match_mem R p))).
  Proof.
    intros ge1 ge2 Hge e1 e2 Henv m1 m2 Hm vars [e1' m1'] H.
    revert H p e2 m2 Henv Hm.
    simpl.
    induction 1 as [e1 m1 | e1 m1 id ty vars m1' b1 m1'' e1'' Hm1' Hm1'' IH].
    - intros.
      exists (e2, m2).
      split.
      + constructor.
      + exists p.
        split; [ reflexivity | ].
        split; eauto.
    - intros.
      edestruct (simrel_alloc p m1 m2 Hm 0 (sizeof ge1 ty)) as (p' & Hp' & Hm' & Hb); eauto.
      destruct (Mem.alloc m2 0 (sizeof ge1 ty)) as [m2' b2] eqn:Hm2'.
      rewrite Hm1' in *; simpl in *.
      specialize (IH p' (PTree.set id (b2, ty) e2) m2').
      edestruct IH as ((e2'' & m2'') & Hvars & p'' & He'' & Hm''); eauto.
      {
        (** We only have [ptree_set_le], we would need support for
          multiple instances to declare [ptree_set_rel] as well. *)
        unfold env_match in *.
        intro j.
        destruct (Decision.decide (j = id)); subst.
        - rewrite !PTree.gss.
          constructor.
          split; eauto.
        - rewrite !PTree.gso by assumption.
          rauto.
      }
      eexists (e2'', m2'').
      split.
      + simpl.
        econstructor; eauto.
        destruct Hge; simpl in *.
        assumption.
      + exists p''.
        split.
        * etransitivity; eauto.
        * assumption.
  Qed.

  Global Instance: Params (@alloc_variables) 6.

  Global Instance bind_parameters_match Rf p:
    Monotonic
      bind_parameters
      (clight_genv_le Rf ++>
       env_match p ++>
       match_mem R p ++>
       - ==>
       list_rel (match_val R p) ++>
       set_rel (incr p (match_mem R p))).
  Proof.
    intros ge1 ge2 Hge e1 e2 He m1 m2 Hm vars vl1 vl2 Hvl m1' H.
    revert H p He vl2 m2 Hvl Hm.
    induction 1 as [m1 | m1 id ty params v1 vl1 b1 m1' m1'' Hb1 Hm1' Hm1'' IH].
    - intros.
      exists m2.
      split; eauto; try now solve_monotonic.
      inversion Hvl; subst.
      constructor.
    - intros.
      generalize He. intro He_.
      specialize (He id).
      pose proof (fun m: mwd D2 => bind_parameters_cons ge2 e2 m id) as Hbp_cons.
      destruct He as [[xb1 xty] [b2 yty] [Hb Hty] | ]; try discriminate.
      simpl in *.
      inversion Hb1; clear Hb1.
      repeat subst.
      inversion Hvl as [ | xv1 v2 Hv xvl1 vl2' Hvl']; subst.
      generalize (match_block_sameofs_ptrbits _ _ Ptrofs.zero _ _ Hb Logic.eq_refl). intro PTR.
      transport_hyps.
      subst.
      edestruct (IH p') as (m2'' & Hm2'' & Hm''); eauto.
      (* TODO: incr, transitivity *)
      + eapply env_match_le; eauto.
      + eapply list_subrel; eauto.
        solve_monotonic.
      + destruct Hm'' as (? & ? & ?).
        esplit.
        split; eauto.
        solve_monotonic.
  Qed.

  Global Instance: Params (@bind_parameters) 6.

  Hint Extern 1 (Transport _ _ _ _ _) =>
    set_rel_transport @bind_parameters : typeclass_instances.

  Global Instance create_undef_temps_match p:
    Monotonic
      (@create_undef_temps)
      (- ==> temp_env_match p).
  Proof.
    intros temps.
    induction temps as [ | [id t] temps IHtemps]; simpl; solve_monotonic.
  Qed.

  Global Instance bind_parameter_temps_match p:
    Monotonic
      (@bind_parameter_temps)
      (- ==>
       list_rel (match_val R p) ++>
       temp_env_match p ++>
       option_rel (temp_env_match p)).
  Proof.
    intros formals args1 args2 Hargs.
    revert formals.
    induction Hargs as [ | v1 v2 Hv args1 args2 Hargs IH].
    - intros [|]; simpl; intros; solve_monotonic.
    - intros [| [id t] formals]; simpl; solve_monotonic.
      eapply IH.
      solve_monotonic.
  Qed.

  Global Instance block_of_binding_match Rf p:
    Monotonic
      (@block_of_binding)
      (clight_genv_le Rf ++> eq * (match_block_sameofs R p * eq) ++>
       match_block_sameofs R p * eq * eq).
  Proof.
    intros ge1 ge2 Hge (id1 & b1 & ty1) (id2 & b2 & ty2) (Hid & Hb & Hty).
    simpl in *.
    solve_monotonic.
    destruct Hge; simpl; congruence.
  Qed.

  Section LOCALS.
    Local Instance blocks_of_env_match_strong Rf p:
      Monotonic
        (@blocks_of_env)
        (clight_genv_le Rf ++> env_match p ++>
         list_rel (match_block_sameofs R p * eq * eq)).
    Proof.
      unfold blocks_of_env.
      solve_monotonic.
    Qed.

    Local Instance match_blocks_sameofs_ptrrange p:
      Related
        (match_block_sameofs R p * eq * eq)%rel
        (match_ptrrange R p)
        subrel.
    Proof.
      repeat red.
      inversion 1; subst.
      inversion H0; subst.
      destruct x as [ [ ? ? ] ? ].
      destruct y as [ [ ? ? ] ? ].
      simpl in * |- * .
      subst.
      replace z2 with (z1 + (z2 - z1))%Z by omega.
      constructor.
      apply match_block_sameofs_ptr; auto.
    Qed.

    Global Instance blocks_of_env_match_weak Rf p:
      Monotonic
        (@blocks_of_env)
        (clight_genv_le Rf ++> env_match p ++> list_rel (match_ptrrange R p)).
    Proof.
      solve_monotonic.
    Qed.
  End LOCALS.

  Global Instance set_opttemp_match p:
    Monotonic
      (@set_opttemp)
      (- ==>
       match_val R p ++>
       temp_env_match p ++>
       temp_env_match p).
  Proof.
    unfold set_opttemp.
    solve_monotonic.
  Qed.

  (** [select_switch_default], [select_switch_case], [select_switch]
    and [seq_of_label_statement] are entierly about syntax. *)
  Lemma eval_expr_lvalue_match Rf p:
    forall ge1 ge2, clight_genv_le Rf ge1 ge2 ->
    forall e1 e2, env_match p e1 e2 ->
    forall le1 le2, temp_env_match p le1 le2 ->
    forall m1 m2, match_mem R p m1 m2 ->
    (forall expr v1,
       eval_expr ge1 e1 le1 m1 expr v1 ->
       exists v2,
         eval_expr ge2 e2 le2 m2 expr v2 /\
         match_val R p v1 v2) /\
    (forall expr b1 ofs,
       eval_lvalue ge1 e1 le1 m1 expr b1 ofs ->
       exists b2 ofs2,
         eval_lvalue ge2 e2 le2 m2 expr b2 ofs2 /\
         match_ptrbits R p (b1, ofs) (b2, ofs2)).
  Proof.
    intros ge1 ge2 Hge e1 e2 He le1 le2 Hle m1 m2 Hm.
    apply eval_expr_lvalue_ind.

    - eexists; repeat (solve_monotonic; constructor).
    - eexists; repeat (solve_monotonic; constructor).
    - eexists; repeat (solve_monotonic; constructor).
    - eexists; repeat (solve_monotonic; constructor).

    - intros.
      transport_hyps.
      eexists; split; eauto; repeat rstep.
      constructor; eauto.

    - intros expr ty loc ofs H IH.
      destruct IH as (b2 & ofs2 & Hb2 & Hptr).
      eexists; repeat (solve_monotonic; constructor).

    - intros op expr ty v1 v1' Hv1 IHv1 Hv1'.
      destruct IHv1 as (v2 & Hv2 & Hv).
      pose proof (sem_unary_operation_match R). (* necessary to transport Hv1' *)
      transport_hyps.
      eexists; repeat (solve_monotonic; econstructor).

    - intros op expra exprb ty va1 vb1 v1 Hva1 IHva Hvb1 IHvb Hv1.
      destruct IHva as (va2 & Hva2 & Hva).
      destruct IHvb as (vb2 & Hvb2 & Hvb).
      transport_hyps.
      eexists; repeat (solve_monotonic; econstructor).

    - intros expr ty v1 v1' Hv1 IHv1 Hv1'.
      destruct IHv1 as (v2 & Hv2 & Hv).
      pose proof (sem_cast_match R). (* necessary to transport Hv1' *)
      transport_hyps.
      eexists; repeat (solve_monotonic; econstructor).

    - eexists; repeat (solve_monotonic; constructor).
      destruct Hge; simpl.
      solve_monotonic.

    - eexists; repeat (solve_monotonic; constructor).
      destruct Hge; simpl.
      solve_monotonic.

    - intros expr b1 ofs1 v1 Hptr1 (b2 & ofs2 & Hptr & Hptr2) Hv1.
      transport_hyps.
      eexists; repeat (solve_monotonic; econstructor).

    - intros id b1 ty Hb1.
      specialize (He id).
      (** XXX: need transport to try both option_le and option_rel *)
      eapply option_rel_some_inv in Hb1; [ | solve_monotonic].
      destruct Hb1 as ((b2 & ty') & Hb2 & Hb & Hty).
      simpl in *; subst.
      eexists.
      repeat (solve_monotonic; econstructor).
      apply match_block_sameofs_ptrbits; auto.

    - intros id b1 ty He1 Hb1.
      transport_hyps.
      subst.
      eexists.
      eexists.
      split.
      + eapply eval_Evar_global; eauto.
      + apply match_block_sameofs_ptrbits; auto.
        apply match_global_block_sameofs.
        rewrite stencil_matches_symbols in H
          by (eapply genv_le_stencil_matches_r; rauto).
        eapply find_symbol_block_is_global.
        eassumption.

    - intros expr ty b1 ofs H1 IH.
      destruct IH as (ptr2 & H2 & Hptr).
      inversion Hptr; clear Hptr; subst.
      eexists.
      eexists.
      split; eauto.
      constructor; eauto.

    - intros expr fid ty b1 ofs1 sid sflist satt delta H1 IH Hs Hf Hdelta.
      destruct IH as (ptr2 & H2 & Hptr).
      inversion Hptr; clear Hptr; subst.
      destruct Hge; simpl in *.
      eauto 6 using @eval_Efield_struct, match_ptrbits_shift.

    - intros expr fid ty b1 ofs1 uid uflist uatt H1 IH Hu.
      destruct IH as (ptr2 & H2 & Hptr).
      inversion Hptr; clear Hptr; subst.
      destruct Hge; simpl in *.
      eauto using @eval_Efield_union.
  Qed.

  Global Instance eval_expr_match Rf p:
    Monotonic
      eval_expr
      (clight_genv_le Rf ++>
       env_match p ++>
       temp_env_match p ++>
       match_mem R p ++>
       - ==>
       set_rel (match_val R p)).
  Proof.
    intros ge1 ge2 Hge e1 e2 He le1 le2 Hle m1 m2 Hm expr v1 Hv1.
    edestruct eval_expr_lvalue_match; eauto.
  Qed.

  Global Instance: Params (@eval_expr) 6.

  Hint Extern 1 (Transport _ _ _ _ _) =>
    set_rel_transport @eval_expr : typeclass_instances.

  Global Instance eval_lvalue_match Rf p:
    Monotonic
      eval_lvalue
      (clight_genv_le Rf ++>
       env_match p ++>
       temp_env_match p ++>
       match_mem R p ++>
       - ==>
       % set_rel (match_ptrbits R p)).
  Proof.
    intros ge1 ge2 Hge e1 e2 He le1 le2 Hle m1 m2 Hm expr [b1 ofs] Hp1.
    simpl in *.
    edestruct eval_expr_lvalue_match as [_ H]; eauto.
    edestruct H as (b2 & ofs2 & H'); eauto.
    exists (b2, ofs2).
    split_hyps.
    split; eauto.
  Qed.

  Global Instance: Params (@eval_lvalue) 7.

  Hint Extern 1 (Transport _ _ _ _ _) =>
    rel_curry_set_rel_transport @eval_lvalue : typeclass_instances.

  Global Instance eval_exprlist_match Rf p:
    Monotonic
      eval_exprlist
      (clight_genv_le Rf ++>
       env_match p ++>
       temp_env_match p ++>
       match_mem R p ++>
       - ==> - ==>
       set_rel (list_rel (match_val R p))).
  Proof.
    intros ge1 ge2 Hge e1 e2 He le1 le2 Hle m1 m2 Hm exprlist tys vs1 Hvs1.
    induction Hvs1 as [|expr exprs ty tys v1 v1' v1s Hv1 Hv1' Hv1s IHv1s]; simpl.
    - exists nil.
      split; constructor.
    - split_hyps.
      pose proof (sem_cast_match R). (* necessary to transport Hv1' *)
      transport_hyps.
      eexists.
      split; econstructor; eauto.
  Qed.

  Global Instance: Params (@eval_exprlist) 7.

  Hint Extern 1 (Transport _ _ _ _ _) =>
    set_rel_transport @eval_exprlist : typeclass_instances.

  Inductive cont_match (p: simrel_world R): rel cont cont :=
    | Kstop_match:
        Monotonic (@Kstop) (cont_match p)
    | Kseq_match:
        Monotonic (@Kseq) (- ==> cont_match p ++> cont_match p)
    | Kloop1_match:
        Monotonic (@Kloop1) (- ==> - ==> cont_match p ++> cont_match p)
    | Kloop2_match:
        Monotonic (@Kloop2) (- ==> - ==> cont_match p ++> cont_match p)
    | Kswitch_match:
        Monotonic (@Kswitch) (cont_match p ++> cont_match p)
    | Kcall_match:
        Monotonic
          (@Kcall)
          (- ==> - ==>
           env_match p ++>
           temp_env_match p ++>
           cont_match p ++>
           cont_match p).

  Global Existing Instance Kstop_match.
  Global Existing Instance Kseq_match.
  Global Existing Instance Kloop1_match.
  Global Existing Instance Kloop2_match.
  Global Existing Instance Kswitch_match.
  Global Existing Instance Kcall_match.

  Global Instance cont_match_le:
    Monotonic (@cont_match) ((≤) ++> subrel).
  Proof.
    repeat red.
    intros x y H x0 y0 H0.
    revert y H.
    induction H0; constructor; auto; solve_monotonic.
  Qed.

  Global Instance call_cont_match p:
    Monotonic (@call_cont) (cont_match p ++> cont_match p).
  Proof.
    intros k1 k2 Hk.
    induction Hk; simpl; solve_monotonic.
  Qed.

  Section LOCALS2.
    Local Instance is_call_cont_match_strong p:
      Monotonic (@is_call_cont) (cont_match p ++> iff).
    Proof.
      intros k1 k2 Hk.
      destruct Hk; solve_monotonic.
    Qed.

    Global Instance is_call_cont_match_weak p:
      Monotonic (@is_call_cont) (cont_match p ++> impl).
    Proof.
      solve_monotonic.
    Qed.
  End LOCALS2.

  Inductive state_match Rf p: rel (state (mem := mwd D1)) (state (mem := mwd D2)) :=
    | State_rel:
        Monotonic
          State
          (- ==> - ==>
           cont_match p ++>
           env_match p ++>
           temp_env_match p ++>
           match_mem R p ++>
           state_match Rf p)
    | Callstate_rel:
        Monotonic
          Callstate
          (Rf ++>
           list_rel (match_val R p) ++>
           (cont_match p /\ lsat is_call_cont) ++>
           match_mem R p ++>
           state_match Rf p)
    | Returnstate_rel:
        Monotonic
          Returnstate
          (match_val R p ++>
           (cont_match p /\ lsat is_call_cont) ++>
           match_mem R p ++>
           state_match Rf p).

  Global Existing Instance State_rel.
  Global Existing Instance Callstate_rel.
  Global Existing Instance Returnstate_rel.

  Global Instance: Params (@State) 6.
  Global Instance: Params (@Callstate) 4.
  Global Instance: Params (@Returnstate) 3.

  Scheme statement_ind_mutual := Induction for statement Sort Prop
    with ls_ind_mutual := Induction for labeled_statements Sort Prop.

  Global Instance find_label_match p:
    Monotonic
      (@find_label)
      (- ==> - ==> cont_match p ++> option_rel (eq * cont_match p)).
  Proof.
    intros lbl s.
    pattern s.
    pose proof Some_rel.
    eapply statement_ind_mutual with
      (P0 := fun ls =>
                 (cont_match p ++> option_rel (eq * cont_match p))%rel
                 (find_label_ls lbl ls)
                 (find_label_ls lbl ls));
    simpl; intros;
    solve_monotonic.
    destruct (ident_eq _ _); rauto. (* XXX coqrel *)
  Qed.

  Global Instance function_entry2_match Rf p:
    Monotonic
      function_entry2
      (clight_genv_le Rf ++>
       - ==>
       list_rel (match_val R p) ++>
       match_mem R p ++>
       % % set_rel (incr p (env_match p * temp_env_match p * match_mem R p))).
  Proof.
    intros ge1 ge2 Hge f vargs1 vargs2 Hvargs m1 m2 Hm [[e1 le1] m1'] H.
    simpl in *.
    destruct H as [Hfvnr Hfpnr Hfvpd Hm1' Hle1].
    pose proof (empty_env_match p) as Hee.
    destruct (alloc_variables_match Rf p _ _ Hge _ _ Hee _ _ Hm _ (e1, m1') Hm1')
      as ((e2 & m2') & Hm2' & p' & Hp' & He & Hm').
    transport Hle1.
    exists (e2, x, m2').
    simpl in *.
    split.
    - constructor; eauto.
    - exists p'.
      split; eauto.
      solve_monotonic.
  Qed.

  Hint Extern 1 (Transport _ _ _ _ _) =>
    rel_curry2_set_rel_transport @function_entry2 : typeclass_instances.

  (** Special case for [Genv.find_funct] *)

  Global Instance find_funct_transfer {F V} Rf p ge1 ge2 v1 v2 f1:
    Transport
      (genv_le (F:=F) (V:=V) Rf * match_val R p)%rel
      (ge1, v1)
      (ge2, v2)
      (Genv.find_funct ge1 v1 = Some f1)
      (exists f2,
         Genv.find_funct ge2 v2 = Some f2 /\
         exists b, v1 = Vptr b Ptrofs.zero /\ Rf b f1 f2).
  Proof.
    repeat red.
    intros [Hge Hv].
    simpl in Hge, Hv.
    intros H.
    inversion Hv; subst; try discriminate.
    generalize H. intro H_.
    simpl in H_.
    destruct (Ptrofs.eq_dec _ _); try discriminate.
    subst.
    generalize H0. intro H0_.
    assert (block_is_global b1) as GLOBAL by eauto.
    apply (match_global_ptrbits p _ Ptrofs.zero) in GLOBAL.
    generalize (match_ptrbits_functional _ _ _ _ H0 GLOBAL).
    inversion 1; subst.
    simpl.
    destruct (Ptrofs.eq_dec _ _); try congruence.
    clear H.
    transport H_.
    eauto.
  Qed.

  Definition state_sim Rf := (rexists p, state_match Rf p)%rel.

  Require Import CompCertBuiltins.
  Context `{ec1_ops: !ExternalCallsOpsX (mwd D1)}.
  Context `{ec2_ops: !ExternalCallsOpsX (mwd D2)}.
  Context `{eb1: !EnableBuiltins (mwd D1)}.
  Context `{eb2: !EnableBuiltins (mwd D2)}.

  (*Context `{res_id: I64helpers.ReservedId}.
  Context `{cc1_ops: !CompilerConfigOps mem1}.
  Context `{cc2_ops: !CompilerConfigOps mem2}.*)

  Class ClightFunrel (Rf: block -> rel fundef fundef) ge1 ge2 :=
    {
      clight_funrel_type b :>
        Proper (Rf b ++> eq) type_of_fundef;
      clight_funrel_builtin_disabled:
        cc_enable_external_as_builtin (mem := mwd D1) = false;
      clight_funrel_callstate_sim p b t :>
        clight_genv_le Rf ge1 ge2 ->
        Related
          (fun f1 vargs1 k1 m1 s1' =>
             step2 ge1 (Callstate f1 vargs1 k1 m1) t s1')
          (fun f2 vargs2 k2 m2 s2' =>
             Smallstep.plus step2 ge2 (Callstate f2 vargs2 k2 m2) t s2')
          (Rf b ++>
           list_rel (match_val R p) ++>
           (cont_match p /\ lsat is_call_cont) ++>
           match_mem R p ++>
           set_rel (incr p (state_match (rexists b, Rf b) p)))
    }.

  Require EventsX.
  Import Smallstep.

  Definition genv_sim Rf (ge1 ge2: genv) :=
    (rforall p,
       state_match Rf p ++>
       - ==>
       set_rel (incr p (state_match Rf p)))%rel
    (Clight.step2 ge1)
    (plus Clight.step2 ge2).

  Lemma genv_sim_plus Rf:
    (rforall p,
       genv_sim Rf ++>
       state_match Rf p ++>
       - ==>
       set_rel (incr p (state_match Rf p)))%rel
    (plus Clight.step2)
    (plus Clight.step2).
  Proof.
    intros p ge1 ge2 Hge s1 s2 Hs t s1' Hs1'.
    revert p s2 Hs.
    pattern s1, t, s1'.
    eapply plus_ind2; try eassumption; clear s1 t s1' Hs1'.
    - intros s1 t s1' Hstep p s2 Hs.
      eapply (Hge p); eauto.
    - intros s1 t s1' u s1'' tu H1 H1' IH Htu.
      intros p1 s2 Hs.
      eapply Hge in H1; eauto.
      destruct H1 as (s2' & H2 & p' & (INCR' & Hs')).
      edestruct IH as (s2'' & H2' & p'' & (INCR'' & Hs'')); eauto.
      exists s2''.
      split.
      + eapply plus_trans; eauto.
      + exists p''.
        split; eauto.
        etransitivity; eauto.
  Qed.

  Lemma call_cont_is_call_cont k:
    is_call_cont (call_cont k).
  Proof.
    induction k; simpl; try constructor; eauto.
  Qed.

  Lemma clight_sim `{HRf: ClightFunrel}:
    clight_genv_le Rf ge1 ge2 ->
    genv_sim (rexists b, Rf b) ge1 ge2.
  Proof.
    intros Hge.
    intros p s1 s2 Hs t s1' H1.
    pose proof (assign_loc_match Rf p) as Hal.
    pose proof (sem_cast_match R) as Hcast.
    pose proof (bool_val_match R) as Hbv.

    deconstruct H1 ltac:(fun x => pose (c := x)); inversion Hs; clear Hs; subst.

    -
    transport_hyps; subst.
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; solve_monotonic ].
    erewrite <- clight_funrel_type; eassumption.
    split.
    { reflexivity. }
    solve_monotonic.

    -
    pose proof (builtin_external_call_x_match (F:=fundef) (V:=type) R p ef) as Hbc.
    specialize (Hbc clight_funrel_builtin_disabled BUILTIN_ENABLED).
    assert (Hecp: Params (@external_call) 6) by constructor.
    transport_hyps.
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; solve_monotonic ].
    {
      destruct ef; try reflexivity.
      simpl in BUILTIN_ENABLED.
      rewrite clight_funrel_builtin_disabled in BUILTIN_ENABLED.
      elim BUILTIN_ENABLED.
    }
    split.
    {
      eassumption.
    }
    solve_monotonic.

    -
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    inversion H7; clear H7; subst.
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    inversion H7; clear H7; subst.
    transport_hyps; subst.
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    inversion H7; clear H7; subst.
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    inversion H7; clear H7; subst;
    (transport_hyps; subst;
     eexists;
     split;
     [ eapply Smallstep.plus_one; eapply c; eauto |
       eexists; split; solve_monotonic ]).

    -
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    inversion H7; clear H7; subst.
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    inversion H7; clear H7; subst.
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    inversion H7; clear H7; subst.
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    inversion H7; clear H7; subst.
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    transport_hyps; subst.
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].
    split.
    + eapply cont_match_le; eauto.
      solve_monotonic.
    + apply call_cont_is_call_cont.

    -
    transport_hyps; subst.
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].
    + split.
      * eapply cont_match_le; eauto.
        solve_monotonic.
      * apply call_cont_is_call_cont.

    -
    transport_hyps; subst.
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].
    +
    eapply @is_call_cont_match_weak; eauto. (* TODO: this step should be automatic *)
    + split.
      * eapply cont_match_le; eauto.
      * assumption.

    -
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    inversion H7; clear H7; subst.
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    inversion H7; clear H7; subst.
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    transport e0.
    destruct x.
    inversion H0; clear H0; simpl in *; subst.
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].

    -
    destruct H4.
    eapply clight_funrel_callstate_sim in H1; eauto.

    -
    destruct H4.
    eapply clight_funrel_callstate_sim in H1; eauto.

    -
    destruct H5 as [H5 ?].
    inversion H5; clear H5; subst.
    transport_hyps; subst;
    eexists;
    split;
    [ eapply Smallstep.plus_one; eapply c; eauto |
      eexists; split; solve_monotonic ].
  Qed.
End CLIGHT_REL.

(** Redeclare the [set_rel_transport] instances. *)
Hint Extern 1 (Transport _ _ _ _ _) =>
  set_rel_transport @deref_loc : typeclass_instances.
Hint Extern 1 (Transport _ _ _ _ _) =>
  set_rel_transport @assign_loc : typeclass_instances.
Hint Extern 1 (Transport _ _ _ _ _) =>
  set_rel_transport @bind_parameters : typeclass_instances.
Hint Extern 1 (Transport _ _ _ _ _) =>
  set_rel_transport @eval_expr : typeclass_instances.
Hint Extern 1 (Transport _ _ _ _ _) =>
  rel_curry_set_rel_transport @eval_lvalue : typeclass_instances.
Hint Extern 1 (Transport _ _ _ _ _) =>
  set_rel_transport @eval_exprlist : typeclass_instances.
Hint Extern 1 (Transport _ _ _ _ _) =>
  rel_curry2_set_rel_transport @function_entry2 : typeclass_instances.
Hint Extern 1 (Transport _ _ _ _ _) =>
  rel_curry_set_rel_transport @external_call : typeclass_instances.

author: DeepSpec


text:
From Coq Require Import
     String.
From ExtLib Require Import
     Monad.
From SimpleIO Require Import
     IO_Random
     SimpleIO.
Import
  MonadNotation.
Open Scope monad_scope.
Open Scope string_scope.

Definition coin : IO unit :=
  b <- ORandom.bool tt;;
  print_endline (if b : bool then "head" else "tail").

RunIO (ORandom.self_init tt;; coin;; coin;; coin).

author: Lysxia

repo: coq-simple-io

save_path: github-repos/coq/Lysxia-coq-simple-io


text:
(** * Bush *)

Require Import LNDT.
Require Import Spreadable.

(* DOESN'T WORK

Definition Bush : TT := LNDT Bush.
Fixpoint Bush : TT := LNDT Bush.

Definition bush_spreadable : SpreadAble Bush :=
  lndt_spreadable bush_spreadable.

Definition bush_map         n := map         _ (map_able _ bush_spreadable).
Definition bush_cng_map     n := map_congru  _ (map_able _ bush_spreadable).
Definition bush_cmp_map     n := map_compo   _ (map_able _ bush_spreadable).
Definition bush_foldr       n := foldr       _ (fold_able _ bush_spreadable).
Definition bush_foldl       n := foldl       _ (fold_able _ bush_spreadable).
Definition bush_size        n := size        _ (fold_able _ bush_spreadable).
Definition bush_flatten     n := flatten     _ (fold_able _ bush_spreadable).
Definition bush_show        n := show        _ (fold_able _ bush_spreadable).
Definition bush_any         n := any         _ (any_all_able _ bush_spreadable).
Definition bush_dec_any     n := dec_any     _ (any_all_able _ bush_spreadable).
Definition bush_all         n := all         _ (any_all_able _ bush_spreadable).
Definition bush_dec_all     n := dec_all     _ (any_all_able _ bush_spreadable).
Definition bush_in_prop     n := in_prop     _ (any_all_able _ bush_spreadable).
Definition bush_empty       n := empty       _ (any_all_able _ bush_spreadable).
Definition bush_dec_in_prop n := dec_in_prop _ (any_all_able _ bush_spreadable).
Definition bush_dec_eq      n := dec_eq      _ (eq_able _ bush_spreadable). *)

author: mmontin

repo: libndt

save_path: github-repos/coq/mmontin-libndt