text:
Require Import Bool Vector List String Peano_dec.
Require Import Common FMap HVector ListSupport IndexSupport.
Require Import Syntax Topology Semantics Invariant.
Require Import RqRsLang.

Require Import Ex.Spec Ex.SpecInds Ex.Template Ex.Msi.
Require Import Ex.MsiInc.Msi Ex.MsiInc.MsiObjInv.

Set Implicit Arguments.

Local Open Scope list.
Local Open Scope hvec.
Local Open Scope fmap.

Section System.
  Variable tr: tree.
  Hypothesis (Htr: tr <> Node nil).

  Local Notation topo := (fst (tree2Topo tr 0)).
  Local Notation cifc := (snd (tree2Topo tr 0)).
  Local Notation impl := (impl Htr).

  Hint Extern 0 (TreeTopo _) => apply tree2Topo_TreeTopo.
  Hint Extern 0 (WfDTree _) => apply tree2Topo_WfDTree.

  Lemma msi_indices:
    map obj_idx (sys_objs impl) = c_li_indices cifc ++ c_l1_indices cifc.
  Proof.
    simpl; rewrite c_li_indices_head_rootOf at 2 by assumption.
    simpl; f_equal.
    rewrite map_app, map_map, map_id; simpl.
    rewrite map_map, map_id; reflexivity.
  Qed.

  Lemma msi_GoodORqsInit: GoodORqsInit (initsOf impl).
  Proof.
    apply initORqs_GoodORqsInit.
  Qed.

  Lemma msi_WfDTree: WfDTree topo.
  Proof.
    apply tree2Topo_WfDTree.
  Qed.

  Lemma msi_RqRsChnsOnDTree: RqRsChnsOnDTree topo.
  Proof.
    apply tree2Topo_RqRsChnsOnDTree.
  Qed.

  Lemma msi_RqRsChnsOnSystem: RqRsChnsOnSystem topo impl.
  Proof.
    eapply tree2Topo_RqRsChnsOnSystem with (tr0:= tr) (bidx:= [0]); try reflexivity.
    - destruct (tree2Topo _ _); reflexivity.
    - simpl.
      rewrite map_app.
      do 2 rewrite map_trans.
      do 2 rewrite map_id.
      rewrite app_comm_cons.
      rewrite <-c_li_indices_head_rootOf by assumption.
      reflexivity.
  Qed.

  Lemma msi_ExtsOnDTree: ExtsOnDTree topo impl.
  Proof.
    eapply tree2Topo_ExtsOnDTree with (tr0:= tr) (bidx:= [0]); try reflexivity.
    destruct (tree2Topo _ _); reflexivity.
  Qed.

  Lemma msi_RqRsDTree: RqRsDTree topo impl.
  Proof.
    red; repeat ssplit.
    - auto using msi_WfDTree.
    - auto using msi_RqRsChnsOnDTree.
    - auto using msi_RqRsChnsOnSystem.
    - auto using msi_ExtsOnDTree.
  Qed.

  Ltac solve_GoodRqRsRule_unfold ::= autounfold with MsiRules.

  Lemma msi_GoodRqRsSys: GoodRqRsSys topo impl.
  Proof.
    repeat
      match goal with
      | |- GoodRqRsSys _ _ => red
      | |- GoodRqRsObj _ _ _ => red
      | |- Forall _ _ => simpl; constructor; simpl
      | |- Forall _ (_ ++ _) => apply Forall_app
      end.

    - (** Main memory *)

      assert (In (rootOf topo) (c_li_indices cifc)) as Hrin.
      { rewrite c_li_indices_head_rootOf by assumption.
        left; reflexivity.
      }

      simpl.
      repeat
        match goal with
        | |- Forall _ (_ ++ _) => apply Forall_app
        | |- Forall _ (_ :: _) => constructor
        | |- Forall _ nil => constructor
        end.

      apply Forall_forall; intros.
      unfold liRulesFromChildren in H.
      apply concat_In in H; dest.
      apply in_map_iff in H; dest; subst.
      dest_in.
      all: try (solve_GoodRqRsRule; fail).

    - (** Li caches *)
      apply Forall_forall; intros.
      apply in_map_iff in H.
      destruct H as [oidx [? ?]]; subst.
      red; simpl.

      (* pre-register a fact: an Li cache always has a parent *)
      pose proof (c_li_l1_indices_has_parent
                    Htr _ _ (in_or_app _ _ _ (or_introl H0))).
      destruct H as [pidx ?].

      repeat
        match goal with
        | |- Forall _ (_ ++ _) => apply Forall_app
        | |- Forall _ (_ :: _) => constructor
        | |- Forall _ nil => constructor
        end.
      all: try (solve_GoodRqRsRule; fail).

      1: {
        apply Forall_forall; intros.
        unfold liRulesFromChildren in H1.
        apply concat_In in H1; dest.
        apply in_map_iff in H1; dest; subst.
        dest_in.
        all: try (solve_GoodRqRsRule; fail).

        { (* [liGetSRqUpDownM] *)
          apply subtreeChildrenIndsOf_parentIdxOf in H3; [|apply tree2Topo_WfDTree].
          pose proof (tree2Topo_li_child_li_l1 _ _ _ (tl_In _ _ H0) H3).
          rewrite <-msi_indices in H1.

          rule_rqud; eapply rqUpDownRule_RqFwdRule; eauto.

          (** [RqUpDownSound] *)
          red; simpl; intros; dest.
          apply subtreeChildrenIndsOf_parentIdxOf in H4; [|apply tree2Topo_WfDTree].
          repeat ssplit; [discriminate| |intuition auto].
          repeat constructor; try assumption.
        }

        { (* [liGetMRqUpDownM] *)
          apply subtreeChildrenIndsOf_parentIdxOf in H3; [|apply tree2Topo_WfDTree].
          pose proof (tree2Topo_li_child_li_l1 _ _ _ (tl_In _ _ H0) H3).
          rewrite <-msi_indices in H1.

          rule_rqud; eapply rqUpDownRule_RqFwdRule; eauto.

          (** [RqUpDownSound] *)
          red; simpl; intros; dest.
          apply subtreeChildrenIndsOf_parentIdxOf in H4; [|apply tree2Topo_WfDTree].
          repeat ssplit; [discriminate| |intuition auto].
          repeat constructor; try assumption.
        }

        { (* [liGetMRqUpDownS] *)
          apply subtreeChildrenIndsOf_parentIdxOf in H3; [|apply tree2Topo_WfDTree].
          pose proof (tree2Topo_li_child_li_l1 _ _ _ (tl_In _ _ H0) H3).
          rewrite <-msi_indices in H1.

          rule_rqud; eapply rqUpDownRule_RqFwdRule; eauto.

          (** [RqUpDownSound] *)
          red; simpl; intros; dest.
          repeat ssplit.
          { assumption. }
          { apply Forall_forall; intros.
            apply in_remove in H9.
            apply H4 in H9.
            eapply subtreeChildrenIndsOf_parentIdxOf; eauto.
          }
          { apply remove_In. }
        }
      }

      { (* [liDownSRqDownDownM] *)
        rule_rqdd.
        eapply rqDownDownRule_RqFwdRule; eauto.
        (** [RqDownDownSound] *)
        red; simpl; intros; dest.
        repeat ssplit; [discriminate|].
        repeat constructor.
        eapply subtreeChildrenIndsOf_parentIdxOf; eauto.
      }

      { (* [liGetMRsDownRqDownDirS] *)
        rule_rsrq; eapply rsDownRqDownRule_RsDownRqDownRule; eauto.
        (** [RsDownRqDownSound] *)
        red; simpl; intros; dest.
        red in H1.
        unfold getUpLockIdxBackI, getUpLockIdxBack in *.
        destruct (orq@[upRq]) as [rqiu|]; simpl in *; auto.
        destruct H1 as [rcidx [rqUp ?]]; dest.
        pose proof (tree2Topo_li_child_li_l1 _ _ _ (tl_In _ _ H0) H1).
        rewrite <-msi_indices in H9.
        intros; rewrite H11 in *.
        repeat ssplit.
        { assumption. }
        { apply Forall_forall; intros.
          apply in_remove in H12.
          apply H3 in H12.
          eapply subtreeChildrenIndsOf_parentIdxOf; eauto.
        }
        { exists rcidx, rqUp.
          repeat split; try assumption.
        }
      }

      { (* [liDownIRqDownDownDirS] *)
        rule_rqdd.
        eapply rqDownDownRule_RqFwdRule; eauto.
        (** [RqDownDownSound] *)
        red; simpl; intros; dest.
        repeat ssplit; [assumption|].
        apply Forall_forall; intros.
        apply H2 in H4.
        eapply subtreeChildrenIndsOf_parentIdxOf; eauto.
      }

      { (* [liDownIRqDownDownDirM] *)
        rule_rqdd.
        eapply rqDownDownRule_RqFwdRule; eauto.
        (** [RqDownDownSound] *)
        red; simpl; intros; dest.
        repeat ssplit; [discriminate|].
        repeat constructor.
        eapply subtreeChildrenIndsOf_parentIdxOf; eauto.
      }

      { (* [liDownIRqDownDownDirMS] *)
        rule_rqdd.
        eapply rqDownDownRule_RqFwdRule; eauto.
        (** [RqDownDownSound] *)
        red; simpl; intros; dest.
        repeat ssplit; [assumption|].
        apply Forall_forall; intros.
        apply H2 in H4.
        eapply subtreeChildrenIndsOf_parentIdxOf; eauto.
      }

      { (* [liBInvRqS] *)
        rule_rqsd.
        eapply rqUpDownRuleS_RqFwdRule; eauto.
        (** [RqUpDownSoundS] *)
        red; simpl; intros; dest.
        repeat ssplit.
        { assumption. }
        { apply Forall_forall; intros.
          apply H2 in H4.
          eapply subtreeChildrenIndsOf_parentIdxOf; eauto.
        }
      }

      { (* [liBInvRqM] *)
        rule_rqsd.
        eapply rqUpDownRuleS_RqFwdRule; eauto.
        (** [RqUpDownSoundS] *)
        red; simpl; intros; dest.
        repeat ssplit.
        { discriminate. }
        { apply Forall_forall; intros.
          dest_in.
          eapply subtreeChildrenIndsOf_parentIdxOf; eauto.
        }
      }

    - (** L1 caches *)
      apply Forall_forall; intros.
      apply in_map_iff in H.
      destruct H as [oidx [? ?]]; subst.
      red; simpl.

      (* pre-register a fact: an L1 cache always has a parent *)
      pose proof (c_li_l1_indices_has_parent
                    Htr _ _ (in_or_app _ _ _ (or_intror H0))).
      destruct H as [pidx ?].

      repeat
        match goal with
        | |- Forall _ (_ ++ _) => apply Forall_app
        | |- Forall _ (_ :: _) => constructor
        | |- Forall _ nil => constructor
        end.
      all: try (solve_GoodRqRsRule; fail).
  Qed.

  Ltac exfalso_RqToUpRule_unfold ::= repeat autounfold with MsiRules in *.
  Ltac exfalso_RsToUpRule_unfold ::= repeat autounfold with MsiRules in *.
  Ltac disc_rule_custom ::= disc_msi_obj_invs.

  Lemma msi_RqUpRsUpOkSys: RqUpRsUpOkSys topo impl (MsiObjInvs topo).
  Proof. (* SKIP_PROOF_ON
    repeat
      match goal with
      | |- RqUpRsUpOkSys _ _ _ => red
      | |- Forall _ _ => simpl; constructor; simpl
      | |- Forall _ (_ ++ _) => apply Forall_app
      end.

    - (** The main memory: no RqUp rules *)
      red; intros.
      simpl in H; unfold liRulesFromChildren in H.
      apply concat_In in H; dest.
      apply in_map_iff in H; dest; subst.
      dest_in.
      all: try (exfalso_RqToUpRule; fail).

    - (** Li cache *)
      apply Forall_forall; intros.
      apply in_map_iff in H.
      destruct H as [oidx [? ?]]; subst.
      red; intros.

      simpl in H; apply in_app_or in H; destruct H;
        [unfold liRulesFromChildren in H;
         apply concat_In in H; dest;
         apply in_map_iff in H; dest; subst;
         dest_in|dest_in].
      all: try (exfalso_RqToUpRule; fail).

      + simpl in H2; apply in_app_or in H2; destruct H2;
          [unfold liRulesFromChildren in H;
           apply concat_In in H; dest;
           apply in_map_iff in H; dest; subst;
           dest_in|dest_in].
        all: try (exfalso_RsToUpRule; fail).
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; auto.
          all: try (destruct H17; dest; try solve [congruence|solve_msi]).
        }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; try solve_msi.
          f_equal; apply M.add_remove_comm; discriminate.
        }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; try solve_msi.
          f_equal; apply M.add_remove_comm; discriminate.
        }
        { clear; solve_rule_conds_ex; try solve_msi.
          f_equal; apply M.add_remove_comm; discriminate.
        }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }

      + simpl in H2; apply in_app_or in H2; destruct H2;
          [unfold liRulesFromChildren in H;
           apply concat_In in H; dest;
           apply in_map_iff in H; dest; subst;
           dest_in|dest_in].
        all: try (exfalso_RsToUpRule; fail).

        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex.
          all: try (destruct H17; dest; try solve [congruence|solve_msi]).
        }
        { clear; solve_rule_conds_ex.
          all: try (destruct H17; dest; try solve [congruence|solve_msi]).
        }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; try solve_msi.
          f_equal; apply M.add_remove_comm; discriminate.
        }
        { clear; solve_rule_conds_ex; try solve_msi. }
        { clear; solve_rule_conds_ex; try solve_msi.
          f_equal; apply M.add_remove_comm; discriminate.
        }
        { clear; solve_rule_conds_ex; try solve_msi.
          f_equal; apply M.add_remove_comm; discriminate.
        }
        { clear; solve_rule_conds_ex; try solve_msi. }
        { clear; solve_rule_conds_ex; try solve_msi. }

      + simpl in H2; apply in_app_or in H2; destruct H2;
          [unfold liRulesFromChildren in H;
           apply concat_In in H; dest;
           apply in_map_iff in H; dest; subst;
           dest_in|dest_in].
        all: try (exfalso_RsToUpRule; fail).

        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_const; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_const; try solve_msi.
          all: rewrite invalidate_I; solve_msi.
        }
        { clear; solve_rule_conds_const; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }

      + simpl in H2; apply in_app_or in H2; destruct H2;
          [unfold liRulesFromChildren in H;
           apply concat_In in H; dest;
           apply in_map_iff in H; dest; subst;
           dest_in|dest_in].
        all: try (exfalso_RsToUpRule; fail).

        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_const; try intuition solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_const; try intuition solve_msi.
          rewrite invalidate_I; [|solve_msi].
          intuition solve_msi.
        }
        { clear; solve_rule_conds_const; try intuition solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; try intuition solve_msi. }
        { clear; solve_rule_conds_ex; try intuition solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }
        { clear; solve_rule_conds_ex; solve_msi. }

    - (** L1 cache *)
      apply Forall_forall; intros.
      apply in_map_iff in H.
      destruct H as [oidx [? ?]]; subst.
      red; intros.

      phide H2; dest_in.
      all: try (exfalso_RqToUpRule; fail).

      + preveal H4; dest_in.
        all: try (exfalso_RsToUpRule; fail).
        { clear; solve_rule_conds_const; solve_msi. }
        { clear; solve_rule_conds_const; auto. }
        { clear; solve_rule_conds_const; auto. }

      + preveal H4; dest_in.
        all: try (exfalso_RsToUpRule; fail).
        { clear; solve_rule_conds_const. }
        { clear; solve_rule_conds_const; solve_msi. }
        { clear; solve_rule_conds_const; solve_msi. }

      + preveal H4; dest_in.
        all: try (exfalso_RsToUpRule; fail).
        { clear; solve_rule_conds_const; try solve_msi. }
        { clear; solve_rule_conds_const.
          all: rewrite invalidate_I; solve_msi.
        }
        { clear; solve_rule_conds_const; try solve_msi. }

      + preveal H4; dest_in.
        all: try (exfalso_RsToUpRule; fail).
        { clear; solve_rule_conds_const; try solve_msi. }
        { clear; solve_rule_conds_const.
          rewrite invalidate_I; solve_msi.
        }
        { clear; solve_rule_conds_const.
          rewrite invalidate_I; solve_msi.
        }

        END_SKIP_PROOF_ON *) admit.
  Qed.

  Lemma msi_GoodExtRssSys: GoodExtRssSys impl.
  Proof. (* SKIP_PROOF_ON
    red; simpl.
    constructor; [|apply Forall_app].
    - (** the main memory *)
      red; simpl.
      apply Forall_forall; intros.
      unfold memRulesFromChildren in H.
      apply concat_In in H; dest.
      apply in_map_iff in H; dest; subst.
      dest_in.
      all: try (red; simpl; disc_rule_conds_ex; solve_GoodExtRssSys; fail).

    - (** Li cache *)
      apply Forall_forall; intros.
      apply in_map_iff in H.
      destruct H as [oidx [? ?]]; subst.
      red; simpl.
      apply Forall_app.

      + apply Forall_forall; intros.
        unfold liRulesFromChildren in H.
        apply concat_In in H; dest.
        apply in_map_iff in H; dest; subst.
        dest_in.
        all: try (red; simpl; disc_rule_conds_ex; solve_GoodExtRssSys; fail).
        { (* [liGetMRqUpDownS] *)
          red; simpl; disc_rule_conds_ex.
          apply in_map_iff in H3; dest; subst.
          apply in_remove in H12.
          apply H5 in H12.
          simpl in *; solve_GoodExtRssSys.
        }

      + repeat constructor.
        all: try (red; simpl; disc_rule_conds_ex; solve_GoodExtRssSys; fail).
        { (* [liGetMRsDownRqDownDirS] *)
          red; simpl; disc_rule_conds_ex.
          apply in_map_iff in H2; dest; subst.
          apply in_remove in H5.
          apply H11 in H5.
          simpl in *; solve_GoodExtRssSys.
        }
        { (* [liDownIRqDownDownDirS] *)
          red; simpl; disc_rule_conds_ex.
          apply in_map_iff in H2; dest; subst.
          apply H4 in H7.
          simpl in *; solve_GoodExtRssSys.
        }
        { (* [liDownIRqDownDownDirMS] *)
          red; simpl; disc_rule_conds_ex.
          apply in_map_iff in H2; dest; subst.
          apply H4 in H7.
          simpl in *; solve_GoodExtRssSys.
        }
        { (* [liBInvRqS] *)
          red; simpl; disc_rule_conds_ex.
          apply in_map_iff in H2; dest; subst.
          apply H6 in H8.
          simpl in *; solve_GoodExtRssSys.
        }

    - (** L1 cache *)
      apply Forall_forall; intros.
      apply in_map_iff in H.
      destruct H as [oidx [? ?]]; subst.
      red; simpl.
      repeat constructor.
      all: try (red; simpl; disc_rule_conds_ex; solve_GoodExtRssSys; fail).

      END_SKIP_PROOF_ON *) admit.
  Qed.

  Lemma msi_GoodRqRsInterfSys: GoodRqRsInterfSys topo impl (MsiObjInvs topo).
  Proof.
    split.
    - apply msi_RqUpRsUpOkSys.
    - apply msi_GoodExtRssSys.
  Qed.

  Lemma msi_RqRsSys: RqRsSys topo impl (MsiObjInvs topo).
  Proof.
    red; repeat ssplit.
    - apply msi_RqRsDTree.
    - apply msi_GoodRqRsSys.
    - apply msi_GoodRqRsInterfSys.
  Qed.

End System.

#[global] Hint Resolve msi_GoodORqsInit msi_WfDTree msi_RqRsDTree msi_RqRsSys.

author: mit-plv

repo: hemiola

save_path: github-repos/coq/mit-plv-hemiola


text:
Require Import compcert.lib.Axioms.
Require Import compcert.lib.Maps.

Require Import VST.concurrency.sepcomp.
From mathcomp.ssreflect Require Import ssreflect ssrbool ssrnat ssrfun eqtype seq fintype finfun.
Set Implicit Arguments.

Require Import Coq.ZArith.ZArith.

Require Import VST.concurrency.permissions.
Require Import compcert.common.Memory. (*for Mem.perm_order'' *)
Require Import VST.concurrency.bounded_maps.
Require Import VST.concurrency.permissions.

Require Import VST.sepcomp.semantics_lemmas.
Require Import Coqlib.
Require Import VST.veric.Clight_new.
Require Import VST.veric.Clightnew_coop.

Require Import Coq.Logic.FunctionalExtensionality.

Lemma CLight_Deterministic: forall ge c m c1 m1 c2 m2,
    veric.Clight_new.cl_step ge c m c2 m2 ->
    veric.Clight_new.cl_step ge c m c1 m1 ->
    c1 = c2 /\ m1 = m2.
Proof. intros.
       specialize (cl_corestep_fun _ _ _ _ _ _ _ H H0); intros X; inversion X; subst. split; trivial.
Qed.

Definition bnd_from_init m := bounded_maps.bounded_map (snd (getMaxPerm m)) /\ (Mem.mem_access m).1 = fun z k => None.

Lemma mem_storebytes_counded_init:
  forall m m' b ofs bytes,
    bnd_from_init m ->
    Mem.storebytes m b ofs bytes = Some m' ->
    bnd_from_init m'.
Proof.
  intros ? ? ? ? ? H0 H.
  destruct H0; split.
  unfold getMaxPerm in *. erewrite Mem.storebytes_access; eauto.
  erewrite Mem.storebytes_access; eauto.
Qed.

Lemma mem_alloc_bounded_init:
  forall m lo hi m1 b,
    bnd_from_init m ->
    Mem.alloc m lo hi = (m1, b) ->
    bnd_from_init m1.
Proof.
  { intros ? ? ? ? ? H0 H.
    Transparent Mem.alloc. unfold Mem.alloc in H. Opaque Mem.alloc.
    inversion H; clear H; subst.
    destruct H0; split; simpl in *; trivial.
    red; intros. red in H.
    rewrite (PTree.gmap1 (fun f : Z -> perm_kind -> option permission => f^~ Max)
                         p (PTree.set (Mem.nextblock m)
                                      (fun (ofs : Z) (_ : perm_kind) => if zle lo ofs && zlt ofs hi then Some Freeable else None)
                                      (Mem.mem_access m).2)) in H1.
    unfold option_map in H1.
    rewrite PTree.gsspec in H1.
    destruct (peq p (Mem.nextblock m)); subst.
    { inversion H1; clear H1; subst. clear H0 H. red.
      exists hi, lo; split; intros.
      { destruct (zle lo p); destruct (zlt p hi); simpl; trivial; omega. }
      { destruct (zle lo p); destruct (zlt p hi); simpl; trivial; omega. } }
    { apply (H p); clear H0. rewrite PTree.gmap1. apply H1. } }
Qed.

Lemma mem_free_bounded_init:
  forall m lo hi m' b,
    bnd_from_init m ->
    Mem.free m b lo hi = Some m' ->
    bnd_from_init m'.
Proof.
  intros ? ? ? ? ? H0 Heqq.
  Transparent Mem.free. unfold Mem.free in Heqq. Opaque Mem.free.
  destruct (Mem.range_perm_dec m b lo hi Cur Freeable); try discriminate.
  inversion Heqq; clear Heqq; subst.
  destruct H0 as [? INI]; split.
  intros p f F.  simpl.
  destruct (peq p b); subst.
  { simpl in F. rewrite PTree.gmap1 in F. unfold option_map in F. rewrite PTree.gss in F. inversion F; clear F; subst.
    specialize (H b).
    remember (((getMaxPerm m).2) ! b) as g. destruct g; symmetry in Heqg.
    { assert (Some o = Some o) by trivial. specialize (H _ H0); clear H0. rename o into g.
      destruct H as [HI [LO [HHi HLo]]]. unfold getMaxPerm in Heqg. unfold PMap.get. simpl in *.
      rewrite PTree.gmap1 in Heqg. unfold option_map in Heqg. rewrite INI.
      destruct (((Mem.mem_access m).2) ! b); try discriminate. inversion Heqg; clear Heqg; subst.
      exists  HI, LO; split; intros.
      { destruct (zle lo p); destruct (zlt p hi); simpl; trivial; eauto. }
      { destruct (zle lo p); destruct (zlt p hi); simpl; trivial; eauto. } }
    { clear H. unfold getMaxPerm in Heqg.
      destruct (zlt lo hi).
      { assert (A: lo <= lo < hi) by omega. specialize (r _ A).
        apply Mem.perm_max in r. unfold Mem.perm, PMap.get in r.
        rewrite PTree.gmap1 in Heqg. unfold option_map in Heqg.
        remember (((Mem.mem_access m).2) ! b) as q. destruct q; simpl in *. discriminate.
        rewrite INI in r. inversion r. }
      { simpl in Heqg. rewrite PTree.gmap1 in Heqg. unfold option_map in Heqg. unfold PMap.get.
        remember (((Mem.mem_access m).2) ! b) as w. destruct w; try discriminate. clear Heqg.
        rewrite INI.
        exists lo, lo; split; intros.
        { destruct (zle lo p); destruct (zlt p hi); simpl; trivial. }
        { destruct (zle lo p); destruct (zlt p hi); simpl; trivial. } } } }
  { apply (H p). unfold getMaxPerm in *; simpl in *.
    rewrite PTree.gmap1 in F. rewrite PTree.gmap1. unfold option_map in *.
    rewrite PTree.gso in F; trivial. }
  simpl; trivial.
Qed.

Lemma mem_drop_perm_bounded_init:
  forall m b lo hi P m',
    bnd_from_init m ->
    Mem.drop_perm m b lo hi P = Some m' ->
    bnd_from_init m'.
Proof.
  intros ? ? ? ? ? ? H0 Heqq.
  Transparent Mem.drop_perm. unfold Mem.drop_perm in Heqq. Opaque Mem.drop_perm.
  destruct (Mem.range_perm_dec m b lo hi Cur Freeable); try discriminate.
  inversion Heqq; clear Heqq; subst.
  destruct H0 as [? INI]; split.
  - intros p f F.  simpl.
    destruct (peq p b); subst.
    { simpl in F.
      rewrite PTree.gmap1 in F.
      unfold option_map in F.
      rewrite PTree.gss in F.
      inversion F; clear F; subst.
      specialize (H b).
      remember (((getMaxPerm m).2) ! b) as g. destruct g; symmetry in Heqg.
      { assert (Some o = Some o) by trivial. specialize (H _ H0); clear H0. rename o into g.
      destruct H as [HI [LO [HHi HLo]]]. unfold getMaxPerm in Heqg. unfold PMap.get. simpl in *.
      rewrite PTree.gmap1 in Heqg. unfold option_map in Heqg. rewrite INI.
      destruct (((Mem.mem_access m).2) ! b); try discriminate. inversion Heqg; clear Heqg; subst.
      exists  (Z.max HI hi), (Z.min LO lo); split; intros.
      { destruct (zle lo p); destruct (zlt p hi); simpl; trivial; eauto.
        - move : H=> /Z.gt_lt_iff /Z.max_lub_lt_iff [] ? ?.
          xomega.
        - move : H=> /Z.gt_lt_iff /Z.max_lub_lt_iff [] /Z.gt_lt_iff /HHi //.
        - move : H=> /Z.gt_lt_iff /Z.max_lub_lt_iff [] /Z.gt_lt_iff /HHi //.
        - move : H=> /Z.gt_lt_iff /Z.max_lub_lt_iff [] /Z.gt_lt_iff /HHi //.
      }
      { destruct (zle lo p); destruct (zlt p hi); simpl; trivial; eauto.
        - move : H=> /Z.min_glb_lt_iff [] ? ?.
          xomega.
        - move : H=> /Z.min_glb_lt_iff [] ? ?.
          omega.
        - move : H=> /Z.min_glb_lt_iff [] /HLo //.
        - move : H=> /Z.min_glb_lt_iff [] /HLo //.
      } }
    { clear H. unfold getMaxPerm in Heqg.
      destruct (zlt lo hi).
      { assert (A: lo <= lo < hi) by omega. specialize (r _ A).
        apply Mem.perm_max in r. unfold Mem.perm, PMap.get in r.
        rewrite PTree.gmap1 in Heqg. unfold option_map in Heqg.
        remember (((Mem.mem_access m).2) ! b) as q. destruct q; simpl in *. discriminate.
        rewrite INI in r. inversion r. }
      { simpl in Heqg. rewrite PTree.gmap1 in Heqg. unfold option_map in Heqg. unfold PMap.get.
        remember (((Mem.mem_access m).2) ! b) as w. destruct w; try discriminate. clear Heqg.
        rewrite INI.
        exists lo, lo; split; intros.
        { destruct (zle lo p); destruct (zlt p hi); simpl; trivial. xomega. }
        { destruct (zle lo p); destruct (zlt p hi); simpl; trivial. xomega.  } } } }
  { apply (H p). unfold getMaxPerm in *; simpl in *.
    rewrite PTree.gmap1 in F. rewrite PTree.gmap1. unfold option_map in *.
    rewrite PTree.gso in F; trivial. }
  simpl; trivial.
Qed.

Lemma mem_free_list_bounded_init:
  forall m l m',
    bnd_from_init m ->
    Mem.free_list m l = Some m' ->
    bnd_from_init m'.
Proof.
  intros ? ? ? H0 H.
  { generalize dependent m'. generalize dependent m. induction l; intros.
    { inversion H; clear H; subst. trivial. }
    { destruct a as [[b lo] hi]. simpl in H. remember (Mem.free m b lo hi) as q; symmetry in Heqq.
      destruct q; try discriminate. apply (IHl m0); trivial. clear H IHl m'.
      rename m0 into m'.
      eapply mem_free_bounded_init; eauto.
  } }
Qed.

Lemma preserve_bnd: memstep_preserve (fun m m' => bnd_from_init m -> bnd_from_init m').
Proof.
  econstructor; intros; eauto.
  induction H; intros.
  - eapply mem_storebytes_counded_init; eauto.
  - eapply mem_alloc_bounded_init; eauto.
  - eapply mem_free_list_bounded_init; eauto.
  - eauto.
Qed.

Lemma CLight_step_mem_bound' ge c m c' m':
  veric.Clight_new.cl_step ge c m c' m' -> bnd_from_init m -> bnd_from_init m'.
Proof.
  intros.
  apply (memsem_preserves (CLN_memsem ge) _ preserve_bnd _ _ _ _ H H0).
Qed.

(*This proof is already in juicy_machine.
 * move it to a more general position.*)
Lemma Mem_canonical_useful: forall m loc k,
    fst (Mem.mem_access m) loc k = None.
Proof. intros. destruct m; simpl in *.
       unfold PMap.get in nextblock_noaccess.
       pose (b:= Pos.max (TreeMaxIndex (snd mem_access) + 1 )  nextblock).
       assert (H1:  ~ Plt b nextblock).
       { intros H. assert (HH:= Pos.le_max_r (TreeMaxIndex (snd mem_access) + 1) nextblock).
         clear - H HH. unfold Pos.le in HH. unfold Plt in H.
         apply HH. eapply Pos.compare_gt_iff.
         auto. }
       assert (H2 :( b > (TreeMaxIndex (snd mem_access)))%positive ).
       { assert (HH:= Pos.le_max_l (TreeMaxIndex (snd mem_access) + 1) nextblock).
         apply Pos.lt_gt. eapply Pos.lt_le_trans; eauto.
         xomega. }
       specialize (nextblock_noaccess b loc k H1).
       apply max_works in H2. rewrite H2 in nextblock_noaccess.
       assumption.
Qed.

Lemma mem_bound_init_mem_bound:
  forall m,
    bounded_maps.bounded_map (snd (getMaxPerm m)) <->
    bnd_from_init m.
Proof.
  repeat (split; intros) ; eauto.
  - extensionality x;
    extensionality y;
    eapply Mem_canonical_useful.
  - destruct H; auto.
Qed.

Lemma CLight_step_mem_bound ge c m c' m':
  veric.Clight_new.cl_step ge c m c' m' ->
  bounded_maps.bounded_map (snd (getMaxPerm m)) ->
  bounded_maps.bounded_map (snd (getMaxPerm m')).
Proof.
  intros.
  eapply CLight_step_mem_bound' in H;
  apply mem_bound_init_mem_bound; eauto.
Qed.

Definition bounded_mem (m: mem) := bounded_maps.bounded_map (snd (getMaxPerm m)) .

Lemma mem_alloc_bounded:
  forall m lo hi m1 b,
    bounded_mem m ->
    Mem.alloc m lo hi = (m1, b) ->
    bounded_mem m1.
Proof.
  intros m lo hi m1 b H H0.
  apply mem_bound_init_mem_bound; eauto.
  eapply mem_alloc_bounded_init; eauto.
  apply mem_bound_init_mem_bound; eauto.
Qed.

Lemma drop_perm_bounded:
  forall m b lo hi P m',
    bounded_mem m ->
    Mem.drop_perm m b lo hi P = Some m' ->
    bounded_mem m'.
Proof.
  intros m b lo hi P m' H H0.
  apply mem_bound_init_mem_bound; eauto.
  eapply mem_drop_perm_bounded_init ; eauto.
  apply mem_bound_init_mem_bound; eauto.
Qed.

Lemma store_bounded:
  forall Mint32 m b ofs v m',
    bounded_mem m ->
    Mem.store Mint32 m b ofs v = Some m' ->
    bounded_mem m'.
Proof.
  intros Mint m b ofs v m' H H0.
  eapply mem_bound_init_mem_bound; eauto.
  eapply mem_storebytes_counded_init; eauto.
  - eapply mem_bound_init_mem_bound; eauto.
  - eapply Mem.store_storebytes; eauto.
Qed.

Lemma bounded_getMaxPerm:
  forall m p Hlt,
    @bounded_mem m ->
    @bounded_mem (@restrPermMap p m Hlt).
Proof.
  intros ? ? ? H b f.
  rewrite /restrPermMap /= PTree.gmap1 PTree.gmap.
  move: (H b f).
  rewrite /getMaxPerm /= PTree.gmap1.
  destruct (((Mem.mem_access m).2) ! b)=> //.
Qed.

Lemma store_init_data_bounded:
  forall F V ge m b ofs data m',
    bounded_mem m ->
    @Globalenvs.Genv.store_init_data F V ge m b ofs data = Some m' ->
    bounded_mem m'.
Proof.
  intros.
  move: H0.
  destruct data; simpl;
  try eapply store_bounded; eauto.
  - intros HH; inversion HH.
    subst; auto.
  - destruct ( Globalenvs.Genv.find_symbol ge i);
    try solve[intros HH; inversion HH];
    eapply store_bounded; eauto.
Qed.

Lemma store_init_data_list_bounded:
  forall F V ge m b ofs B m',
    bounded_mem m ->
    @Globalenvs.Genv.store_init_data_list F V ge m b ofs B = Some m' ->
    bounded_mem m'.
Proof.
  intros.
  move: m' ofs b m H H0.
  induction B.
  - intros; inversion H0; subst; auto.
  - intros; simpl in H0.
    destruct (Globalenvs.Genv.store_init_data ge m b ofs a) eqn:STORE_INIT;
      try solve[inversion H0].
    eapply IHB; try apply H0.
    eapply store_init_data_bounded; eauto.
Qed.

Lemma store_zeros_init_data_bounded:
  forall m b ofs a m',
    bounded_mem m ->
    Globalenvs.store_zeros m b ofs a = Some m' ->
    bounded_mem m'.
Proof.
  intros.
  destruct (zle a 0) eqn:AA.
  - rewrite Globalenvs.store_zeros_equation in H0.
    rewrite AA in H0; inversion H0; subst; auto.
  - assert (exists n, Z.of_nat n = a).
    { exists (nat_of_Z a).
      apply nat_of_Z_eq. omega. }
    destruct H1 as [n H1].
    subst a.
    clear g AA.
    move: n m b ofs m' H H0.
    induction n.
    + intros.
      rewrite Globalenvs.store_zeros_equation in H0.
      rewrite Nat2Z.inj_0 in H0.
      destruct (zle 0 0); try omega.
      inversion H0; subst; assumption.
    + intros.
      rewrite Globalenvs.store_zeros_equation in H0.
      destruct (zle (Z.of_nat n.+1) 0).
      { rewrite Nat2Z.inj_succ in l.
        assert (HH:=coqlib4.Z_of_nat_ge_O n).
        clear - l HH.
        xomega.
      }
      destruct ( Mem.store AST.Mint8unsigned m b ofs Values.Vzero) eqn:STORE';
        try solve[inversion H0].
      replace (Z.of_nat n.+1 - 1) with (Z.of_nat n) in H0 by xomega.
      eapply IHn; try eapply H0.
      eapply store_bounded; eauto.
Qed.

Lemma alloc_global_bounded:
  forall F V ge m m' a,
    @bounded_mem m ->
    @Globalenvs.Genv.alloc_global F V ge m a = Some m' ->
    @bounded_mem m'.
Proof.
  move => ? ? ge m m' [] ? a BND.
  rewrite /Globalenvs.Genv.alloc_global.
  destruct a.
  - destruct (Mem.alloc m 0 1) eqn:ALLOC; intros DROP;
    try solve[inversion DROP].
    eapply drop_perm_bounded; try eapply DROP.
    eapply mem_alloc_bounded; eauto.
  - remember (AST.init_data_list_size (AST.gvar_init v)) as  A; clear HeqA.
    destruct (Mem.alloc m 0 A) eqn:ALLOC.
    destruct (Globalenvs.store_zeros m0 b 0 ) eqn:STORE;
      try solve[intros HH; inversion HH ].
    remember ((AST.gvar_init v)) as  B; clear HeqB.
    destruct (Globalenvs.Genv.store_init_data_list ge m1 b 0 B) eqn:STORE_INIT;
      try solve[intros HH; inversion HH ].
    intros DROP.
    eapply drop_perm_bounded; try eapply DROP. clear DROP.
    eapply store_init_data_list_bounded;
      try eapply STORE_INIT.
    eapply store_zeros_init_data_bounded; try eapply STORE.
    eapply mem_alloc_bounded; eauto.
Qed.

author: PrincetonUniversity

repo: VST


text:
(** * Postscript *)

(** Congratulations: We've made it to the end! *)

(* ################################################################# *)
(** * Looking Back *)

(** We've covered quite a bit of ground so far.  Here's a quick review...

   - _Functional programming_:
          - "declarative" programming style (recursion over persistent
            data structures, rather than looping over mutable arrays
            or pointer structures)
          - higher-order functions
          - polymorphism *)

(**
     - _Logic_, the mathematical basis for software engineering:

               logic                        calculus
        --------------------   ~   ----------------------------
        software engineering       mechanical/civil engineering

          - inductively defined sets and relations
          - inductive proofs
          - proof objects *)

(**
     - _Coq_, an industrial-strength proof assistant
          - functional core language
          - core tactics
          - automation
*)

(* ################################################################# *)
(** * Looking Forward *)

(** If what you've seen so far has whetted your interest, you have two
    choices for further reading in the _Software Foundations_ series:

           - _Programming Language Foundations_ (volume 2, by a set of
             authors similar to this book's) covers material that
             might be found in a graduate course on the theory of
             programming languages, including Hoare logic, operational
             semantics, and type systems.

           - _Verified Functional Algorithms_ (volume 3, by Andrew
             Appel) builds on the themes of functional programming and
             program verification in Coq, addressing a range of topics
             that might be found in a standard data structures course,
             with an eye to formal verification. *)

(* ################################################################# *)
(** * Other sources *)

(** Here are some other good places to learn more...

       - This book includes some optional chapters covering topics
         that you may find useful.  Take a look at the table of contents and the chapter dependency diagram to find
         them.

       - For questions about Coq, the #coq area of Stack
         Overflow (https://stackoverflow.com/questions/tagged/coq)
         is an excellent community resource.

       - Here are some great books on functional programming
            - Learn You a Haskell for Great Good, by Miran Lipovaca
              [Lipovaca 2011].
            - Real World Haskell, by Bryan O'Sullivan, John Goerzen,
              and Don Stewart [O'Sullivan 2008]
            - ...and many other excellent books on Haskell, OCaml,
              Scheme, Racket, Scala, F sharp, etc., etc.

       - And some further resources for Coq:
           - Certified Programming with Dependent Types, by Adam
             Chlipala [Chlipala 2013].
           - Interactive Theorem Proving and Program Development:
             Coq'Art: The Calculus of Inductive Constructions, by Yves
             Bertot and Pierre Casteran [Bertot 2004].

       - If you're interested in real-world applications of formal
         verification to critical software, see the Postscript chapter
         of _Programming Language Foundations_.

       - For applications of Coq in building verified systems, the
         lectures and course materials for the 2017 DeepSpec Summer
         School are a great resource.
         https://deepspec.org/event/dsss17/index.html
*)

author: AKKID

repo: If

save_path: github-repos/coq/AKKID-If


text:
Require Import CompCert.Events.
Require Import CompCert.Smallstep.
Require Import CompCert.Behaviors.
Require Import Common.Definitions.
Require Import Common.Util.
Require Import Common.Memory.
Require Import Common.Blame.
Require Import Common.Linking.
Require Import Common.CompCertExtensions.
Require Import Common.Traces.
Require Import Source.Language.
Require Import Source.GlobalEnv.
Require Import Source.CS.
Require Import Source.PS.
Require Import Lib.Extra.
Require Import Old.Source.CSExtra.
Require Import Old.Source.PSExtra.

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Set Bullet Behavior "Strict Subproofs".

Import Source.

Section Decomposition.
  Variable p c: program.

  Hypothesis wf1 : well_formed_program p.
  Hypothesis wf2 : well_formed_program c.

  Hypothesis linkability: linkable (prog_interface p) (prog_interface c).

  Hypothesis closedness_after_linking:
    closed_program (program_link p c).

  Lemma match_initial_states:
    forall ics,
      CS.initial_state (program_link p c) ics ->
    exists ips,
      PS.initial_state p (prog_interface c) ips /\
      PS.partial_state (prog_interface c) ics ips.
  Proof.
    intros ics Hics_init.
    CS.unfold_states.
    (* case analysis on who has control, then build the partial state *)
    destruct (C \in domm (prog_interface c)) eqn:Htarget;
      exists (PS.partialize (prog_interface c) [CState C, s, mem, k, e, arg]);
      simpl; rewrite Htarget.
    (* context has control *)
    - split.
      + eapply PS.initial_state_intro with (p':=c).
        * reflexivity.
        * assumption.
        * assumption.
        * assumption.
        * assumption.
        * eapply PS.ContextControl; eauto.
        * apply Hics_init.
      + eapply PS.ContextControl; eauto.
    (* program has control *)
    - split.
      + eapply PS.initial_state_intro with (p':=c).
        * reflexivity.
        * assumption.
        * assumption.
        * assumption.
        * assumption.
        * eapply PS.ProgramControl; auto.
          ** PS.simplify_turn.
             unfold negb. rewrite Htarget. auto.
        * apply Hics_init.
      + eapply PS.ProgramControl; auto.
        * PS.simplify_turn.
          unfold negb. rewrite Htarget. auto.
  Qed.

  Lemma match_final_states:
    forall ics ips,
      PS.partial_state (prog_interface c) ics ips ->
      CS.final_state ics ->
      PS.final_state p (prog_interface c) ips.
  Proof.
    intros ics ips Hpartial Hics_final.
    CS.unfold_states.
    (* case analysis on who has control *)
    destruct (C \in domm (prog_interface c)) eqn:Htarget.
    (* context has control *)
    - inversion Hpartial; inversion H; subst.
      + PS.simplify_turn.
        by rewrite Htarget in H6.
      + apply PS.final_state_context.
        PS.simplify_turn. auto.
    (* program has control *)
    - inversion Hpartial; inversion H; subst.
      + eapply PS.final_state_program with (p':=c).
        * reflexivity.
        * assumption.
        * assumption.
        * assumption.
        * PS.simplify_turn. rewrite Htarget. auto.
        * eauto.
        * assumption.
      + PS.simplify_turn.
        rewrite Htarget in H6. discriminate.
  Qed.

  Lemma match_initial_states_by_partialize : forall scs0,
    CS.initial_state (program_link p c) scs0 ->
    PS.initial_state p (prog_interface c) (PS.partialize (prog_interface c) scs0).
  Proof.
    intros scs0 Hini.
    eapply PS.initial_state_intro;
      try reflexivity;
      try assumption.
    unfold CS.initial_state in Hini.
    unfold CS.initial_machine_state in *.
    rewrite <- PS.partialize_correct.
    destruct (prog_main (program_link p c)) as [main |] eqn:Hmain;
      subst;
      easy.
  Qed.

  Lemma lockstep_simulation:
    forall ics t ics',
      CS.kstep (prepare_global_env (program_link p c)) ics t ics' ->
    forall ips,
      PS.partial_state (prog_interface c) ics ips ->
    exists ips',
      PS.kstep p (prog_interface c) (prepare_global_env p) ips t ips' /\
      PS.partial_state (prog_interface c) ics' ips'.
  Proof.
    intros ics t ics' Hstep ips Hpartial.

    (* case analysis on who has control and the executed step *)
    inversion linkability; subst.
    inversion Hpartial; subst;
    inversion Hstep; subst.

    (** program has control **)

    (* epsilon steps *)

    - (* KS_Binop1 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_Binop2 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_BinopEval *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_Seq1 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_Seq2 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_If1 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_If2 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_Arg *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_LocalBuffer *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_Alloc1 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_AllocEval *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_Deref1 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_DerefEval *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_Assign1 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_Assign2 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_AssignEval *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_InitCall *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    - (* KS_InternalCall *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    (* call *)
    - PS.simplify_turn.
      (* case analisys on the target *)
      destruct (C' \in domm (prog_interface c)) eqn:Htarget.
      (* external call *)
      + eexists. split.
        * eapply PS.partial_step with (p':=c); auto.
          ** eassumption.
          ** eapply PS.ProgramControl; auto.
          ** eapply PS.ContextControl; auto.
        * eapply PS.ContextControl; auto.
      (* internal call *)
      + eexists. split.
        * eapply PS.partial_step with (p':=c); auto.
          ** eassumption.
          ** eapply PS.ProgramControl; auto.
          ** eapply PS.ProgramControl; auto.
             *** PS.simplify_turn.
                 unfold negb. rewrite Htarget. auto.
        * eapply PS.ProgramControl; auto.
          ** PS.simplify_turn.
             unfold negb. rewrite Htarget. auto.

    (* internal return (program to program) *)
    - PS.simplify_turn.
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * econstructor; eauto.
      + econstructor; auto.

    (* external return *)
    - PS.simplify_turn.
      (* case analisys on the target *)
      destruct (C' \in domm (prog_interface c)) eqn:Htarget.
      (* external return *)
      + eexists. split.
        * eapply PS.partial_step with (p':=c); auto.
          ** eassumption.
          ** eapply PS.ProgramControl; auto.
          ** eapply PS.ContextControl; auto.
        * eapply PS.ContextControl; auto.
      (* internal return *)
      + eexists. split.
        * eapply PS.partial_step with (p':=c); auto.
          ** eassumption.
          ** eapply PS.ProgramControl; auto.
          ** eapply PS.ProgramControl; auto.
             *** PS.simplify_turn.
                 unfold negb. rewrite Htarget. auto.
        * eapply PS.ProgramControl; auto.
          ** PS.simplify_turn.
             unfold negb. rewrite Htarget. auto.

    (** context has control **)

    - (* KS_Binop1 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    - (* KS_Binop2 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    - (* KS_BinopEval *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    - (* KS_Seq1 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    - (* KS_Seq2 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    - (* KS_If1 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    - (* KS_If2 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    - (* KS_Arg *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    - (* KS_LocalBuffer *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    - (* KS_Alloc1 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    - (* KS_AllocEval *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
          ** PS.simplify_turn.
             match goal with (* TODO: clean up. *)
             | |- ?FMEM = ?FMEM' =>
               change FMEM with (to_partial_memory mem (domm (prog_interface c)));
               change FMEM' with (to_partial_memory mem' (domm (prog_interface c)))
             end.
             erewrite <- context_allocation_in_partialized_memory; eauto.
      + eapply PS.ContextControl; eauto.
        * PS.simplify_turn.
          match goal with (* TODO: clean up. *)
          | |- ?FMEM = ?FMEM' =>
            change FMEM with (to_partial_memory mem (domm (prog_interface c)));
            change FMEM' with (to_partial_memory mem' (domm (prog_interface c)))
          end.
          erewrite <- context_allocation_in_partialized_memory; eauto.

    - (* KS_Deref1 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    - (* KS_DerefEval *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    - (* KS_Assign1 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    - (* KS_Assign2 *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    - (* KS_AssignEval *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
          ** PS.simplify_turn.
             match goal with (* TODO: clean up. *)
             | |- ?FMEM = ?FMEM' =>
               change FMEM with (to_partial_memory mem (domm (prog_interface c)));
               change FMEM' with (to_partial_memory mem' (domm (prog_interface c)))
             end.
             erewrite <- context_store_in_partialized_memory; eauto.
      + eapply PS.ContextControl; eauto.
        * PS.simplify_turn.
          match goal with (* TODO: clean up. *)
          | |- ?FMEM = ?FMEM' =>
            change FMEM with (to_partial_memory mem (domm (prog_interface c)));
            change FMEM' with (to_partial_memory mem' (domm (prog_interface c)))
          end.
          erewrite <- context_store_in_partialized_memory; eauto.

    - (* KS_InitCall *)
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    (* internal call *)
    - PS.simplify_turn.
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    (* external call *)
    - PS.simplify_turn.
      (* case analysis on the target *)
      destruct (C' \in domm (prog_interface c)) eqn:Htarget.
      (* internal call *)
      + eexists. split.
        * eapply PS.partial_step with (p':=c); auto.
          ** eassumption.
          ** eapply PS.ContextControl; auto.
          ** eapply PS.ContextControl; auto.
        * eapply PS.ContextControl; auto.
      (* external call *)
      + eexists. split.
        * eapply PS.partial_step with (p':=c); auto.
          ** eassumption.
          ** eapply PS.ContextControl; auto.
          ** eapply PS.ProgramControl; auto.
             *** PS.simplify_turn.
                 unfold negb. rewrite Htarget. auto.
        * eapply PS.ProgramControl; auto.
          ** PS.simplify_turn.
             unfold negb. rewrite Htarget. auto.

    (* internal return *)
    - PS.simplify_turn.
      eexists. split.
      + eapply PS.partial_step with (p':=c); eauto.
        * eapply PS.ContextControl; eauto.
      + eapply PS.ContextControl; eauto.

    (* external return *)
    - PS.simplify_turn.
      (* case analysis on the target *)
      destruct (C' \in domm (prog_interface c)) eqn:Htarget.
      (* internal return *)
      + eexists. split.
        * eapply PS.partial_step with (p':=c); auto.
          ** eassumption.
          ** eapply PS.ContextControl; auto.
          ** eapply PS.ContextControl; auto.
        * eapply PS.ContextControl; auto.
      (* external return *)
      + eexists. split.
        * eapply PS.partial_step with (p':=c); auto.
          ** eassumption.
          ** eapply PS.ContextControl; auto.
          ** eapply PS.ProgramControl; auto.
             *** PS.simplify_turn.
                 unfold negb. rewrite Htarget. auto.
        * eapply PS.ProgramControl; auto.
          ** PS.simplify_turn.
             unfold negb. rewrite Htarget. auto.
  Qed.

  Theorem decomposition:
    forward_simulation (CS.sem (program_link p c))
                       (PS.sem p (prog_interface c)).
  Proof.
    eapply forward_simulation_step.
    - apply match_initial_states.
    - apply match_final_states.
    - apply lockstep_simulation.
  Qed.

  Corollary decomposition_with_safe_behavior:
    forall beh,
      program_behaves (CS.sem (program_link p c)) beh ->
      not_wrong beh ->
      program_behaves (PS.sem p (prog_interface c)) beh.
  Proof.
    intros beh.
    eapply forward_simulation_same_safe_behavior; eauto.
    apply decomposition.
  Qed.

  Corollary decomposition_with_refinement:
    forall beh1,
      program_behaves (CS.sem (program_link p c)) beh1 ->
    exists beh2,
      program_behaves (PS.sem p (prog_interface c)) beh2 /\
      behavior_improves beh1 beh2.
  Proof.
    intros beh1 Hbeh1.
    eapply forward_simulation_behavior_improves; eauto.
    apply decomposition.
  Qed.

  Inductive well_defined_components (iface: Program.interface): event -> Prop :=
  | wf_comps_call: forall C1 P arg C2,
      C1 \in domm iface ->
      C2 \in domm iface ->
      well_defined_components iface (ECall C1 P arg C2)
  | wf_comps_ret: forall C1 arg C2,
      C1 \in domm iface ->
      C2 \in domm iface ->
      well_defined_components iface (ERet C1 arg C2).

  Definition well_defined_components_trace (iface : Program.interface) (t : trace) : Prop :=
    forall e, In e t -> well_defined_components iface e.

  (* This follows easily from previous lemmas by a right-side induction on Star. *)
  Lemma initial_star_has_well_defined_components :
    forall sini t sfin,
      initial_state (CS.sem (program_link p c)) sini ->
      Star (CS.sem (program_link p c)) sini t sfin ->
      well_defined_components_trace (unionm (prog_interface p) (prog_interface c)) t.
  Proof.
    move=> sini t sfin Hinitial Hstar e /In_in in_t.
    move: (cprog_main_existence closedness_after_linking).
    case e_main: (prog_main _)=> [mainP|] //= _.
    have := linking_well_formedness wf1 wf2 linkability.
    move/(CS.trace_wf Hstar Hinitial e_main)=> trace_wf.
    have := cprog_closed_interface closedness_after_linking.
    move/(well_formed_trace_int trace_wf)/seq.allP/(_ _ in_t).
    rewrite /declared_event_comps.
    by case: e {in_t}=> /= [????|???] /andP [??]; constructor.
  Qed.

  Lemma ub_behavior_has_well_defined_components:
    forall t,
      program_behaves (CS.sem (program_link p c)) (Goes_wrong t) ->
    forall e,
      In e t ->
      well_defined_components (prog_interface (program_link p c)) e.
  Proof.
    intros t Hprbeh e HIn.
    inversion Hprbeh as [sini tmp Hini Hstbeh |]; subst;
      last easy.
    inversion Hstbeh as [| | | tmp sfin HStar HNostep Hfinalst]; subst.
    eapply initial_star_has_well_defined_components; eassumption.
  Qed.

  Lemma ub_blaming t :
    program_behaves (CS.sem (program_link p c)) (Goes_wrong t) ->
    undef_in t (prog_interface p) \/
    undef_in t (prog_interface c).
  Proof.
    move=> Hbeh; rewrite /undef_in /last_comp.
    apply/fsetUP; rewrite -domm_union /last_comp.
    have wf12 := linking_well_formedness wf1 wf2 linkability.
    rewrite -[unionm _ _]/(prog_interface (program_link p c)).
    move: (seq.mem_last Component.main (seq.map next_comp_of_event t)).
    rewrite seq.inE=> /orP [/eqP ->|].
      case: closedness_after_linking; rewrite wfprog_defined_procedures //.
      by rewrite /prog_main /find_procedure mem_domm; case: getm.
    case/seq.mapP=> e /In_in e_in_t ->.
    by case: (ub_behavior_has_well_defined_components Hbeh e_in_t).
  Qed.

  Lemma program_ub_doesnt_improve t beh_imp :
    program_behaves (PS.sem p (prog_interface c)) (Goes_wrong t) ->
    undef_in t (prog_interface p) ->
    program_behaves (PS.sem p (prog_interface c)) (behavior_app t beh_imp) ->
    beh_imp = Goes_wrong E0.
  Proof.
    move e_t: (Goes_wrong t)=> beh Hbeh.
    case: beh / Hbeh e_t; last first.
      (* program went wrong because it doesn't have an initial state *)
      move=> not_init [->] _; rewrite behavior_app_E0.
      by case: beh_imp / => // ? ? /not_init.
    (* program reaches a stuck state after zero or many steps *)
    move=> s_i beh Hinitial Hbeh.
    case: beh / Hbeh t=> // t s_f Hstar Hstuck Hnot_final _ [->] Hin_p.
    move e_beh: (behavior_app t beh_imp)=> beh Hbeh.
    case: beh / Hbeh e_beh; last by move=> /(_ _ Hinitial).
    move=> s_i' beh Hinitial'; have {s_i' Hinitial'} -> : s_i' = s_i.
      exact: PS.initial_state_determinism Hinitial' Hinitial.
    have [|/empty_behaviorPn beh_n0] := boolP (empty_behavior beh_imp).
      case: beh_imp=> _ //= /eqP ->; rewrite E0_right=> Hbeh e_beh;
      case: beh / Hbeh t e_beh Hstar Hin_p;
      move=> // t s_f' Hstar' Hfinal _ [->] Hstar Hin_p.
        have [ff|ff] := PS.state_determinism_star_same_trace Hstar Hstar'.
          case: ff Hnot_final Hfinal Hstuck=> [? Hnot_final /Hnot_final //|].
          by move=> ?????? Hstep _ _ _ _ /(_ _ _ Hstep).
        have {Hin_p} Hin_p : PS.is_program_component s_f' (prog_interface c).
          case: linkability=> _ dis.
          by rewrite -(PS.undef_in_program dis Hinitial Hstar').
        elim/star_E0_ind: s_f' s_f / ff Hnot_final Hfinal Hin_p {Hstuck Hstar Hstar'}.
          by move=> ? Hnot_final /Hnot_final.
        move=> s_f' s s_f Hstep _ _ Hfinal Hin_p.
        by have := PS.final_state_stuck Hfinal Hin_p Hstep.
      have [ff|ff] := PS.state_determinism_star_same_trace Hstar Hstar'.
        suffices [s contra] : exists s, Step (PS.sem p (prog_interface c)) s_f E0 s.
          by case/Hstuck: contra.
        by elim/star_E0_ind: ff Hfinal=> [? []|]; eauto.
      have {Hin_p} Hin_p : PS.is_program_component s_f' (prog_interface c).
        case: linkability=> _ dis.
        by rewrite -(PS.undef_in_program dis Hinitial Hstar').
      suffices [s contra] : exists s, Step (PS.sem p (prog_interface c)) s_f E0 s.
        by case/Hstuck: contra.
      elim/star_E0_ind: s_f' s_f / ff Hfinal Hin_p {Hstuck Hnot_final Hstar Hstar'}.
        by move=> s []; eauto.
      move=> s_a s_b s_c Hstep IH Hfinal Hin_p; apply: IH=> //.
        case: s_a / Hfinal Hstep Hin_p=> s_a s_b' /= Hstep' Hfinal Hstep Hin_p.
        by rewrite (PS.state_determinism_program Hin_p Hstep Hstep').
      rewrite /PS.is_program_component /PS.is_context_component /turn_of /=.
      by rewrite (PS.kstep_component Hstep).
    case: beh_n0=> {beh_imp} e [beh_imp ->].
    rewrite -behavior_app_assoc => Hbeh e_beh.
    move: Hbeh; rewrite -{}e_beh {beh}.
    case/(@state_behaves_app_inv _ (@PS.singleton_traces p (prog_interface c))).
    move=> s3 [/(star_middle1_inv (@PS.singleton_traces p (prog_interface c)))].
    case=> s1 [s2 [Hstar1 [Hstep2 Hstar3]]].
    have {Hstar} [Hstar|Hstar] := PS.state_determinism_star_same_trace Hstar Hstar1.
      suffices [s [t' contra]] : exists s t', Step (PS.sem p (prog_interface c)) s_f t' s.
        by case/Hstuck: contra.
      by elim/star_E0_ind: s_f s1 / Hstar Hstep2 {Hstuck Hnot_final Hstar1}; eauto.
    have {Hin_p} Hin_p : PS.is_program_component s1 (prog_interface c).
      case: linkability=> _ dis.
      by rewrite -(PS.undef_in_program dis Hinitial Hstar1).
    elim/star_E0_ind: s1 s_f / Hstar Hstuck Hstep2 Hin_p {Hnot_final Hstar1}.
      by move=> s_f Hstuck /Hstuck.
    move=> s1 s1a s1b Hstep1 _ _ Hstep2 Hin_p.
    by have [] := PS.state_determinism_program' Hin_p Hstep1 Hstep2.
  Qed.

  Set Implicit Arguments.

  Lemma improving_star_ending_in_stuck_state:
    forall s t s' t' s'',
      star (PS.kstep c (prog_interface p)) (prepare_global_env c) s t s' ->
      star (PS.kstep c (prog_interface p)) (prepare_global_env c) s (t ** t') s'' ->
      nostep (PS.kstep c (prog_interface p)) (prepare_global_env c) s' ->
      t' = E0 /\ star (PS.kstep c (prog_interface p)) (prepare_global_env c) s'' E0 s'.
  Proof.
    intros s t s' t' s''.
    intros Hstar1 Hstar2 Hnostep.
    destruct (PS.star_prefix Hstar1 Hstar2) as [|].
    - inversion H; subst.
      + split; auto.
      + exfalso. eapply Hnostep. eauto.
    - destruct H; subst. split; auto.
  Qed.
End Decomposition.

author: secure-compilation

repo: when-good-components-go-bad


text:
(** Generated by coq-of-ocaml *)
Require Import OCaml.OCaml.

Local Set Primitive Projections.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Local Open Scope type_scope.
Import ListNotations.

Unset Positivity Checking.
Unset Guard Checking.

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Inductive natural : Set :=
| Zero : natural
| Succ : natural -> natural.

Fixpoint plus (plus_arg0 : natural) (plus_arg1 : natural) {struct plus_arg0}
  : natural :=
  match plus_arg0 with
  | Zero => plus_arg1
  | Succ n => Succ (plus n plus_arg1)
  end.

Fixpoint mult (mult_arg0 : natural) (mult_arg1 : natural) {struct mult_arg0}
  : natural :=
  match mult_arg0 with
  | Zero => Zero
  | Succ n => plus (mult n mult_arg1) mult_arg1
  end.

Definition synth (lf1 : natural) (y : natural) : natural :=
  mult lf1 (plus y Zero).

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                Coq V5.10                                 *)
(*                              Nov 25th 1994                               *)
(*                                                                          *)
(****************************************************************************)
(*                                  Zrec.v                                  *)
(****************************************************************************)
Require Export Arith.
Require Export Nat_complements.
Require Export misc.
Require Export Zbase.
Require Export Zle.

(**********)
Lemma lt_OZ : forall m : Z, ~ ltZ (absZ m) OZ.

intros; unfold ltZ in |- *; elim m.
unfold not in |- *; simpl in |- *; intros; exact H.
unfold not in |- *; simpl in |- *; intros; exact H.
unfold not in |- *; simpl in |- *; intros; exact H.
Qed.

(**********)
Lemma Zrec1 :
 forall P : Z -> Set,
 (forall n : Z, (forall m : Z, lt_absZ m n -> P m) -> P n) -> P OZ.

intros; apply (H OZ); intros.
unfold lt_absZ in H0; unfold absZ at 2 in H0; elim (lt_OZ m); assumption.
Qed.

(**********************************)
Inductive and_set_set_set (S1 S2 : Set) : Set :=
    and_set_set_set_i : S2 -> S1 -> and_set_set_set S1 S2.

(*****************)
Definition and_recZ (p : nat) (P : Z -> Set) :=
  forall n : nat, n <= p -> and_set_set_set (P (pos n)) (P (neg n)).

(**********)
Lemma Zrec2 :
 forall P : Z -> Set,
 (forall n : Z, (forall m : Z, lt_absZ m n -> P m) -> P n) -> and_recZ 0 P.

unfold and_recZ in |- *; intros; apply and_set_set_set_i.
(* neg n *)
elim (le_n_O_eq n H0). apply (H (neg 0)); intros.
rewrite (tech_lt_abs_OZ m). apply (Zrec1 P H). exact H1.
(* pos n *)
elim (le_n_O_eq n H0). apply (H (pos 0)); intros.
rewrite (tech_lt_abs_OZ m). apply (Zrec1 P H). exact H1.
Qed.

(**********)
Lemma Zrec3 :
 forall (P : Z -> Set) (p : nat),
 (forall n : Z, (forall m : Z, lt_absZ m n -> P m) -> P n) ->
 and_recZ p P -> and_recZ (S p) P.

split.
(* P (neg n) *)
elim (lt_succ n p H1); intros. elim (H0 n a); intros; trivial with arith.
rewrite b. apply (H (neg (S p))).
simple destruct m. intros; apply (Zrec1 P H).
unfold lt_absZ in |- *; unfold absZ in |- *; unfold ltZ in |- *;
 unfold leZ in |- *; intros.
elim (H0 n0); auto with arith.
unfold lt_absZ in |- *; unfold absZ in |- *; unfold ltZ in |- *;
 unfold leZ in |- *; intros.
elim (H0 n0); auto with arith.
(* P (pos n) *)
elim (lt_succ n p H1); intros. elim (H0 n); intros; trivial with arith.
rewrite b. apply (H (pos (S p))).
simple destruct m. intros; apply (Zrec1 P H).
unfold lt_absZ in |- *; unfold absZ in |- *; unfold ltZ in |- *;
 unfold leZ in |- *; intros.
elim (H0 n0); auto with arith.
unfold lt_absZ in |- *; unfold absZ in |- *; unfold ltZ in |- *;
 unfold leZ in |- *; intros.
elim (H0 n0); auto with arith.
Qed.

(*************)
Theorem Zrec4 :
 forall P : Z -> Set,
 (forall n : Z, (forall m : Z, lt_absZ m n -> P m) -> P n) ->
 forall p : nat, and_recZ p P.

intros; elim p.
exact (Zrec2 P H).
intros; apply Zrec3; trivial with arith.
Qed.

(************)
Theorem recZ :
 forall P : Z -> Set,
 (forall n : Z, (forall m : Z, lt_absZ m n -> P m) -> P n) ->
 forall p : Z, P p.

intros; elim p.
(* OZ *)
exact (Zrec1 P H).
(* pos n *)
intro n; cut (and_recZ n P). intros.
elim (H0 n); auto with arith.
apply Zrec4; trivial with arith.
(* neg n *)
intro n; cut (and_recZ n P). intros.
elim (H0 n); auto with arith.
apply Zrec4; trivial with arith.
Qed.

author: coq-contribs

repo: chinese

save_path: github-repos/coq/coq-contribs-chinese


text:
(** * Adjunction composition *)
(** ** Definition *)
Require Adjoint.Composition.Core.
(** ** Associativity *)
Require Adjoint.Composition.AssociativityLaw.
(** * Left and right identity laws *)
Require Adjoint.Composition.IdentityLaws.

Include Adjoint.Composition.Core.
Include Adjoint.Composition.AssociativityLaw.
Include Adjoint.Composition.IdentityLaws.

Module Export AdjointCompositionNotations.
  Include AdjointCompositionCoreNotations.
End AdjointCompositionNotations.

author: HoTT

repo: Coq-HoTT

save_path: github-repos/coq/HoTT-Coq-HoTT


text:
Require Import SpecDeps.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import Constants.
Require Import CommonLib.
Require Import AbsAccessor.Spec.
Require Import PSCIAux.Spec.

Local Open Scope Z_scope.

Section SpecLow.

  Fixpoint system_off_reboot_loop0 (n: nat) (i: Z) (idx: Z) (g_rd: Pointer) (rec_list: Pointer) (adt: RData) :=
    match n with
    | O => Some (adt, i)
    | S n' =>
      match system_off_reboot_loop0 n' i idx g_rd rec_list adt with
      | Some (adt, i) =>
        rely is_int64 i;
        if i =? idx then
          Some (adt, i + 1)
        else
          when g_target_rec, adt == find_lock_rec_spec g_rd rec_list (VZ64 i) adt;
          when null == is_null_spec g_target_rec adt;
          rely is_int null;
          if null =? 0 then
            when t_rec, adt == granule_map_spec g_target_rec SLOT_REC_TARGET adt;
            when adt == set_rec_runnable_spec t_rec 0 adt;
            when adt == buffer_unmap_spec t_rec adt;
            when adt == granule_unlock_spec g_target_rec adt;
            Some (adt, i + 1)
        else Some (adt, i + 1)
      | _ => None
      end
    end.

  Definition system_off_reboot_spec0 (rec: Pointer) (adt: RData) : option RData :=
    when g_rec == get_rec_g_rec_spec rec adt;
	  when g_rd == get_rec_g_rd_spec rec adt;
	  when' idx == get_rec_rec_idx_spec rec adt;
    rely is_int64 idx;
    when g == get_rec_g_rec_list_spec rec adt;
    when adt == granule_lock_spec g_rec adt;
	  when adt == set_rec_runnable_spec rec 0 adt;
	  when adt == granule_unlock_spec g_rec adt;
    when rec_list, adt == granule_map_spec g SLOT_REC_LIST adt;
    match system_off_reboot_loop0 (Z.to_nat MAX_NUM_RECS) 0 idx g_rd rec_list adt with
    | Some (adt, i) =>
      rely is_int64 i;
      buffer_unmap_spec rec_list adt
    | _ => None
    end.

End SpecLow.

author: columbia