text:
From ITree Require Import ITree.
From compcert Require Coqlib.
From Paco Require Import paco.

Require Import sflib.
Require Import Axioms StdlibExt IntegersExt.

Require Import SysSem.
Require Import IPModel DiscreteTimeModel.
Require Import RTSysEnv.

Require Import List.
Require Import Arith ZArith Lia.

Module SNode.
  Section SNODE.
    Context {sysE: Type -> Type}.
    Context {msgT: Set}.
    Variable sanitize_msg: msgT -> msgT?.

    Notation appE := (sysE +' @abst_sendE msgT).

    Record t : Type :=
      mk { (* mcast_groups: list Tid ; *)
           app_state: Type ;
           init_app_state: app_state -> Prop ;

           period_begin: Z(*sytm*) -> list (msgT?) ->
                         app_state -> app_state -> Prop ;
           app_step: app_state -> app_state -> Prop ;
           at_event: app_state -> event_call appE -> Prop ;
           after_event: app_state -> event appE -> app_state -> Prop ;
           period_end: app_state -> bool ;
         }.

    (** ** ITree as SNode *)
    Section RUN_PERIOD.
      Variable num_tasks: nat.
      Variable mcasts: list (list Tid).

      Variable node: t.
      Notation app_state := node.(app_state).

      Inductive istep
        : app_state -> (event (nbE +' sysE))? ->
          (Tid * msgT)? -> app_state -> Prop :=
      | IStep_Tau
          ast ast'
          (TAU_STEP: node.(app_step) ast ast')
        : istep ast None None ast'
      | IStep_SysEvent
          R (syse: sysE R) (r: R)
          ast (evt: event (nbE +' sysE)) ast'
          (AT_EVENT: node.(at_event) ast (EventCall (inl1 syse)))
          (AFT_EVENT: node.(after_event)
                             ast (Event (inl1 syse) r) ast')
          (VIS_EVENT: evt = Event (subevent _ syse) r)
        : istep ast (Some evt) None ast'
      | IStep_Msg
          tid msg snde
          ast ast'
          (SEND_EVENT: snde = AbstSendEvent tid msg)
          (AT_EVENT: node.(at_event) ast (EventCall (inr1 snde)))
          (AFT_EVENT: node.(after_event)
                             ast (Event (inr1 snde) tt) ast')
        : istep ast None (Some (tid, msg)) ast'
      .

      Definition is_in_tids (tid: Tid) (tids: list Tid): bool :=
        existsb (Nat.eqb tid) tids.

      Definition check_available1
                 (outbox: list msgT?)
                 (tid_ad: Tid)
        : bool :=
        match nth_error outbox tid_ad with
        | None => false
        | Some entry =>
          match entry with
          | None => true
          | Some _ => false
          end
        end.

      Definition check_available
                 (tids_ad: list Tid)
                 (outbox: list msgT?) : bool :=
        andb_all (map (check_available1 outbox) tids_ad).

      Definition get_actual_dest (tid: Tid): list Tid :=
        if tid <? num_tasks then [tid]
        else
          match nth_error mcasts (tid - num_tasks) with
          | None => []
          | Some member_tids => member_tids
          end.

      Definition insert_msg1
                 (tids_ad: list Tid) (msg: msgT)
                 (tid_entry: Tid) (entry: msgT?)
        : msgT? :=
        if is_in_tids tid_entry tids_ad then
          Some msg
        else entry.

      Definition insert_msg
                 (tids_ad: list Tid) (msg: msgT)
                 (outbox: list msgT?)
        : list msgT? :=
        imap (insert_msg1 tids_ad msg) 0 outbox.

      Definition update_outbox
                 (outb: list msgT?)
                 (oms: (Tid * msgT)?)
        : list msgT? :=
        match oms with
        | None => outb
        | Some (tid_d, msg) =>
          match sanitize_msg msg with
          | None => outb
          | Some msg_s =>
            let tids_ad := get_actual_dest tid_d in
            if check_available tids_ad outb then
              insert_msg tids_ad msg_s outb
            else outb
          end
        end.

      Lemma update_outbox_None outb:
        update_outbox outb None = outb.
      Proof. ss. Qed.

      Lemma update_outbox_not_in
            outb tid1 tid2 msg
            (IN: ~ List.In tid1 (get_actual_dest tid2)):
        nth tid1 (update_outbox outb (Some (tid2, msg))) None =
        nth tid1 outb None.
      Proof.
        ss. des_ifs.
        unfold insert_msg.
        destruct (classic (tid1 < length outb)); cycle 1.
        { repeat rewrite nth_overflow; ss; try nia.
          rewrite imap_length. nia.
        }
        specialize (imap_nth_error_iff
                      _ _ (insert_msg1 (get_actual_dest tid2) m) 0 outb tid1). i.
        erewrite nth_error_nth' in H0; cycle 1.
        { rewrite imap_length. ss. }
        erewrite nth_error_nth' in H0; ss.
        inv H0. rewrite H2.
        instantiate (1:=None).
        unfold insert_msg1. des_ifs.
        unfold is_in_tids in *.
        erewrite existsb_exists in Heq1. des.
        rewrite Nat.eqb_eq in Heq2. subst. ss.
      Qed.

      Lemma update_outbox_in
            outb tid1 tid2 msg msg_s
            (LENGTH: length outb = num_tasks)
            (MSG: sanitize_msg msg = Some msg_s)
            (IN: In tid1 (get_actual_dest tid2))
            (TID: tid1 < length outb)
            (AVAILABLE: check_available (get_actual_dest tid2) outb = true):
        nth tid1 (update_outbox outb (Some (tid2, msg))) None = Some msg_s.
      Proof.
        ss. rewrite MSG, AVAILABLE.
        unfold insert_msg.
        specialize (imap_nth_error_iff
                      _ _ (insert_msg1 (get_actual_dest tid2) msg_s) 0 outb tid1). i.
        erewrite nth_error_nth' in H; cycle 1.
        { rewrite imap_length. ss. }
        erewrite nth_error_nth' in H; ss.
        inv H. rewrite H1. instantiate (1:=None).
        unfold insert_msg1. des_ifs.
        unfold is_in_tids in *.
        exploit existsb_exists. i. des.
        exploit x1; cycle 1.
        { i. rewrite x in Heq. ss. }
        { esplits; try eapply IN. apply Nat.eqb_eq. ss. }
      Qed.

      Lemma update_outbox_length outb msg:
        length (update_outbox outb msg) = length outb.
      Proof.
        unfold update_outbox. des_ifs.
        unfold insert_msg. apply imap_length.
      Qed.

      Lemma update_outbox_empty msg:
        update_outbox [] msg = [].
      Proof.
        unfold update_outbox. des_ifs.
      Qed.

      Lemma update_outbox_check_available
            tid1 tid2 outb msg
            (IN: ~ In tid1 (get_actual_dest tid2)):
        check_available1 (update_outbox outb (Some (tid2, msg))) tid1 =
        check_available1 outb tid1.
      Proof.
        unfold update_outbox. des_ifs.
        unfold insert_msg, check_available1.
        rewrite imap_nth_error_iff.
        unfold insert_msg1. ss.
        destruct (nth_error outb tid1) eqn:NTH; ss.
        des_ifs.
        unfold is_in_tids in *.
        rewrite existsb_exists in Heq2. des.
        rewrite Nat.eqb_eq in Heq1. subst. ss.
      Qed.

      Inductive istar
        : app_state * list msgT? ->
          events (nbE +' sysE) ->
          app_state? * list msgT? -> Prop :=
      | IStar_Fail
          ast outb
        : istar (ast, outb) [] (None, outb)
      | IStar_Base
          ast outb
        : istar (ast, outb) [] (Some ast, outb)
      | IStar_step
          ast es1 oms1 ast1
          outb outb1
          es2 oast' outb' es
          (ASTEP: istep ast es1 oms1 ast1)
          (INSERT_OUTB: outb1 = update_outbox outb oms1)
          (ASTAR': istar (ast1, outb1) es2
                         (oast', outb'))
          (EVENTS_APP: es = opt2list es1 ++ es2)
          (* (OUTMSGS_APP: oms = opt2list oms1 ++ oms2) *)
        : istar (ast, outb) es (oast', outb')
      .

      Definition init_box: list msgT? :=
        repeat None num_tasks.

      Inductive run_period
                (sytm: nat) (inb: list msgT?)
        : app_state -> events (nbE +' sysE) ->
          list msgT? -> app_state? -> Prop :=
      | RunPeriod_PrdInitFailed
          ast (* outb_i *)
          (* (OUT B_I: outb_i = repeat None num_tasks) *)
        : run_period sytm inb
                     ast [] (* outb_i *) [] None
      | RunPeriod_PrdInitOK
          ast ast1 es oast' outb'
          (PERIOD_BEGIN: node.(period_begin) (Z.of_nat sytm) inb ast ast1)
          (STAR: istar (ast1, init_box) es (oast', outb'))
          (FINAL: option_rel1 node.(period_end) oast')
        : run_period sytm inb
                     ast es outb' oast'.

    End RUN_PERIOD.

    Inductive state: Type :=
      State (tid: Tid) (node: t)
            (* (mids: list Tid) *)
            (inbox: list msgT?)
            (oast: node.(app_state)?).

    Inductive state_wf (num_tasks: nat) (tid: Tid)
      : state -> Prop :=
      StateWf
        node inb oast
        (LEN_INB: length inb = num_tasks)
      : state_wf num_tasks tid (State tid node inb oast).

    Definition init_state (num_tasks: nat)
               (tid: Tid) (node: t) : state :=
      (* let mids := i_get_mcast_of tid imcasts in *)
      State tid node (repeat None num_tasks) None.

    Lemma wf_init_state nts tid node
      : state_wf nts tid (init_state nts tid node).
    Proof.
      econs; eauto.
      rewrite repeat_length. ss.
    Qed.

    Inductive step
              (num_tasks: nat)
              (mcasts: list (list Tid))
              (sytm: nat)
      : state -> (events (nbE +' sysE)) ->
        (list msgT?) -> state -> Prop :=
    | Step_InactInact
        tid node inb inb_i
        (INB_I: inb_i = init_box num_tasks)
      : step num_tasks mcasts sytm
             (State tid node inb None) ([]) []
             (State tid node inb_i None)

    | Step_Activate
        tid node inb ast inb_i
        (INB_I: inb_i = init_box num_tasks)
        (INIT_APP_STATE: node.(init_app_state) ast)
      : step num_tasks mcasts sytm
             (State tid node inb None) ([]) []
             (State tid node inb_i (Some ast))

    | Step_Run
        tid node inb ast
        es outb oast' inb_i
        (RUN_PERIOD: run_period
                       num_tasks mcasts
                       node sytm inb ast es outb oast')
        (* (OUTBOX_DEST: outb_d = make_outbox outb) *)
        (INB_I: inb_i = init_box num_tasks)
      : step num_tasks mcasts sytm
             (State tid node inb (Some ast))
             (es) outb
             (State tid node inb_i oast')
    .

    Lemma wf_prsv
          nt mcs sytm
          st te oms st' tid
          (STEP: step nt mcs sytm
                      st te oms st')
          (WF: state_wf nt tid st)
      : state_wf nt tid st'.
    Proof.
      inv WF.
      inv STEP.
      - econs.
        unfold init_box.
        rewrite repeat_length. ss.
      - econs.
        unfold init_box.
        rewrite repeat_length. ss.
      - econs.
        unfold init_box.
        rewrite repeat_length. ss.
    Qed.

    Definition get_outbox_msg_by_dest
               (tid: Tid)
               (outb: list msgT?): msgT? :=
      match nth_error outb tid with
      | None => None
      | Some om => om
      end.

    Lemma get_outbox_msg_nth tid outb:
      get_outbox_msg_by_dest tid outb = nth tid outb None.
    Proof.
      unfold get_outbox_msg_by_dest. des_ifs.
      - eapply nth_error_nth in Heq. eauto.
      - rewrite nth_error_None in Heq.
        symmetry. apply nth_overflow. ss.
    Qed.

    Definition accept_msgs
               (in_msgs_sys: list (list msgT?))
               (st: state)
      : state :=
      match st with
      | State tid node _ oast =>
        let inb: list msgT? :=
            map (get_outbox_msg_by_dest tid) in_msgs_sys in
        State tid node inb oast
      end.

    Lemma wf_accept_msgs_prsv
          nts tid ins
          st st'
          (ACCEPT: accept_msgs ins st = st')
          (LEN_INS: length ins = nts)
          (WF: state_wf nts tid st)
      : state_wf nts tid st'.
    Proof.
      inv WF. ss.
      econs.
      rewrite map_length. ss.
    Qed.

    Lemma step_progress
          nts mcs sytm st
      : exists es outb st',
        step nts mcs sytm
             st es outb st'.
    Proof.
      destruct st as [tid node inb []].
      - esplits. econs; eauto.
        econs 1; eauto.
      - esplits. econs 1. eauto.
    Qed.

    (** istar lemmas *)

    Lemma istar_snoc_fail
          n mcs (node: t)
          ast outb es oast1 outb1
          (ISTAR: istar n mcs node (ast, outb) es (oast1, outb1))
      : istar n mcs node (ast, outb) es (None, outb1).
    Proof.
      remember (ast, outb) as st.
      remember (oast1, outb1) as st1.
      depgen ast. depgen oast1.
      revert outb outb1.
      induction ISTAR; i; ss.
      - clarify. econs.
      - clarify. econs.
      - clarify.
        hexploit IHISTAR; eauto.
        intro ISTAR'.
        econs; eauto.
    Qed.

    Lemma istar_app
          n mcs (node: t)
          ast0 outb0 es1
          ast1 outb1 es2
          oast' outb'
          (ISTAR1: istar n mcs node (ast0, outb0) es1
                         (Some ast1, outb1))
          (ISTAR2: istar n mcs node (ast1, outb1) es2
                         (oast', outb'))
      : istar n mcs node (ast0, outb0) (es1 ++ es2)
              (oast', outb').
    Proof.
      remember (ast0, outb0) as st0 eqn:ST0.
      remember (Some ast1, outb1) as st1 eqn:ST1.
      clear ast0 outb0 ST0.

      induction ISTAR1; i; ss.
      - clarify.
      - clarify.
        econs 3; eauto.
        rewrite app_assoc. ss.
    Qed.

  End SNODE.

End SNode.

Module SyncSys.
  Section SYS.
    Context {sysE: Type -> Type}.
    Context {msgT: Set}.

    Record t: Type :=
      mk { period: nat ;
           nodes: list (@SNode.t sysE msgT) ;
           mcasts: list (list Tid) ;

           sanitize_msg: msgT -> msgT? ;
         }.

    Inductive wf: t -> Prop :=
      Wf prd nds mcs sntz (* imcasts *)
         (PERIOD_POS: 0 < prd)
      : wf (mk prd nds mcs sntz).

    Record state: Type :=
      State { time: nat ;
              node_states: list (@SNode.state sysE msgT) ;
            }.

    Inductive state_wf (num_tasks: nat)
      : state -> Prop :=
      StateWf
        tm nsts
        (WF_NSTS: iForall (SNode.state_wf num_tasks) 0 nsts)
        (NUM_TASKS: length nsts = num_tasks)
      : state_wf num_tasks (State tm nsts).

    Definition init_state (tm_init: nat) (sys: t): state :=
      let nds := nodes sys in
      let nsts := imap (SNode.init_state (length nds)) 0 nds in
      State tm_init nsts.

    Lemma wf_init_state
          tm sys
          (* (WF_SYS: wf sys) *)
      : state_wf (length (nodes sys))
                 (init_state tm sys).
    Proof.
      econs; eauto.
      2: { rewrite imap_length. ss. }
      (* inv WF_SYS. ss. *)
      destruct sys as [period nodes mcasts]. ss.
      apply iForall_nth. ss.
      i. rewrite imap_nth_error_iff.
      destruct (nth_error nodes n); ss.
      econs. rewrite repeat_length; ss.
    Qed.

    Inductive step
              (mcasts: list (list Tid)) (period: nat)
              (sntz: msgT -> msgT?)
      : state -> list (tsp * events (nbE +' sysE)) ->
        state -> Prop :=
    | Step_Wait
        tm nsts tes
        (WAIT: ~ Nat.divide period tm)
        (EMPTY_EVTS: tes = List.repeat (Z.of_nat tm, []) (length nsts))
      : step mcasts period sntz
             (State tm nsts) tes (State (S tm) nsts)

    | Step_Run
        tm nsts ess tes outs nsts1 nsts'
        (WAIT: Nat.divide period tm)
        (STEPS: Forall4 (SNode.step sntz (length nsts) mcasts tm) nsts ess outs nsts1)
        (ACCEPT_MSGS: List.map (SNode.accept_msgs outs) nsts1 = nsts')
        (ATTACH_TIMESTAMP: map (fun es => (Z.of_nat tm, es)) ess = tes)
      : step mcasts period sntz
             (State tm nsts) tes (State (S tm) nsts')
    .

    Lemma wf_prsv
          nt mcs sntz prd
          st es st'
          (STEP: step mcs prd sntz
                      st es st')
          (WF_STATE: state_wf nt st)
      : state_wf nt st'.
    Proof.
      inv WF_STATE. inv STEP.
      - econs; eauto.
      - econs; eauto.
        2: { rewrite map_length.
             hexploit Forall4_length; eauto.
             i. des. eauto. }
        apply iForall_nth. i.
        rewrite iForall_nth in WF_NSTS.
        specialize (WF_NSTS n). ss.

        rewrite Coqlib.list_map_nth.
        destruct (nth_error nsts n) as [nst_n|] eqn: NST_N.
        2: {
          rewrite nth_error_None2.
          { econs. }
          apply Forall4_length in STEPS.
          des.
          rewrite <- LEN14.
          apply nth_error_None. ss.
        }

        hexploit Forall4_nth1; eauto. i. des.
        rewrite NTH4. ss.
        eapply SNode.wf_accept_msgs_prsv; eauto.
        { hexploit Forall4_length; eauto. i. des. ss. }
        eapply SNode.wf_prsv; eauto.
    Qed.

    Lemma wf_progress
          mcs prd sntz
          nt st
          (WF_STATE: state_wf nt st)
      : exists es st',
        step mcs prd sntz st es st'.
    Proof.
      destruct st as [tm nsts].

      destruct (Nat_divide_dec prd tm).
      2: { esplits. econs 1; eauto. }

      assert (exists l2 l3 l4,
                 Forall4 (SNode.step sntz (length nsts) mcs tm)
                         nsts l2 l3 l4).
      { eapply Forall4_exists_list.
        i. apply SNode.step_progress. }
      des.
      esplits. econs 2; eauto.
    Qed.

    Definition num_sites (st: state): nat :=
      length st.(node_states).

    Program Definition as_dsys (sys: t) (tm_init: nat): DSys.t :=
      DSys.mk state num_sites
              (step (mcasts sys) (period sys) (sanitize_msg sys))
              (fun st => st = init_state tm_init sys) _.
    Next Obligation.
      splits.
      - unfold num_sites.
        inv STEP; ss.
        + rewrite repeat_length. ss.
        + hexploit Forall4_length; eauto. i. des.
          rewrite map_length. ss.
      - unfold num_sites.
        inv STEP; ss.
        rewrite map_length.
        hexploit Forall4_length; eauto. i. des. ss.
    Qed.

    Lemma safe
          tm
          (sys: t)
          (WF: wf sys)
      : DSys.safe (as_dsys sys tm).
    Proof.
      econs.
      { esplits; ss. }
      i.
      pose (num_tasks := length (nodes sys)).

      assert (WF_STATE: state_wf num_tasks st_i).
      { subst num_tasks.
        inv INIT.
        apply wf_init_state. }
      rename st_i into st.
      clear INIT.
      depgen st.

      pcofix CIH. i.
      pfold. econs.
      { eapply wf_progress. eauto. }
      i. right. ss.
      hexploit wf_prsv; eauto.
    Qed.

  End SYS.
End SyncSys.

Module AppMod.
  Record t {sysE: Type -> Type} {msgT: Set}: Type :=
    mk { abst_state_t: Type;
         job_itree: Z (*sync_time*) -> list msgT? ->
                    abst_state_t ->
                    itree (sysE +' (* bsendE *) @abst_sendE msgT) abst_state_t ;

         init_abst_state: abst_state_t ;
       }.
End AppMod.

Module ITrSNode.
  Section SNODE.
    Context {sysE: Type -> Type}.
    Context {msgT: Set}.

    Variable app_mod: @AppMod.t sysE msgT.

    Let sendE: Type -> Type := @abst_sendE msgT.
    Let appE: Type -> Type := sysE +' sendE.

    Let astate_t: Type := AppMod.abst_state_t app_mod.
    Let t : Type := itree appE astate_t.

    Inductive init_app_state : t -> Prop :=
      InitAppState
        ast itr
        (INIT_ASTATE: AppMod.init_abst_state app_mod = ast)
        (INIT_ITREE: itr = Ret ast)
      : init_app_state itr.

    Inductive period_begin (zsytm: Z) (inb: list msgT?)
      : t -> t -> Prop :=
      PeriodBegin
        itr0 ast0 itr1
        (RET: observe itr0 = RetF ast0)
        (PERIOD_INIT_ITREE:
           itr1 = AppMod.job_itree app_mod zsytm inb ast0)
      : period_begin zsytm inb itr0 itr1.

    Inductive app_step: t -> t -> Prop :=
    | AppStep
        itr itr'
        (OBS_TAU: observe itr = TauF itr')
      : app_step itr itr'
    .

    Inductive at_event: t -> event_call appE -> Prop :=
      AtEvent
        R itr (e: appE R) k
        (OBS: observe itr = VisF e k)
      : at_event itr (EventCall e)
    .

    Inductive after_event: t -> event appE -> t -> Prop :=
      AfterEvent
        R itr (e: appE R) k (r: R) itr'
        (OBS: observe itr = VisF e k)
        (AFTER_EVENT: k r = itr')
      : after_event itr (Event e r) itr'.

    Definition period_end (itr: t): bool :=
      match observe itr with
      | RetF _ => true
      | _ => false
      end.

    Definition to_snode: SNode.t :=
      SNode.mk t
               init_app_state period_begin
               app_step at_event after_event period_end.

  End SNODE.
End ITrSNode.

author: kim-yoonseung

repo: pals-thesis-dev


text:
Require Import Coq.Program.Basics.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Program.Combinators.
Require Import omega.Omega.
Require Import Setoid.
Require Import ZArith.

Require Import FinProof.Common.
Require Import FinProof.CommonInstances.
Require Import FinProof.StateMonad2.
Require Import FinProof.StateMonadInstances.
Require Import FinProof.ProgrammingWith.

Local Open Scope struct_scope.

Require Import FinProof.CommonProofs.
Require Import depoolContract.ProofEnvironment.
Require Import depoolContract.DePoolClass.
Require Import depoolContract.SolidityNotations.

Require Import depoolContract.DePoolFunc.
Module DePoolFuncs := DePoolFuncs XTypesSig StateMonadSig.
Import DePoolFuncs.
Import DePoolSpec.
Import LedgerClass.

Require Import depoolContract.Lib.CommonModelProofs.
Module CommonModelProofs := CommonModelProofs StateMonadSig.
Import CommonModelProofs.
Require Import depoolContract.Lib.Tactics.
Require Import depoolContract.Lib.ErrorValueProofs.
(*Require Import depoolContract.Lib.CommonCommon.*)
(* Require Import depoolContract.Lib.tvmFunctionsProofs. *)

Import DePoolSpec.LedgerClass.SolidityNotations.

Local Open Scope struct_scope.
Local Open Scope Z_scope.
Local Open Scope solidity_scope.
Require Import Lists.List.
Import ListNotations.
Local Open Scope list_scope.

Set Typeclasses Iterative Deepening.
Set Typeclasses Depth 100.

Require Export depoolContract.Scenarios.Projections.Round_Stakes.States.
Require Export depoolContract.Scenarios.Common.RotateRoundsCondition.
Require Export depoolContract.Scenarios.Common._returnOrReinvestMove.
Require Export depoolContract.Scenarios.Common.RewardsMove.
Require Export depoolContract.Scenarios.Common.RotateRoundsCondition.

Section Round_Stakes_conditions.

Variable constructorCalled : Prop.
Variable ticktockCalled : Prop.
Variable completeRoundWithChunkCalled : Prop.
Variable addOrdinaryStakeCalled : Prop.
Variable addVestingStakeCalled : Prop.
Variable addLockStateCalled : Prop.
Variable withdrawFromPoolingRoundCalled : Prop.
Variable roundId participantQty chunkSize stake totalPeriod withdrawalPeriod : Z.
Variable withdrawValue queryId elector : Z.
Variable beneficiary : XAddress.

Definition generateRoundCalled (l : Ledger) :=
    constructorCalled \/ rotate_round_conditions_full l ticktockCalled.

Definition projection_round_stakes_constructor_condition
(l : Ledger) (r : RoundsBase_ι_Round) :=
    generateRoundCalled l.

Definition projection_round_stakes_constructor_move
(ol nl : Ledger) (or nr : RoundsBase_ι_Round) :=
    roundIn nl nr /\
    ~ roundIn ol nr /\
    projection_round_stakes_constructor_condition ol or /\
    getProjectionRoundStakesState nr = _Projection_Round_Stakes_State 0 0 0 false 0 0 0.

Definition projection_round_stakes_add_ordinary_stake_condition
(l : Ledger) (r : RoundsBase_ι_Round) :=
    eval_state (↑12 ε DePoolContract_ι_m_poolClosed) l = false /\
    internalMessage l /\
    addOrdinaryStakeCalled /\
    r = round0 l /\
    stake + STAKE_FEE l <= msgValue l /\
    m_minStake l <= stake
    .

Definition projection_round_stakes_add_ordinary_stake_move
(ol nl : Ledger) (or nr : RoundsBase_ι_Round) :=
    projection_round_stakes_add_ordinary_stake_condition ol or /\
    roundsSame or nr /\
    nr = round0 nl /\
    let nprc := getProjectionRoundStakesState nr in
    let oprc := getProjectionRoundStakesState or in
    projection_round_stakes_getStake nprc = projection_round_stakes_getStake oprc + stake /\
    projection_round_stakes_getRecoveredStake nprc = projection_round_stakes_getRecoveredStake oprc /\
    projection_round_stakes_getUnused nprc = projection_round_stakes_getUnused oprc /\
    projection_round_stakes_getIsValidatorStakeCompleted nprc =
        projection_round_stakes_getIsValidatorStakeCompleted oprc /\
    projection_round_stakes_getRewards nprc = projection_round_stakes_getRewards oprc /\
    projection_round_stakes_getValidatorStake nprc = projection_round_stakes_getValidatorStake oprc /\
    projection_round_stakes_getHandledStakesAndRewards nprc =
        projection_round_stakes_getHandledStakesAndRewards oprc.

Definition projection_round_stakes_add_vesting_or_lock_stake_condition
(l : Ledger) (r : RoundsBase_ι_Round) :=
    eval_state (↑12 ε DePoolContract_ι_m_poolClosed) l = false /\
    (addLockStateCalled \/ addVestingStakeCalled)  /\
    isStdAddrWithoutAnyCast beneficiary = true /\
    (r = round0 l \/ r = roundPre0 l) /\
    stake + STAKE_FEE l <= msgValue l /\
    m_minStake l <= stake / 2 /\
    totalPeriod <= withdrawalPeriod /\
    totalPeriod <= 18 * 365 * 86400 /\
    0 < withdrawalPeriod /\
    Zmod totalPeriod withdrawalPeriod = 0
    .

Definition projection_round_stakes_add_vesting_or_lock_stake_move
(ol nl : Ledger) (or nr : RoundsBase_ι_Round) :=
    projection_round_stakes_add_ordinary_stake_condition ol or /\
    roundsSame or nr /\
    ((nr = round0 nl /\ or = round0 ol) \/ (nr = roundPre0 nl /\ or = roundPre0 ol))  /\
    let nprc := getProjectionRoundStakesState nr in
    let oprc := getProjectionRoundStakesState or in
    projection_round_stakes_getStake nprc = projection_round_stakes_getStake oprc + stake /\
    projection_round_stakes_getRecoveredStake nprc = projection_round_stakes_getRecoveredStake oprc /\
    projection_round_stakes_getUnused nprc = projection_round_stakes_getUnused oprc /\
    projection_round_stakes_getIsValidatorStakeCompleted nprc =
        projection_round_stakes_getIsValidatorStakeCompleted oprc /\
    projection_round_stakes_getRewards nprc = projection_round_stakes_getRewards oprc /\
    projection_round_stakes_getValidatorStake nprc = projection_round_stakes_getValidatorStake oprc /\
    projection_round_stakes_getHandledStakesAndRewards nprc =
        projection_round_stakes_getHandledStakesAndRewards oprc.

Definition projection_round_stakes_complete_round_with_chunk_condition
(l : Ledger) (r : RoundsBase_ι_Round) :=
    selfCall l /\
    completeRoundWithChunkCalled /\
    poolClosed l = false /\
    roundId = RoundsBase_ι_Round_ι_id r /\
    r = round2 l /\
    RoundsBase_ι_Round_ι_step r = RoundsBase_ι_RoundStepP_ι_Completing /\
    (0%nat < length (RoundsBase_ι_Round_ι_stakes r))%nat.

Definition projection_round_stakes_complete_round_with_chunk_move
(ol nl : Ledger) (or nr : RoundsBase_ι_Round) :=
    projection_round_stakes_complete_round_with_chunk_condition ol or /\
    roundsSame or nr /\
    nr = round2 nl  /\
    let nprc := getProjectionRoundStakesState nr in
    let oprc := getProjectionRoundStakesState or in
    projection_round_stakes_getStake nprc = projection_round_stakes_getStake oprc /\
    projection_round_stakes_getRecoveredStake nprc = projection_round_stakes_getRecoveredStake oprc /\
    projection_round_stakes_getUnused nprc = projection_round_stakes_getUnused oprc /\
    projection_round_stakes_getIsValidatorStakeCompleted nprc = true /\
    projection_round_stakes_getRewards nprc = projection_round_stakes_getRewards oprc /\
    projection_round_stakes_getValidatorStake nprc =
        projection_round_stakes_getValidatorStake oprc /\
    projection_round_stakes_getHandledStakesAndRewards nprc =
    _returnOrReinvest_round2_handledStakesAndRewards ol or.

Definition projection_round_stakes_complete_round_with_chunk0_condition
(l : Ledger) (r : RoundsBase_ι_Round) :=
    selfCall l /\
    completeRoundWithChunkCalled /\
    poolClosed l = false /\
    roundId = RoundsBase_ι_Round_ι_id (round2 l) /\
    r = round0 l /\
    RoundsBase_ι_Round_ι_step (round2 l) = RoundsBase_ι_RoundStepP_ι_Completing /\
    (0%nat < length (RoundsBase_ι_Round_ι_stakes (round2 l)))%nat.

Definition projection_round_stakes_complete_round_with_chunk0_move
(ol nl : Ledger) (or nr : RoundsBase_ι_Round) :=
    projection_round_stakes_complete_round_with_chunk0_condition ol or /\
    roundsSame or nr /\
    nr = round0 nl  /\
    let nprc := getProjectionRoundStakesState nr in
    let oprc := getProjectionRoundStakesState or in
    projection_round_stakes_getStake nprc = projection_round_stakes_getStake oprc +
        _returnOrReinvest_round0_stake ol (round2 ol) /\
    projection_round_stakes_getRecoveredStake nprc = projection_round_stakes_getRecoveredStake oprc /\
    projection_round_stakes_getUnused nprc = projection_round_stakes_getUnused oprc /\
    projection_round_stakes_getIsValidatorStakeCompleted nprc =
        projection_round_stakes_getIsValidatorStakeCompleted oprc /\
    projection_round_stakes_getRewards nprc = projection_round_stakes_getRewards oprc /\
    projection_round_stakes_getValidatorStake nprc =
        projection_round_stakes_getValidatorStake oprc /\
    projection_round_stakes_getHandledStakesAndRewards nprc =
    projection_round_stakes_getHandledStakesAndRewards oprc.

Definition projection_round_stakes_withdraw_from_pooling_round_condition
(l : Ledger) (r : RoundsBase_ι_Round) :=
    internalMessage l /\
    withdrawFromPoolingRoundCalled /\
    r = round0 l /\
    poolClosed l = false /\
    0 < withdrawValue /\
    isSome ((RoundsBase_ι_Round_ι_stakes r) ->fetch (msgSender l)) = true /\
    0 < RoundsBase_ι_StakeValue_ι_ordinary (
        maybeGet ((RoundsBase_ι_Round_ι_stakes r) ->fetch (msgSender l))).

Definition projection_round_stakes_withdraw_from_pooling_round_move
(ol nl : Ledger) (or nr : RoundsBase_ι_Round) :=
    projection_round_stakes_withdraw_from_pooling_round_condition ol or /\
    roundsSame or nr /\
    nr = round0 nl  /\
    let nprc := getProjectionRoundStakesState nr in
    let oprc := getProjectionRoundStakesState or in
    projection_round_stakes_getStake nprc = projection_round_stakes_getStake oprc -
        intMin
            (RoundsBase_ι_StakeValue_ι_ordinary (
                maybeGet ((RoundsBase_ι_Round_ι_stakes or) ->fetch (msgSender ol))))
            withdrawValue /\
    projection_round_stakes_getRecoveredStake nprc = projection_round_stakes_getRecoveredStake oprc /\
    projection_round_stakes_getUnused nprc = projection_round_stakes_getUnused oprc /\
    projection_round_stakes_getIsValidatorStakeCompleted nprc =
        projection_round_stakes_getIsValidatorStakeCompleted oprc /\
    projection_round_stakes_getRewards nprc = projection_round_stakes_getRewards oprc /\
    projection_round_stakes_getValidatorStake nprc =
        projection_round_stakes_getValidatorStake oprc /\
    projection_round_stakes_getHandledStakesAndRewards nprc =
    projection_round_stakes_getHandledStakesAndRewards oprc.

Definition projection_round_stakes_on_recover_stake_condition
    (l : Ledger) (r : RoundsBase_ι_Round) :=
    queryId = RoundsBase_ι_Round_ι_id r /\
    roundIn l r /\
    msgSender l = RoundsBase_ι_Round_ι_proxy r /\
    elector = RoundsBase_ι_Round_ι_elector r /\
    RoundsBase_ι_Round_ι_step r = RoundsBase_ι_RoundStepP_ι_WaitingReward.

Definition projection_round_stakes_on_recover_stake_move
(ol nl : Ledger) (or nr : RoundsBase_ι_Round) :=
    projection_round_stakes_on_recover_stake_condition ol or /\
    roundsSame or nr /\
    let nprc := getProjectionRoundStakesState nr in
    let oprc := getProjectionRoundStakesState or in
    projection_round_stakes_getStake nprc = projection_round_stakes_getStake oprc /\
    projection_round_stakes_getRecoveredStake nprc =
        msgValue ol + PROXY_FEE ol /\
    projection_round_stakes_getUnused nprc = projection_round_stakes_getUnused oprc /\
    projection_round_stakes_getIsValidatorStakeCompleted nprc =
        projection_round_stakes_getIsValidatorStakeCompleted oprc /\
    projection_round_stakes_getRewards nprc = rewardsMove_reward ol or /\
    projection_round_stakes_getValidatorStake nprc =
        projection_round_stakes_getValidatorStake oprc /\
    projection_round_stakes_getHandledStakesAndRewards nprc =
    projection_round_stakes_getHandledStakesAndRewards oprc.

Definition projection_round_stakes_on_recover_stake_unused_condition
    (l : Ledger) (r : RoundsBase_ι_Round) :=
    queryId = RoundsBase_ι_Round_ι_id r /\
    roundIn l r /\
    msgSender l = RoundsBase_ι_Round_ι_proxy r /\
    elector = RoundsBase_ι_Round_ι_elector r /\
    RoundsBase_ι_Round_ι_step r = RoundsBase_ι_RoundStepP_ι_WaitingIfValidatorWinElections /\
    msgValue l < RoundsBase_ι_Round_ι_stake r.

Definition projection_round_stakes_on_recover_stake_unused_move
(ol nl : Ledger) (or nr : RoundsBase_ι_Round) :=
    projection_round_stakes_on_recover_stake_unused_condition ol or /\
    roundsSame or nr /\
    let nprc := getProjectionRoundStakesState nr in
    let oprc := getProjectionRoundStakesState or in
    projection_round_stakes_getStake nprc = projection_round_stakes_getStake oprc /\
    projection_round_stakes_getRecoveredStake nprc = projection_round_stakes_getRecoveredStake oprc /\
    projection_round_stakes_getUnused nprc = msgValue ol + PROXY_FEE ol /\
    projection_round_stakes_getIsValidatorStakeCompleted nprc =
        projection_round_stakes_getIsValidatorStakeCompleted oprc /\
    projection_round_stakes_getRewards nprc = projection_round_stakes_getRewards oprc /\
    projection_round_stakes_getValidatorStake nprc =
        projection_round_stakes_getValidatorStake oprc /\
    projection_round_stakes_getHandledStakesAndRewards nprc =
    projection_round_stakes_getHandledStakesAndRewards oprc.

Definition projection_round_stakes_on_rotate_rounds_condition
    (l : Ledger) (r : RoundsBase_ι_Round) :=
    rotate_round_conditions_full l ticktockCalled /\
    r = round0 l /\
    poolClosed l = false /\
    isValidatorInRound l r = true.

Definition projection_round_stakes_on_rotate_rounds_move
(ol nl : Ledger) (or nr : RoundsBase_ι_Round) :=
    projection_round_stakes_on_rotate_rounds_condition ol or /\
    roundsSame or nr /\
    let nprc := getProjectionRoundStakesState nr in
    let oprc := getProjectionRoundStakesState or in
    projection_round_stakes_getStake nprc = projection_round_stakes_getStake oprc /\
    projection_round_stakes_getRecoveredStake nprc = projection_round_stakes_getRecoveredStake oprc /\
    projection_round_stakes_getUnused nprc = projection_round_stakes_getUnused oprc /\
    projection_round_stakes_getIsValidatorStakeCompleted nprc =
        projection_round_stakes_getIsValidatorStakeCompleted oprc /\
    projection_round_stakes_getRewards nprc = projection_round_stakes_getRewards oprc /\
    projection_round_stakes_getValidatorStake nprc = stakeSum (validatorStake ol or) /\
    projection_round_stakes_getHandledStakesAndRewards nprc =
    projection_round_stakes_getHandledStakesAndRewards oprc.

End Round_Stakes_conditions.

author: Pruvendo


text:
(* SPDX-License-Identifier: GPL-2.0 *)
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import ZSet.
Require Import ListLemma2.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import AuxStateDataType.
Require Import RealParams.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import LayerCalculusLemma.
Require Import TacticsForTesting.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.

Require Import TrapDispatcher.Spec.
Require Import RData.
Require Import Constants.
Require Import FaultHandler.Layer.
Require Import TrapDispatcher.Layer.
Require Import HypsecCommLib.

Local Open Scope Z_scope.
Local Opaque Z.add Z.mul Z.div Z.shiftl Z.shiftr Z.land Z.lor.

Section TrapDispatcherProofHigh.

  Local Open Scope string_scope.
  Local Open Scope Z_scope.

  Context `{real_params: RealParams}.

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

  Notation HDATAOps := (cdata (cdata_ops := TrapDispatcher_ops) HDATA).
  Notation LDATAOps := (cdata (cdata_ops := FaultHandler_ops) HDATA).

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.

    Record relate_RData (f:meminj) (hadt: HDATA) (ladt: LDATA) :=
      mkrelate_RData {
          id_rel: hadt = ladt
        }.

    Inductive match_RData: stencil -> HDATA -> mem -> meminj -> Prop :=
    | MATCH_RDATA: forall habd m f s, match_RData s habd m f.

    Local Hint Resolve MATCH_RDATA.

    Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
      {
        relate_AbData s f d1 d2 := relate_RData f d1 d2;
        match_AbData s d1 m f := match_RData s d1 m f;
        new_glbl := nil
      }.

    Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
    Proof.
      constructor; intros; simpl; trivial.
      constructor; inv H; trivial.
    Qed.

    Section FreshPrim.

      Lemma host_hvc_dispatcher_spec_exists:
        forall habd habd' labd  f
               (Hspec: host_hvc_dispatcher_spec  habd = Some habd')
               (Hrel: relate_RData f habd labd),
          exists labd', host_hvc_dispatcher_spec  labd = Some labd' /\ relate_RData f habd' labd'.
        Proof.
          intros. inv Hrel; subst.
          eexists; split. eassumption.
          constructor; reflexivity.
        Qed.

      Lemma host_hvc_dispatcher_spec_ref:
        compatsim (crel RData RData) (gensem host_hvc_dispatcher_spec) host_hvc_dispatcher_spec_low.
      Proof.
        Opaque host_hvc_dispatcher_spec.
        compatsim_simpl (@match_RData).
        exploit host_hvc_dispatcher_spec_exists; eauto 1;
        intros (labd' & Hspec & Hrel).
        refine_split; repeat (try econstructor; eauto).
      Qed.

      Lemma vm_exit_dispatcher_spec_exists:
        forall habd habd' labd vmid vcpuid res f
               (Hspec: vm_exit_dispatcher_spec vmid vcpuid habd = Some (habd', res))
               (Hrel: relate_RData f habd labd),
          exists labd', vm_exit_dispatcher_spec vmid vcpuid labd = Some (labd', res) /\ relate_RData f habd' labd'.
        Proof.
          intros. inv Hrel; subst.
          eexists; split. eassumption.
          constructor; reflexivity.
        Qed.

      Lemma vm_exit_dispatcher_spec_ref:
        compatsim (crel RData RData) (gensem vm_exit_dispatcher_spec) vm_exit_dispatcher_spec_low.
      Proof.
        Opaque vm_exit_dispatcher_spec.
        compatsim_simpl (@match_RData).
        exploit vm_exit_dispatcher_spec_exists; eauto 1;
        intros (labd' & Hspec & Hrel).
        refine_split; repeat (try econstructor; eauto).
      Qed.

    End FreshPrim.

  End WITHMEM.

End TrapDispatcherProofHigh.

author: VeriGu

repo: VRM-proof

save_path: github-repos/coq/VeriGu-VRM-proof


text:
Require Import Problem.

Theorem solution: task.
Proof.
  unfold task.
  reflexivity.
Qed.

author: matonix

repo: topprover

save_path: github-repos/coq/matonix-topprover


text:
(* PUBLIC DOMAIN *)
Require Export Coq.Vectors.Vector.
Require Export Coq.Lists.List.
Require Import Bool.Bool.
Require Import Logic.FunctionalExtensionality.
Require Import Coq.Program.Wf.
Require Import Lia.

Inductive myeq (A : Type) (x : A) : A -> Type :=
| myeq_refl : myeq A x x.

Fixpoint myvec_comp_as {A B C} (f:B->C) (g:A->B) (n:nat) (t0: Vector.t A n) :
myeq _ (Vector.map f (Vector.map g t0))
(Vector.map (fun x=>(f(g x))) t0).
Proof.
destruct t0.
simpl.
reflexivity.
simpl.
rewrite -> myvec_comp_as.
reflexivity.
Defined.

Fixpoint vec_comp_as {A B C} (f:B->C) (g:A->B) (n:nat) (t0: Vector.t A n) :
Vector.map f (Vector.map g t0) =
Vector.map (fun x=>(f(g x))) t0.
Proof.
destruct t0.
simpl.
reflexivity.
simpl.
rewrite -> vec_comp_as.
reflexivity.
Defined.

Module VS.
Section sec0.
Definition SetVars  := nat.
Definition FuncSymb := nat.
Definition PredSymb := nat.
Record FSV := {
 fs : FuncSymb;
 fsv : nat;
}.
Record PSV := MPSV{
 ps : PredSymb;
 psv : nat;
}.
Check MPSV 0 0.
Notation A1Type:=Set.
Unset Elimination Schemes.
Inductive Terms : A1Type :=
| FVC :> SetVars -> Terms
| FSC (f:FSV) : (Vector.t Terms (fsv f)) -> Terms.
Set Elimination Schemes.
(*Formulas*)
Inductive Fo :=
|Atom (p:PSV) : (Vector.t Terms (psv p)) ->  Fo
|Bot :Fo
|Conj:Fo->Fo->Fo
|Disj:Fo->Fo->Fo
|Impl:Fo->Fo->Fo
|Fora(x:SetVars)(f:Fo): Fo
|Exis(x:SetVars)(f:Fo): Fo
.
(* Substitution *)

Fixpoint substT (t:Terms) (xi: SetVars) (u:Terms): Terms.
Proof.
destruct u.
2 : { refine (FSC _ _).
Check @Vector.map.
Check @Vector.map _ _ (substT t xi) _ t0.
exact ( @Vector.map _ _ (substT t xi) _ t0 ). }

{
(*Check my.beq_natP s xi.*)
destruct (PeanoNat.Nat.eqb s xi).
Print bool.
exact t.
exact s. }
(*Show Proof.*)
Defined.

Fixpoint isParamT (xi : SetVars) (t : Terms) {struct t} : bool :=
   match t with
   | FVC s => PeanoNat.Nat.eqb s xi
   | FSC f t0 => Vector.fold_left orb false (Vector.map (isParamT xi) t0)
   end.

Fixpoint isParamF (xi:SetVars) (f:Fo): bool.
Proof.
(*elim f; intros. *)
destruct f.
Show Proof.
Search "Exists".
exact (Vector.fold_left orb false (Vector.map (isParamT xi) t)).
exact false.
Show Proof.
exact (orb (isParamF xi f1) (isParamF xi f2)).
exact (orb (isParamF xi f1) (isParamF xi f2)).
exact (orb (isParamF xi f1) (isParamF xi f2)).
Show Proof.
exact (match (PeanoNat.Nat.eqb x xi) with
       | true => false
       | false => (isParamF xi f)
       end).
exact (match (PeanoNat.Nat.eqb x xi) with
       | true => false
       | false => (isParamF xi f)
       end).
Show Proof.
Defined.

Fixpoint substF (t:Terms) (xi: SetVars) (u : Fo): option Fo.
Proof.
pose(g := substT t xi).
pose(f := substF t xi).
destruct u.
refine (Some (Atom p _)).
exact (Vector.map g t0).
exact (Some Bot).
 exact (
 match (f u1),(f u2) with
 | Some f0,Some f1 => (Some (Conj f0 f1))
 | _,_ => None
 end).
 exact (
 match (f u1),(f u2) with
 | Some f0,Some f1 => (Some (Disj f0 f1))
 | _,_ => None
 end).
 exact (
 match (f u1),(f u2) with
 | Some f0,Some f1 => (Some (Impl f0 f1))
 | _,_ => None
 end).
(*destruct (isParamF xi (Fora x0 u)).*)
refine (match (isParamF xi (Fora x u)) with
| true => match (isParamT x t) with
          | true => match substF t xi u with
                    | Some q => Some (Fora x q)
                    | None => None
                    end
          | false => None
          end
| false => Some u end).
refine (match (isParamF xi (Fora x u)) with
| true => match (isParamT x t) with
          | true => match substF t xi u with
                    | Some q => Some (Exis x q)
                    | None => None
                    end
          | false => None
          end
| false => Some u end).
Defined.

Definition Top:Fo := Impl Bot Bot.

Notation " x --> y ":=(Impl x y) (at level 80).
(*
Notation " u '[' t >> xi ] ":=(substT t xi u ) (at level 10).
Set Warnings "-notation-overridden".
Notation " ph [ t | xi ] ":=(substF t xi ph ) (at level 10).
(*Set Warnings "default".*)
Check fun (t:Terms) (x:SetVars) => ( t [ t >> x ]).
Check fun (t:Terms) (x:SetVars) (ph:Fo) => ( ph [ t | x ] ).
*)

Open Scope list_scope.
Print List.In.
Locate "+".
Print sum.
Definition InL { A : Type } :=
fix InL (a : A) (l : list A) {struct l} : Type :=
  match l with
  | Datatypes.nil => False
  | b :: m => (sum (b = a) (InL a m))
  end.

Inductive PR (axi:list Fo) : Fo -> Type :=
| hyp (A : Fo): (InL A axi)-> @PR axi A
| a1 (A B: Fo) : @PR axi (Impl A (Impl B A))
| a2 (A B C: Fo) : @PR axi ((A-->(B-->C))-->((A-->B)-->(A-->C)))
| a12 (ph: Fo) (t:Terms) (xi:SetVars)
: @PR axi (match (substF t xi ph) with
      | Some q => (Impl (Fora xi ph) q)
      | None => Top
      end)
| b1 (ps ph: Fo) (xi:SetVars) (H:isParamF xi ps = false):
@PR axi (Impl (Fora xi (Impl ps ph)) (Impl ps (Fora xi ph)) )
| MP (A B: Fo) : (@PR axi A)->(@PR axi (Impl A B))->(@PR axi B)
| GEN (A : Fo) (xi:SetVars): (@PR axi A)->(@PR axi (Fora xi A))
.

Check @PR.
Definition AtoA (A:Fo) : PR (List.nil) (A-->A).
Proof.
apply (MP nil (A-->(A-->A)) _).
apply a1.
apply (MP nil (A-->((A-->A)-->A)) _).
apply a1.
apply a2.
Defined.

Definition B1 (ps ph:Fo) (xi:SetVars) (H:isParamF xi ps = false):
 PR nil (ps --> ph) -> PR nil (ps --> Fora xi ph).
Proof.
intro q.
apply (MP nil (Fora xi (ps --> ph))).
+ apply GEN.
  exact q.
+ apply (b1 _).
  exact H.
Defined.

Definition gen (A:Fo) (xi:SetVars) (*Generalization from Bernay's rule*)
: PR nil (A) -> PR nil (Fora xi A).
Proof.
intro q.
apply (MP nil Top).
unfold Top.
exact (AtoA Bot).
apply (MP nil (Fora xi (Top --> A))).
* apply GEN.
  apply (MP nil A).
  + exact q.
  + apply a1.
* apply b1.
  trivial.
Defined.

Definition neg (f:Fo):= (Impl f Bot).

Definition a1i (A B : Fo)(l : list Fo):(PR l B)->(PR l (Impl A B)).
Proof.
intros x.
apply (MP l B).
exact x.
apply a1.
Defined.

Fixpoint weak (A F:Fo) (l :list Fo) (x: (PR l F)) : (PR (A::l) F).
Proof.
destruct x.
apply hyp.
apply inr. (*or_intror *)
exact i.
apply a1.
apply a2.
apply a12.
apply b1.
assumption.
apply (@MP _ A0).
apply weak.
exact x1.
apply weak.
exact x2.
apply GEN. (* Order is not important! *)
apply weak. (* Order is not important! *)
exact x.
Defined.

Fixpoint weaken (F:Fo) (li l :list Fo) (x: (PR l F)) {struct li}: (PR (li ++ l) F).
Proof.
destruct li.
simpl.
exact x.
simpl.
simple refine (@weak f F (li ++ l) _).
apply weaken.
exact x.
Defined.

(*Export List Notations.*)
Fixpoint notGenWith (xi:SetVars)(l:list Fo)(B:Fo)(m:(PR l B)){struct m}:bool.
Proof.
destruct m.
exact true.
exact true.
exact true.
exact true.
exact true.
exact (andb (notGenWith xi l _ m1) (notGenWith xi l _ m2)).
exact (andb (negb (PeanoNat.Nat.eqb xi xi0)) (notGenWith xi l _ m) ).
Defined.
Check isParamF.
(*Check fun A B=> forall xi:SetVars, (true = isParamF xi A)->(notGenWith xi m).*)
Fixpoint HA xi : true = PeanoNat.Nat.eqb (xi) (xi).
Proof.
destruct xi.
reflexivity.
simpl.
exact (HA xi).
Defined.

Fixpoint ZX (xi:SetVars) :true = negb (PeanoNat.Nat.eqb xi xi) -> False.
Proof.
intro q.
destruct xi.
compute in q.
inversion q.
rewrite <- HA in q.
inversion q.
Defined.

Theorem lm (a b :bool)(G:true = (a && b) ): true = a.
Proof.
destruct a.
trivial.
inversion G.
Defined.

Theorem lm2 (a b :bool)(G:true = (a && b) ): true = b.
Proof.
destruct a.
trivial.
inversion G.
Defined.

Theorem N (rr:bool): (true=rr \/ rr=false).
Proof.
destruct rr; firstorder.
Defined.

Fixpoint Ded (A B:Fo)(il:list Fo)(m:(PR (cons A il) B))
(H:forall xi:SetVars, (true = isParamF xi A)->(true=notGenWith xi _ _ m))
{struct m}:(PR il (A-->B)).
Proof.
destruct m. (*as [i|i|i|i|i|i|i].*)
+ unfold In in i.
  simpl in i .
  destruct i .
  * rewrite <- e.
    pose (J:=weaken _ il nil (AtoA A )).
    rewrite app_nil_r in J.
    exact J.
(*exact (weaken _ il nil (AtoA A )).
apply weak.
exact (AtoA A ).
exfalso.*)
  * simpl in H.
    apply a1i.
    exact (hyp il _ i).
+ apply a1i.
  apply a1.
+ apply a1i.
  apply a2.
+ apply a1i.
  apply a12.
+ apply a1i.
  apply b1.
  trivial.
+ apply (MP _ (A-->A0)).
- simple refine (@Ded _ _ _ _ _).
  exact m1.
  intros xi H0.
  pose (W:=H xi H0).
  simpl in W.
  pose (J:=notGenWith xi (A :: il) A0 m1).
  try reflexivity.
  fold J.
  fold J in W.
  apply (lm _ _ W).
-
apply (MP _ (A-->(A0-->B))).
simple refine (@Ded _ _ _ _ _).
  exact m2.
  intros xi H0.
  pose (W:=H xi H0).
  simpl in W.
  apply (lm2 _ _ W).
(*Last part about GEN*)
apply a2.
+
apply (MP _ (Fora xi (A-->A0))).
apply GEN.
simple refine (@Ded _ _ _ _ _).
  exact m.
  intros xi0 H0.
  pose (W:=H xi0 H0).
  simpl in W.
* exact (lm2 _ _ W).
* simpl.
apply b1.
pose (r := isParamF xi A).
pose (U := H xi).
fold r in U |- *.
simpl in U.

destruct (N r).
pose (C:= lm _ _(U H0)).
exfalso.
exact (ZX _ C).
exact H0.
Show Proof.
Defined.

(*Fixpoint Ded (A B:Fo)(m:(PR (cons A nil) B)) *)

Definition lm3 (a b :bool)(A: true = a)(B: true = b):true = (a && b)
:=
 (if a as a0 return (true = a0 -> true = a0 && b)
  then
   fun _ : true = true =>
   (if b as b0 return (true = b0 -> true = true && b0)
    then fun _ : true = true => eq_refl
    else fun B0 : true = false => B0) B
  else
   fun A0 : true = false =>
   (if b as b0 return (true = b0 -> true = false && b0)
    then fun _ : true = true => A0
    else fun _ : true = false => A0) B) A.
(*destruct a,b.
reflexivity.
simpl.
exact B.
simpl.
exact A.
simpl.
exact A.
Show Proof.
Defined.*)

Fixpoint forClosed (A B:Fo)(m:(PR (cons A nil) B)):
(forall xi:SetVars, (false = isParamF xi A))
->
(forall xi:SetVars, (true = isParamF xi A)->(true=notGenWith xi _ _ m)).
Proof.
intros H xi Q.
destruct m; simpl; try reflexivity.
+ apply lm3.
  simple refine (@forClosed _ _ _ _ _ _); assumption.
  simple refine (@forClosed _ _ _ _ _ _); assumption.
+ apply lm3.
  2 : simple refine (@forClosed _ _ _ _ _ _); assumption.
  pose (U:=H xi).
  rewrite <- Q in U.
  exfalso.
  inversion U.
Show Proof.
Defined.

Fixpoint SimplDed (A B:Fo) (il: list Fo)(m:(PR (cons A il) B))
(NP:forall xi:SetVars, (false = isParamF xi A))
{struct m}:(PR il (A-->B)).
Proof.
simple refine (Ded _ _ _ _ _).
exact m.
intros xi H.
rewrite <- NP in H.
inversion H.
Defined.
End sec0.

(** Correctness theorem **)
(** for two-valued logic **)
Section cor.
Definition Omega := bool. (* Truth values*)
Context (X:Type).
(*Context (val:SetVars->X).*)
Context (fsI:forall(q:FSV),(Vector.t X (fsv q))->X).
(*Context (prI:forall(q:PSV),(Vector.t X (psv q))->Omega).*)
Context (prI:forall(q:PSV),(Vector.t X (psv q))->Prop).

Fixpoint teI (val:SetVars->X) (t:Terms): X.
Proof.
destruct t.
exact (val s).
refine (fsI f _).
simple refine (@Vector.map _ _ _ _ _).
2 : apply teI.
exact val.
exact t.
Show Proof.
Defined.
(*
Fixpoint foI (val:SetVars->X) (f:Fo): Omega.
Proof.
destruct f.
+ refine (prI p _).
  apply (Vector.map  (teI val)).
  exact t.
+ exact false.
+ exact ( andb (foI val f1) (foI val f2)).
+ exact (  orb (foI val f1) (foI val f2)).
+ exact (implb (foI val f1) (foI val f2)).
+  (*Infinite conjunction!!!*)
 Show Proof.
*)

(** (\pi + (\xi \mapsto ?) ) **)
Definition cng (val:SetVars -> X) (xi:SetVars) (m:X) :=
(fun r:SetVars =>
match Nat.eqb r xi with
| true => m
| false => (val r)
end).

Fixpoint foI (val:SetVars->X) (f:Fo): Prop.
Proof.
destruct f.
+ refine (prI p _).
  apply (@Vector.map Terms X (teI val)).
  exact t.
+ exact False.
+ exact ( and (foI val f1) (foI val f2)).
+ exact (  or (foI val f1) (foI val f2)).
+ exact ( (foI val f1) -> (foI val f2)).
+ exact (forall m:X, foI (cng val x m) f).
(*forall m:X, foI (fun r:SetVars =>
match Nat.eqb r x with
| true => m
| false => (val r)
end
) f*)
+ exact (exists m:X, foI (fun r:SetVars =>
match Nat.eqb r x with
| true => m
| false => (val r)
end
) f
).
Defined.

Definition ap {A B}{a0 a1:A} (f:A->B) (h:a0=a1):((f a0)=(f a1))
:= match h in (_ = y) return (f a0 = f y) with
   | eq_refl => eq_refl
   end.

Definition myap {A B}{a0 a1:A} (f:A->B) (h:myeq _ a0 a1):(myeq _ (f a0) (f a1)).
Proof.
destruct h.
constructor.
Show Proof.
Defined.

Lemma equal_a : forall (A B : Type) (f : A -> B) (a0 a1:A),
  (a0 = a1) -> f a0 = f a1.
Proof.
intros A B f a0 a1 r.
destruct r.
reflexivity.
Defined.

(* Measure for terms: the sum of all functional symbols and variables. *)
Definition meas:=
(fix meas (u : Terms) : nat :=
   match u with
   | FVC _ => 1
   | FSC f t0 =>
       @Vector.fold_left nat nat Nat.add 1 (fsv f)
         (@Vector.map Terms nat meas (fsv f) t0) + (fsv f)
   end).
Check Build_FSV 0 1.
Compute (meas (FSC (Build_FSV 0 1) (Vector.cons _ (FVC 0) 0 (Vector.nil _)))).

(*Program *)
Fixpoint qlem1 (t : Terms) (xi : SetVars) (pi : SetVars->X) (u :Terms)
:= match u with
   | FVC v => FVC (v+1)
   | FSC f H => FSC f (Vector.map (qlem1 t xi pi) H)
   end.

(*(v:SetVars)(f:FSV)(H:t Terms (fsv f))*)
(* lem1  (is not proven yet) *)
(*
Fixpoint lem1 (t : Terms) (xi : SetVars) (pi : SetVars->X) (u :Terms)
{struct u}
:
(teI pi (substT t xi u))=(teI (cng pi xi (teI pi t)) u).
Proof.
apply Terms_ind.
Check Terms_ind. *)
Check True.

Theorem myfe :forall (A B : Type) (f g : A -> B),
(forall x : A, myeq _ (f x) (g x)) -> myeq _ f g.
Proof.
intros.
assert( KK : (forall x : A, f x = g x)).
intro x.
destruct (H x).
reflexivity.

pose(v:=(@functional_extensionality _ _ f g KK)).
destruct (@functional_extensionality _ _ f g KK).
reflexivity.
Defined.

Section Lem1.
Context (t : Terms).

Definition P(xi : SetVars) (pi : SetVars->X) (u :Terms)
:=(teI pi (substT t xi u))=(teI (cng pi xi (teI pi t)) u).

(**
Local Open Scope vector.**)
Inductive InV {A} (a:A): forall {n}, Vector.t A n -> Type :=
 |In_cons_hd {m} (v: Vector.t A m): InV a (@Vector.cons A a m v)
 |In_cons_tl {m} x (v: Vector.t A m): InV a v -> InV a (@Vector.cons A x m v).

Definition foma := @Vector.fold_left.
(* \u0418\u0437\u043c\u0435\u0440\u0435\u043d\u0438\u0435 - \u043a\u043e\u0434\u0438\u0440\u043e\u0432\u0430\u043d\u0438\u0435 \u0442\u0435\u0440\u043c\u043e\u0432 \u0430\u0440\u0438\u0444\u043c\u0435\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0435 x,y,z |-> c(x,y,z)*)
(* \u041d\u0430\u0434\u043e \u043f\u0440\u0438\u0434\u0443\u043c\u0430\u0442\u044c wf-\u043e\u0442\u043d\u043e\u0448\u0435\u043d\u0438\u0435 \u043d\u0430 \u0442\u0435\u0440\u043c\u0430\u0445 *)
(* x is less than y if ... *)
Definition rela : forall (x y:Terms), Prop.
Proof.
fix rela 2.
intros x y.
destruct y.
+ exact False.
+ refine (or _ _).
  exact (Vector.In x t0).
  simple refine (@Vector.fold_left Terms Prop _ False (fsv f) t0).
  intros Q e.
  exact (or Q (rela x e)).
Defined.

Definition snglV {A} (a:A) := Vector.cons A a 0 (Vector.nil A).

Require Import Arith Omega.
From Equations Require Import Equations.
Require Import Equations.Subterm.
Derive Signature Subterm for vector.
(*Derive Signature Subterm for Terms.*)
Section equ.
Context (*u :Terms*) (xi : SetVars)(pi : SetVars->X).

Equations mid (u : Terms) :
option ((teI pi (substT t xi u))=(teI (cng pi xi (teI pi t)) u)) :=
(*  mid n by rec n lt := *)
  mid (FVC s) := Some
      (let b := s =? xi in
       let ek : (s =? xi) = b := eq_refl in
       (if b as b0
         return
           ((s =? xi) = b0 ->
            teI pi (if b0 then t else s) = (if b0 then teI pi t else pi s))
        then fun _ : (s =? xi) = true => eq_refl
        else fun _ : (s =? xi) = false => eq_refl) ek)
; mid (FSC f v) := None
(*  mid (S (S n')) := S (mid n');
   mid (S n') := S (mid n') *)
.
End equ.
(*Equations mid (n : nat) : nat :=
  mid n by rec n lt :=
  mid 0 := 0;
  mid (S (S n')) := S (mid n');
  mid (S n') := S (mid n').*)

(* page 136 of the book *)
Definition lem1 : forall (u :Terms) (xi : SetVars) (pi : SetVars->X) ,
(teI pi (substT t xi u))=(teI (cng pi xi (teI pi t)) u).
Proof.
fix lem1 1.
intros.
destruct u as [s|f] .
+ simpl.
  unfold cng.
  destruct (Nat.eqb s xi) eqn:ek. (* fsI as [H1|H2].*)
  * reflexivity.
  * simpl.
    reflexivity.
Show Proof.
+
  simpl. (* fsI teI *)
  destruct f.
  simpl.
  apply ap.

  simpl in t0.

  pose (g:= (@vec_comp_as _ _ _ (teI pi) (substT t xi) _ t0)).
  rewrite -> g.
(*Check (@vec_comp_as _ _ _ (teI ) (cng pi xi (teI pi t)) _ ).
  pose (g:= (@vec_comp_as _ _ _ (teI pi) (substT t xi) _ t0)).
  rewrite -> g.*)

pose (Y:=fun wm => @Vector.map Terms X wm fsv0 t0).
pose (a1:=(fun x : Terms => teI pi (substT t xi x))).
pose (a2:=(teI (cng pi xi (teI pi t)))).
pose (Y1:= Y a1).
pose (Y2:= Y a2).
unfold Y in Y1.
unfold Y in Y2.
fold Y1 Y2 in |- *.
apply (@ap _ _ a1 a2 Y).
unfold a1, a2 in |- *.
apply functional_extensionality.
    intro x.

refine (lem1 x xi pi ).
Show Proof.
Abort.
End Lem1.

(* lem1  is not proven yet! *)

Fixpoint correct (f:Fo) (l:list Fo) (val:SetVars->X) (m:PR l f)
(lfi : forall h:Fo, (InL h l)->(foI val h)) {struct m}: foI val f.
Proof.
destruct m (* eqn: meq *).
+ exact (lfi A i).
+ simpl.
  intros a b.
  exact a.
+ simpl.
  intros a b c.
  exact (a c (b c)).
+ destruct (substF t xi ph) eqn: j.
  2 : {simpl. trivial. }
  apply (correct _ l).
  2 : {assumption. }
  simpl.
pose (Z:=(@Ded (Fora xi ph) f l )).
simple refine (Z _ _ ).
(*
  pose (W:= lfi f).
  destruct (Nat.eqb r xi).
  simpl in H.
  exact H.
  unfold foI.
  simpl.
*)
Admitted.

End cor.
(* Definition ACK : list Fo := . *)

End VS.

(*Theorem AA (a:nat):nat.
elim a;
[> revert a | idtac 1].
elim a;
[> idtac 1 | idtac 1].
destruct a.
(*Unfocus.*)
[> idtac 1 | idtac 1].*)

author: georgydunaev

repo: TRASH

save_path: github-repos/coq/georgydunaev-TRASH


Require Import Crypto.Specific.Framework.RawCurveParameters.
Require Import Crypto.Util.LetIn.

(***
Modulus : 2^166 - 5
Base: 23 + 5/7
***)

Definition curve : CurveParameters :=
  {|
    sz := 7%nat;
    base := 23 + 5/7;
    bitwidth := 32;
    s := 2^166;
    c := [(1, 5)];
    carry_chains := Some [seq 0 (pred 7); [0; 1]]%nat;

    a24 := None;
    coef_div_modulus := Some 2%nat;

    goldilocks := None;
    karatsuba := None;
    montgomery := false;
    freeze := Some true;
    ladderstep := false;

    mul_code := None;

    square_code := None;

    upper_bound_of_exponent_loose := None;
    upper_bound_of_exponent_tight := None;
    allowable_bit_widths := None;
    freeze_extra_allowable_bit_widths := None;
    modinv_fuel := None
  |}.

Ltac extra_prove_mul_eq _ := idtac.
Ltac extra_prove_square_eq _ := idtac.