text:
(* *********************************************************************)
(*                                                                     *)
(*            The CertiKOS Certified Kit Operating System              *)
(*                                                                     *)
(*                   The FLINT Group, Yale University                  *)
(*                                                                     *)
(*  Copyright The FLINT Group, Yale University.  All rights reserved.  *)
(*  This file is distributed under the terms of the Yale University    *)
(*  Non-Commercial License Agreement.                                  *)
(*                                                                     *)
(* *********************************************************************)
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import MemWithData.
Require Import EventsX.
Require Import Globalenvs.
Require Import LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import VCGen.
Require Import RealParams.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import I64Layer.
Require Import CompCertiKOSproof.
Require Import LinkTactic.
Require Import LayerCalculusLemma.
Require Import PCurID.
Require Import PThreadSched.
Require Import PCurIDCSource.
Require Import PCurIDCode.
Require Import ThreadSchedGen.
Require Import ThreadSchedGenSpec.
Require Import ThreadSchedGenLinkSource.
Require Import ThreadSchedGenAsmSource.
Require Import ThreadSchedGenAsm.

Section WITHCOMPCERTIKOS.

  Context `{compcertikos_prf: CompCertiKOS}.

  Context `{real_params_prf : RealParams}.

  Notation HDATA := AbstractDataType.RData.
  Notation LDATA := AbstractDataType.RData.

  Notation HDATAOps := (cdata (cdata_ops := pthreadsched_data_ops) HDATA).
  Notation LDATAOps := (cdata (cdata_ops := pcurid_data_ops) LDATA).

  Definition oplus_monotonic := PseudoJoin.oplus_monotonic
    (A := compatlayer (cdata _ (cdata_ops := pcurid_data_ops))).
  Definition oplus_sim_monotonic := PseudoJoin.oplus_sim_monotonic.
  Definition right_upper_bound := Structures.right_upper_bound
    (A := compatlayer (cdata _ (cdata_ops := pcurid_data_ops))).
  Definition left_upper_bound := Structures.left_upper_bound
    (A := compatlayer (cdata _ (cdata_ops := pcurid_data_ops))).

  (*
  Lemma thread_kill_correct :
    forall COMPILABLE: LayerCompilable (pcurid ⊕ L64),
    forall MOK: ModuleOK (thread_kill ↦ f_thread_kill),
    forall M2: LAsm.module,
      CompCertiKOS.transf_module (thread_kill ↦ f_thread_kill) = OK M2 ->
      cl_sim _ _
             (crel HDATA LDATA)
             (thread_kill ↦ gensem thread_kill_spec)
             (〚 M2 〛(pcurid ⊕ L64)).
  Proof.
    intros.
    eapply link_compiler; eauto.
    - eapply thread_kill_spec_ref.
    - link_nextblock.
    - link_kernel_mode.
    - eapply PCURIDCODE.thread_kill_code_correct.
    - transitivity pcurid_impl; [| apply impl_le ].
      apply le_right, le_right, le_right.
      apply oplus_monotonic; [ reflexivity |].
      apply oplus_monotonic; [ reflexivity |].
      apply le_right, le_right.
      reflexivity.
  Qed.
  *)

  Lemma thread_spawn_correct :
    forall COMPILABLE: LayerCompilable (pcurid ⊕ L64),
    forall MOK: ModuleOK (thread_spawn ↦ f_thread_spawn),
    forall M2: LAsm.module,
      CompCertiKOS.transf_module (thread_spawn ↦ f_thread_spawn) = OK M2 ->
      cl_sim _ _
             (crel HDATA LDATA)
             (thread_spawn ↦ dnew_compatsem thread_spawn_spec)
             (〚 M2 〛(pcurid ⊕ L64)).
  Proof.
    intros.
    eapply link_compiler; eauto.
    - eapply thread_spawn_spec_ref.
    - link_nextblock.
    - link_kernel_mode.
    - eapply PCURIDCODE.thread_spawn_code_correct.
    - sim_oplus.
  Qed.

  Lemma thread_wakeup_correct :
    forall COMPILABLE: LayerCompilable (pcurid ⊕ L64),
    forall MOK: ModuleOK (thread_wakeup ↦ f_thread_wakeup),
    forall M2: LAsm.module,
      CompCertiKOS.transf_module (thread_wakeup ↦ f_thread_wakeup) = OK M2 ->
      cl_sim _ _
             (crel HDATA LDATA)
             (thread_wakeup ↦ gensem thread_wakeup_spec)
             (〚 M2 〛(pcurid ⊕ L64)).
  Proof.
    intros.
    eapply link_compiler; eauto.
    - eapply thread_wakeup_spec_ref.
    - link_nextblock.
    - link_kernel_mode.
    - eapply PCURIDCODE.thread_wakeup_code_correct.
    - sim_oplus.
  Qed.

  Lemma sched_init_correct :
    forall COMPILABLE: LayerCompilable (pcurid ⊕ L64),
    forall MOK: ModuleOK (sched_init ↦ f_sched_init),
    forall M2: LAsm.module,
      CompCertiKOS.transf_module (sched_init ↦ f_sched_init) = OK M2 ->
      cl_sim _ _
             (crel HDATA LDATA)
             (sched_init ↦ gensem sched_init_spec)
             (〚 M2 〛(pcurid ⊕ L64)).
  Proof.
    intros.
    eapply link_compiler; eauto.
    - eapply sched_init_spec_ref.
    - link_nextblock.
    - link_kernel_mode.
    - eapply PCURIDCODE.sched_init_code_correct.
    - sim_oplus.
  Qed.

  Lemma thread_sched_correct:
      cl_sim _ _
             (crel HDATA LDATA)
             (thread_sched ↦ primcall_thread_schedule_compatsem thread_sched_spec (prim_ident:= thread_sched))
             (〚 thread_sched ↦ threadsched_function 〛 pcurid).
  Proof.
    intros.
    eapply link_assembly; eauto.
    - eapply thread_sched_spec_ref.
    - eapply thread_sched_code_correct.
  Qed.

  Record PThreadSched_impl_inverted (M: module): Prop :=
    {
      (*
      PThreadSched_thread_kill: module;
      *)
      PThreadSched_thread_spawn: module;
      PThreadSched_thread_wakeup: module;
      PThreadSched_sched_init: module;
      (*
      PThreadSched_thread_kill_transf:
        CompCertiKOS.transf_module (thread_kill ↦ f_thread_kill) =
        ret PThreadSched_thread_kill;
      *)
      PThreadSched_thread_spawn_transf:
        CompCertiKOS.transf_module (thread_spawn ↦ f_thread_spawn) =
        ret PThreadSched_thread_spawn;
      PThreadSched_thread_wakeup_transf:
        CompCertiKOS.transf_module (thread_wakeup ↦ f_thread_wakeup) =
        ret PThreadSched_thread_wakeup;
      PThreadSched_sched_init_transf:
        CompCertiKOS.transf_module (sched_init ↦ f_sched_init) =
        ret PThreadSched_sched_init;
      PThreadSched_M:
        M = (((*PThreadSched_thread_kill ⊕*) PThreadSched_thread_spawn ⊕ PThreadSched_thread_wakeup ⊕ PThreadSched_sched_init)
               ⊕ (thread_sched ↦ threadsched_function)) ⊕ ∅;
      PThreadSched_MOK:
        LayerOK (〚M〛 (pcurid ⊕ L64) ⊕ pcurid ⊕ L64)
    }.

  Lemma module_impl_imply:
    forall M, PThreadSched_impl = OK M -> PThreadSched_impl_inverted M.
  Proof.
    unfold PThreadSched_impl. intros M HM.
    inv_monad' HM.
    econstructor.
    (*
    eassumption.
    *)
    eassumption.
    eassumption.
    eassumption.
    inv HM3. reflexivity.
    apply x3.
  Qed.

  Lemma link_correct_aux:
    forall M, PThreadSched_impl = OK M ->
              pcurid ⊕ L64
                    ⊢ (path_inj (crel HDATA LDATA), M)
              : pthreadsched ⊕ L64.
  Proof.
    unfold PThreadSched_impl. intros M HM.
    apply module_impl_imply in HM; destruct HM; subst.
    unfold pthreadsched, pthreadsched_fresh_c, pthreadsched_fresh_asm.
    eapply conseq_le_assoc_comm.
    hcomp_tac.
    {
      hcomp_tac.
      {
        layer_link_split_tac.
        (*
        - apply thread_kill_correct; code_correct_tac.
        *)
        - apply thread_spawn_correct; code_correct_tac.
        - apply thread_wakeup_correct; code_correct_tac.
        - apply sched_init_correct; code_correct_tac.
      }
      {
        apply Language.conseq_le_left with pcurid; [| apply left_upper_bound ].
        layer_link_split_tac; apply thread_sched_correct.
      }
    }
    {
      eapply layer_link_new_glbl_both.
      apply oplus_sim_monotonic.
      apply passthrough_correct.
      apply L64_auto_sim.
    }
  Qed.

  Require Import FlatMemory.
  Require Import Decision.
  Require Import LAsmModuleSem.
  Require Import Soundness.
  Require Import CompatExternalCalls.
  Require Import AuxLemma.
  Require Import Behavior.

  Lemma init_correct:
    forall M, PThreadSched_impl = OK M ->
              ModuleOK M ->
              cl_init_sim HDATAOps LDATAOps (crel HDATA LDATA) (pthreadsched ⊕ L64) M (pcurid ⊕ L64).
  Proof.
    intros.
    pose proof (fun i => module_ok_variable M i (H0 i)) as MOK; clear H0.
    apply cl_init_sim_intro.
    - constructor; simpl; trivial.
      constructor; simpl; trivial. apply FlatMem.flatmem_empty_inj.
      apply kctxt_inj_empty.
      constructor.
    - intros; inv H0.
    - intros; inv H0.
    - intros; inv H0.
    - intros. unfold PThreadSched_impl in H.
      apply module_impl_imply in H; destruct H; subst.
      transf_none i. specialize (MOK i).
      assert (get_module_variable i ((((*PThreadSched_thread_kill ⊕*) PThreadSched_thread_spawn ⊕ PThreadSched_thread_wakeup ⊕ PThreadSched_sched_init) ⊕ thread_sched ↦ threadsched_function) ⊕ ∅) = OK None).
      {
        get_module_variable_relfexivity.
      }
      unfold module, module_ops in *.
      congruence.
    - decision.
  Qed.

  Theorem cl_simulation:
    forall p (s: stencil) (CTXT M: module) pl ph
           (builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
      PThreadSched_impl = OK M ->
      make_program s CTXT (pthreadsched ⊕ L64) = OK ph ->
      make_program s (CTXT ⊕ M) (pcurid ⊕ L64) = OK pl ->
      simulation
        (LAsm.semantics (lcfg_ops := LC (pthreadsched ⊕ L64)) ph)
        (LAsm.semantics (lcfg_ops := LC (pcurid ⊕ L64)) pl)
        (observe_lasm _ p) (observe_lasm _ p).
  Proof.
    intros.
    eapply (soundness_simulation (crel HDATA LDATA)); try eassumption; try decision.

    eapply link_correct_aux; eauto.
    eapply init_correct; eauto.
    eapply make_program_oplus_right; eassumption.

    apply module_impl_imply in H; destruct H; assumption.
  Qed.

  Theorem cl_forward_simulation:
    forall (s: stencil) (CTXT M: module) pl ph
           (builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
      PThreadSched_impl = OK M ->
      make_program s CTXT (pthreadsched ⊕ L64) = OK ph ->
      make_program s (CTXT ⊕ M) (pcurid ⊕ L64) = OK pl ->
      forward_simulation
        (LAsm.semantics (lcfg_ops := LC (pthreadsched ⊕ L64)) ph)
        (LAsm.semantics (lcfg_ops := LC (pcurid ⊕ L64)) pl).
  Proof.
    intros.
    eapply (soundness_forward (crel HDATA LDATA)); try eassumption; try decision.

    eapply link_correct_aux; eauto.
    eapply init_correct; eauto.
    eapply make_program_oplus_right; eassumption.

    apply module_impl_imply in H; destruct H; assumption.
  Qed.

  Theorem cl_backward_simulation:
    forall (s: stencil) (CTXT M: module) pl ph
           (builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
      PThreadSched_impl = OK M ->
      make_program s CTXT (pthreadsched ⊕ L64) = OK ph ->
      make_program s (CTXT ⊕ M) (pcurid ⊕ L64) = OK pl ->
      backward_simulation
        (LAsm.semantics (lcfg_ops := LC (pthreadsched ⊕ L64)) ph)
        (LAsm.semantics (lcfg_ops := LC (pcurid ⊕ L64)) pl).
  Proof.
    intros.
    eapply (soundness (crel HDATA LDATA)); try eassumption; try decision.

    eapply link_correct_aux; eauto.
    eapply init_correct; eauto.
    eapply make_program_oplus_right; eassumption.

    apply module_impl_imply in H; destruct H; assumption.
  Qed.

  Require Import LAsmModuleSemMakeProgram.

  Theorem make_program_exists:
    forall (s: stencil) (CTXT M: module) pl,
      PThreadSched_impl = OK M ->
      make_program s (CTXT ⊕ M) (pcurid ⊕ L64) = OK pl ->
      exists ph, make_program s CTXT (pthreadsched ⊕ L64) = OK ph.
  Proof.
    intros.
    exploit link_correct_aux; eauto.
    eapply make_program_vertical' in H0.
    destruct H0 as [p' Hmake].
    intros Hle.
    eapply make_program_sim_monotonic_exists.
    2: eapply Hle.
    reflexivity.
    eassumption.
    apply module_impl_imply in H; destruct H; assumption.
  Qed.

End WITHCOMPCERTIKOS.

repo: certikos


text:
(* Generated by coq-of-rust *)
Require Import CoqOfRust.CoqOfRust.

Import Root.std.prelude.rust_2015.

Error StructUnit.

Module Single.
  Inductive t : Set := Build (_ : A).

  Global Instance Get_0 : IndexedField.Class t 0 _ := {|
    IndexedField.get '(Build x0) := x0;
  |}.
End Single.
Definition Single := Single.t.

Module SingleGen.
  Inductive t : Set := Build (_ : T).

  Global Instance Get_0 : IndexedField.Class t 0 _ := {|
    IndexedField.get '(Build x0) := x0;
  |}.
End SingleGen.
Definition SingleGen := SingleGen.t.

Definition main (_ : unit) : unit :=
  let _s := Single.Build A in
  let _char := SingleGen.Build a in
  let _t := SingleGen.Build A in
  let _i32 := SingleGen.Build 6 in
  let _char := SingleGen.Build a in
  tt.

author: formal-land

repo: coq-of-rust


text:
(*
A3. Arithmetic Properties
=========================
*)

From graph_pebbling Require Import A1_misc A2_lift.

Infix ".≤" := (liftR le) (at level 60).
Infix ".+" := (lift2 Nat.add) (at level 50).
Infix ".-" := (lift2 Nat.sub) (at level 50).
Infix ".*" := (lift2 Nat.mul) (at level 50).

Notation "(+)" := Nat.add (only parsing).
Notation "(-)" := Nat.sub (only parsing).
Notation "(.+)" := (lift2 Nat.add) (only parsing).
Notation "(.-)" := (lift2 Nat.sub) (only parsing).
Notation "(.*)" := (lift2 Nat.mul) (only parsing).

Notation min := Nat.min.
Notation max := Nat.max.
Notation lift_min := (lift2 min).
Notation lift_max := (lift2 max).

Notation gcd := Nat.gcd.
Notation "m ∣ n" := ((m | n)) (at level 50).

Ltac inst_lift_le x :=
  repeat match goal with
  | H : _ .≤ _ |- _ => inst H x; clear H
  end.

Ltac ext_lia :=
  let x := fresh "x" in
  extensionality x;
  inst_lift_le x; cbn; lia.

(* Nat.sub with the subtrahend first. *)
Definition subtract (n k : nat) := k - n.
Global Arguments subtract _ _ /.
Global Arguments min _ _ : simpl nomatch.

Section Properties.

Ltac see H := repeat intro; cbn; apply H.

Global Instance : IdemP (=) Nat.max := Nat.max_id.
Global Instance : IdemP (=) Nat.min := Nat.min_id.

Global Instance : LeftId (=) 0 Nat.max := Nat.max_0_l.
Global Instance : RightId (=) 0 Nat.max := Nat.max_0_r.
Global Instance : LeftId (=) 0 Nat.add := Nat.add_0_l.
Global Instance : RightId (=) 0 Nat.add := Nat.add_0_r.
Global Instance : LeftId (=) 1 Nat.mul := Nat.mul_1_l.
Global Instance : RightId (=) 1 Nat.mul := Nat.mul_1_r.

Global Instance : LeftAbsorb (=) 0 Nat.min := Nat.min_0_l.
Global Instance : RightAbsorb (=) 0 Nat.min := Nat.min_0_r.
Global Instance : LeftAbsorb (=) 0 Nat.mul := Nat.mul_0_l.
Global Instance : RightAbsorb (=) 0 Nat.mul := Nat.mul_0_r.

Global Instance : Assoc (=) Nat.min := Nat.min_assoc.
Global Instance : Assoc (=) Nat.max := Nat.max_assoc.
Global Instance : Assoc (=) Nat.add := Nat.add_assoc.
Global Instance : Assoc (=) Nat.mul := Nat.mul_assoc.

Global Instance : Comm (=) Nat.min := Nat.min_comm.
Global Instance : Comm (=) Nat.max := Nat.max_comm.
Global Instance : Comm (=) Nat.add := Nat.add_comm.
Global Instance : Comm (=) Nat.mul := Nat.mul_comm.

Global Instance : LeftDistr (=) Nat.mul Nat.add := Nat.mul_add_distr_l.
Global Instance : RightDistr (=) Nat.mul Nat.add := Nat.mul_add_distr_r.
Global Instance : LeftDistr (=) Nat.mul Nat.sub. see Nat.mul_sub_distr_l. Qed.
Global Instance : RightDistr (=) Nat.mul Nat.sub. see Nat.mul_sub_distr_r. Qed.
Global Instance : LeftDistr (=) Nat.mul subtract. see Nat.mul_sub_distr_l. Qed.
Global Instance : RightDistr (=) Nat.mul subtract. see Nat.mul_sub_distr_r. Qed.

Global Instance left_dominant_le n :
  LeftDominant (le n) (+).
Proof. clia. Qed.

Global Instance left_comm_S_add :
  CondLeftComm (=) (λ _, True) S (+).
Proof. clia. Qed.

Global Instance left_comm_add_add n :
  CondLeftComm (=) (λ _, True) ((+) n) (+).
Proof. clia. Qed.

Global Instance left_comm_subtract_add n :
  CondLeftComm (=) (le n) (subtract n) (+).
Proof. clia. Qed.

End Properties.

Lemma alter_add `{EqDecision A} (f : A -> nat) n a :
  alter ((+) n) a f = f .+ <[a:=n]> (const 0).
Proof.
extensionality b; dec (b = a);
simpl_alter; cbn; simpl_insert; clia.
Qed.

author: bergwerf

repo: pebbling

save_path: github-repos/coq/bergwerf-pebbling


text:
Require Import Coqlib.
Require Import STS.
Require Import Behavior.
Require Import ModSem.
Import ModSemL.
Require Import Skeleton.
Require Import PCM.
Require Import Any.
Require Import SimSTS.
Require Import HoareDef.
Require Import SimModSem.
Require Import HTactics.
From Ordinal Require Import Ordinal Arithmetic.

Set Implicit Arguments.

Module TAC.
  Ltac my_steps := repeat (_steps; des_ifs_safe).
  Ltac my_force_l := _force_l.
  Ltac my_force_r := _force_r.
End TAC.
Import TAC.

Section CANCEL.

  (*** execute following commands in emacs (by C-x C-e)
     (progn (highlight-phrase "Any" 'hi-red-b) (highlight-phrase "Any_src" 'hi-green-b) (highlight-phrase "Any_tgt" 'hi-blue-b)
            (highlight-phrase "Any_mid" 'hi-light-green-b)
            (highlight-phrase "Y" 'hi-green-b) (highlight-phrase "Z" 'hi-green-b)) ***)
  Let Any_src := Any.t. (*** src argument (e.g., List nat) ***)
  Let Any_mid := Any.t. (*** src argument (e.g., List nat) ***)
  Let Any_tgt := Any.t. (*** tgt argument (i.e., list val) ***)

  Context `{Σ: GRA.t}.

  Variable mds: list SMod.t.

  Let sk: Sk.t := Sk.sort (fold_right Sk.add Sk.unit (List.map SMod.sk mds)).
  (* Let skenv: SkEnv.t := Sk.load_skenv sk. *)
  Let mss: list SModSem.t := (List.map ((flip SMod.get_modsem) sk) mds).
  Let sbtb: list (gname * fspecbody) := (List.flat_map (SModSem.fnsems) mss).
  Let _stb: list (gname * fspec) := List.map (fun '(fn, fs) => (fn, fs.(fsb_fspec))) sbtb.

  Variable stb: gname -> option fspec.
  Hypothesis STBCOMPLETE:
    forall fn fsp (FIND: alist_find fn _stb = Some fsp), stb fn = Some fsp.
  Hypothesis STBSOUND:
    forall fn (FIND: alist_find fn _stb = None),
      (<<NONE: stb fn = None>>) \/ (exists fsp, <<FIND: stb fn = Some fsp>> /\ <<TRIVIAL: forall x, fsp.(measure) x = ord_top>>).

  Let mds_src: list Mod.t := List.map (SMod.to_src) mds.
  Let mds_mid2: list Mod.t := List.map (SMod.to_mid2 stb) mds.

  Let W: Type := p_state.

  Opaque EventsL.interp_Es.

  Let ms_src: ModSemL.t := ModL.enclose (Mod.add_list mds_src).
  Let ms_mid2: ModSemL.t := ModL.enclose (Mod.add_list mds_mid2).

  Let p_src := ModSemL.prog ms_src.
  Let p_mid2 := ModSemL.prog ms_mid2.

  Require Import IRed.

  Lemma my_lemma__APC o (w: unit) st
    :
      paco8 (_sim_itree (fun (_: unit) '(st_src, st_tgt) => st_src = st_tgt) top2) bot8 unit unit
            (fun st_src st_tgt _ _ => st_src = st_tgt)
            false false w
            (st, Ret tt)
            (st, interp_hCallE_mid2 (_APC o)).
  Proof.
    ginit. revert w st.
    induction (Ord.lt_well_founded o); i. clear H. rename x into o. rename H0 into IH.
    rewrite unfold_APC. my_steps.
    destruct x.
    { my_steps. }
    my_steps. deflag.
    eapply IH; auto.
  Qed.

  Lemma idK_spec2: forall E A B (a: A) (itr: itree E B), itr = Ret a >>= fun _ => itr. Proof. { i. ired. ss. } Qed.

  Context {CONF: EMSConfig}.
  Theorem adequacy_type_m2s:
    Beh.of_program (ModL.compile (Mod.add_list mds_mid2)) <1=
    Beh.of_program (ModL.compile (Mod.add_list mds_src)).
  Proof.
    eapply ModSem.refines_close.
    eapply (@adequacy_local_list_strong mds_src mds_mid2).
    unfold mds_src, mds_mid2.
    eapply Forall2_apply_Forall2.
    { refl. }
    i. subst. econs; ss. i. econs; ss.
    { instantiate (1:=fun (_ _: unit) => True). ss. }
    { instantiate (1:=fun _ '(st_src, st_tgt) => st_src = st_tgt).
      eapply Forall2_apply_Forall2.
      { refl. }
      i. subst. destruct b0. econs; ss. ii. subst.
      unfold fun_to_src, fun_to_mid2, body_to_src, body_to_mid2. ss.
      generalize (fsb_body f y).
      revert mrs_tgt w. ginit. gcofix CIH. i. ides i.
      { steps. }
      { steps. deflag. gbase. eapply CIH. }
      rewrite <- bind_trigger.
      destruct e.
      { resub. destruct h. ired_both.
        Local Transparent APC. unfold APC. Local Opaque APC.
        force_r. i. ired_both.
        steps. deflag. rewrite (idK_spec2 tt (interp_hEs_src (k ()))).
        guclo lbindC_spec. econs.
        { deflag. gfinal. right. eapply paco8_mon.
          { eapply my_lemma__APC. }
          { i. ss. }
        }
        { i. ss. subst. destruct vret_tgt. steps.
          deflag. gbase. et.
        }
      }
      destruct e.
      { resub. destruct c. steps.
        deflag. gbase. et.
      }
      destruct s0.
      { resub. destruct p.
        { ired_both. force_r. force_l. steps.
          deflag. gbase. et.
        }
        { ired_both. force_r. force_l. steps.
          deflag. gbase. et.
        }
      }
      { resub. destruct e.
        { ired_both. force_r. i. force_l. exists x. steps.
          deflag. gbase. et.
        }
        { ired_both. force_l. i. force_r. exists x. steps.
          deflag. gbase. et.
        }
        { ired_both. steps.
          deflag. gbase. et.
        }
      }
    }
    { exists tt. ss. }
    Unshelve. all: ss.
  Qed.

End CANCEL.

author: alxest

repo: CCR

save_path: github-repos/coq/alxest-CCR