text:
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.ZArith.ZArith.
Require Import bedrock2.Syntax.
Require Import Crypto.Arithmetic.Core.
Require Import Crypto.Spec.ModularArithmetic.
Require Import Crypto.Arithmetic.ModularArithmeticTheorems.
Require Import Crypto.Bedrock.Specs.Field.
Require Import Crypto.Bedrock.Field.Common.Types.
Require Import Crypto.Bedrock.Field.Common.Util.
Require Import Crypto.Bedrock.Field.Common.Arrays.ByteBounds.
Require Import Crypto.Bedrock.Field.Common.Names.VarnameGenerator.
Require Import Crypto.Bedrock.Field.Synthesis.New.ComputedOp.
Require Import Crypto.Bedrock.Field.Synthesis.New.Signature.
Require Import Crypto.Bedrock.Field.Translation.Parameters.Defaults.
Require Import Crypto.Bedrock.Field.Translation.Proofs.Func.
Require Import Crypto.BoundsPipeline.
Require Import Crypto.COperationSpecifications.
Require Import Crypto.PushButtonSynthesis.UnsaturatedSolinas.
Require Import Crypto.Language.API.
Require Import Crypto.UnsaturatedSolinasHeuristics.
Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Tactics.SpecializeBy.
Import ListNotations API.Compilers Types.Notations.

Class unsaturated_solinas_ops
  {width BW word mem locals env ext_spec varname_gen error}
  {parameters_sentinel : @parameters width BW word mem locals env ext_spec varname_gen error}
  {field_parameters : FieldParameters}
  {n s c} : Type :=
  { mul_op :
      computed_op
        (UnsaturatedSolinas.carry_mul n s c width) Field.mul
        list_binop_insizes list_binop_outsizes (list_binop_inlengths n);
    add_op :
      computed_op
        (UnsaturatedSolinas.add n s c width) Field.add
        list_binop_insizes list_binop_outsizes (list_binop_inlengths n);
    sub_op :
      computed_op
        (UnsaturatedSolinas.sub n s c width) Field.sub
        list_binop_insizes list_binop_outsizes (list_binop_inlengths n);
    opp_op :
      computed_op
        (UnsaturatedSolinas.opp n s c width) Field.opp
        list_unop_insizes list_unop_outsizes (list_unop_inlengths n);
    square_op :
      computed_op
        (UnsaturatedSolinas.carry_square n s c width)
        Field.square
        list_unop_insizes list_unop_outsizes (list_unop_inlengths n);
    scmula24_op :
      computed_op
        (UnsaturatedSolinas.carry_scmul_const n s c width
                                              (F.to_Z a24)) Field.scmula24
        list_unop_insizes list_unop_outsizes (list_unop_inlengths n);
    felem_copy_op :
      computed_op
        (UnsaturatedSolinas.copy n width) Field.felem_copy
        list_unop_insizes list_unop_outsizes (list_unop_inlengths n);
    from_word_op :
      computed_op
        (UnsaturatedSolinas.encode_word n s c width)
        Field.from_word
        from_word_insizes from_word_outsizes from_word_inlengths;
    from_bytes_op :
      computed_op
        (UnsaturatedSolinas.from_bytes n s c width)
        Field.from_bytes
        from_bytes_insizes from_bytes_outsizes (from_bytes_inlengths
                                                  (n_bytes s));
    to_bytes_op :
      computed_op
        (UnsaturatedSolinas.to_bytes n s c width)
        Field.to_bytes
        to_bytes_insizes to_bytes_outsizes (to_bytes_inlengths n);
  }.
Arguments unsaturated_solinas_ops {_ _ _ _ _ _ _ _ _ _ _} n.

(** We need to tell [check_args] that we are requesting these functions in order to get the relevant properties out *)
Notation necessary_requests := ["to_bytes"; "from_bytes"]%string (only parsing).

Section UnsaturatedSolinas.
  Context
  {width BW word mem locals env ext_spec error}
  {parameters_sentinel : @parameters width BW word mem locals env ext_spec default_varname_gen error}
  {field_parameters : FieldParameters}
  {ok : Types.ok}.

  Context (n : nat) (s : Z) (c : list (Z * Z))
          (M_eq : M = m s c)
          (check_args_ok :
             check_args n s c width necessary_requests (ErrorT.Success tt)
             = ErrorT.Success tt)
          (* TODO: prove a transitivity lemma for list_Z_tighter_than and use
             loose_bounds_tighter_than to prove tight_bounds_tighter_than *)
          (tight_bounds_tighter_than:
             list_Z_tighter_than (tight_bounds n s c)
                                 (@MaxBounds.max_bounds width n))
          (loose_bounds_tighter_than:
             list_Z_tighter_than (loose_bounds n s c)
                                 (@MaxBounds.max_bounds width n)).

  Context (ops : unsaturated_solinas_ops n s c)
          mul_func add_func sub_func opp_func square_func
          scmula24_func felem_copy_func from_word_func from_bytes_func to_bytes_func
          (mul_func_eq : mul_func = b2_func mul_op)
          (add_func_eq : add_func = b2_func add_op)
          (sub_func_eq : sub_func = b2_func sub_op)
          (opp_func_eq : opp_func = b2_func opp_op)
          (square_func_eq : square_func = b2_func square_op)
          (scmula24_func_eq : scmula24_func = b2_func scmula24_op)
          (felem_copy_func_eq : felem_copy_func = b2_func felem_copy_op)
          (from_word_func_eq : from_word_func = b2_func from_word_op)
          (from_bytes_func_eq : from_bytes_func = b2_func from_bytes_op)
          (to_bytes_func_eq : to_bytes_func = b2_func to_bytes_op).
  Local Notation weight :=
    (ModOps.weight (QArith_base.Qnum (limbwidth n s c))
                   (Z.pos (QArith_base.Qden (limbwidth n s c))))
      (only parsing).
  (* Note: annoyingly, prime_bytes_bounds is an option type, unlike loose_bounds
     or tight_bounds, so we have to reconstruct it to match list_Z_bounded_by *)
  Local Notation prime_bytes_bounds_value :=
    (map (fun v : Z => Some {| ZRange.lower := 0; ZRange.upper := v |})
         (prime_bytes_upperbound_list s)).
  Local Instance field_representation : FieldRepresentation
    := field_representation
         n (n_bytes s) weight (list (option ZRange.zrange))
         (UnsaturatedSolinasHeuristics.loose_bounds n s c)
         (UnsaturatedSolinasHeuristics.tight_bounds n s c)
         (prime_bytes_bounds_value)
         list_Z_bounded_by (fun x => x).

  Local Ltac specialize_correctness_hyp Hcorrect :=
    cbv [feval feval_bytes bounded_by bytes_in_bounds Field.loose_bounds
               field_representation Signature.field_representation
               Representation.frep Representation.eval_bytes
               Representation.eval_words
               bin_model bin_xbounds bin_ybounds
               un_model un_xbounds
               ] in *;
    (* if prime_bytes_bounds, simplify first *)
    try match type of Hcorrect with
        | context [list_Z_bounded_by (map ?f ?x)] =>
          change (map f x) with prime_bytes_bounds_value in Hcorrect
        end;
    lazymatch type of Hcorrect with
    | forall x y, ?Px x -> ?Py y -> _ =>
      match goal with
        | Hx : Px ?x, Hy : Py ?y |- _ =>
          specialize (Hcorrect x y Hx Hy)
      end
    | forall x, ?Px x -> _ =>
      match goal with
        | Hx : Px ?x |- _ =>
          specialize (Hcorrect x Hx)
      end
    end.

  Lemma loose_bounds_eq : Field.loose_bounds = loose_bounds n s c.
  Proof using Type. reflexivity. Qed.
  Lemma tight_bounds_eq : Field.tight_bounds = tight_bounds n s c.
  Proof using Type. reflexivity. Qed.

  (* TODO: move to coqutil.Datatypes.List *)
  Lemma Forall_repeat : forall {A} (R : A -> Prop) n x,
    R x -> Forall R (repeat x n).
  Proof using. clear.
    intros; induction n; intros; cbn [repeat];
    constructor; auto.
  Qed.

  Lemma byte_bounds_tighter_than :
    list_Z_tighter_than prime_bytes_bounds_value
                        (byte_bounds (n_bytes s)).
  Proof using Type.
    clear. cbv [prime_bytes_upperbound_list].
    apply tighter_than_if_upper_bounded_by;
    eauto using Forall_repeat, partition_bounded_by.
  Qed.

  Lemma length_byte_bounds :
    length prime_bytes_bounds_value = encoded_felem_size_in_bytes.
  Proof using Type.
    autorewrite with distr_length.
    apply length_prime_bytes_upperbound_list.
  Qed.

  Lemma modulus_fits_in_bytes :
    (0 < m s c <= ModOps.weight 8 1 (n_bytes s))%Z.
  Proof using check_args_ok.
    (* Extract information from check_args *)
    clear - check_args_ok. apply use_curve_good in check_args_ok; rename check_args_ok into H.
    vm_compute Primitives.request_present in H.
    destruct_head'_and.
    specialize_by reflexivity.
    match goal with
    | H : s = ModOps.weight _ _ n |- _ =>
      pose proof H;
      apply Freeze.bytes_n_big in H
    end;
      cbv [m n_bytes]; auto using limbwidth_good with zarith.
  Qed.

  Local Hint Resolve
        relax_valid func_eq
        inname_gen_varname_gen_disjoint
        outname_gen_varname_gen_disjoint
        length_tight_bounds length_loose_bounds
        length_byte_bounds
        byte_bounds_tighter_than
    : helpers.

  Local Hint Unfold
        Solinas.selectznz_correct
        Solinas.from_bytes_correct
        Solinas.encode_word_correct
        Solinas.to_bytes_correct
        Solinas.carry_mul_correct
        Solinas.carry_square_correct
        Solinas.carry_scmul_const_correct
        Solinas.add_correct
        Solinas.sub_correct
        Solinas.opp_correct
        Solinas.carry_correct
        Solinas.zero_correct
        Solinas.one_correct : solinas_specs.

  (* Extra lemma for to_bytes because the COperationSpecifications spec does not
     include bounds *)
  Lemma partition_bounded_by_prime_bytes_bounds x :
    (0 <= x < m s c)%Z ->
    list_Z_bounded_by
      prime_bytes_bounds_value
      (Partition.Partition.partition
         (ModOps.weight 8 1) (n_bytes s) x).
  Proof using check_args_ok.
    clear - check_args_ok. intros.
    apply use_curve_good in check_args_ok.
    vm_compute Primitives.request_present in check_args_ok.
    destruct_head' and.
    specialize_by reflexivity.
    assert (0 <= x < s)%Z as xbounds
        by (cbv [m] in *; auto with zarith).
    cbv [prime_bytes_upperbound_list].
    assert (exists lg2s, s = 2 ^ lg2s)%Z as [lg2s ?]
      by (eexists;
          lazymatch goal with
            H : s = ModOps.weight _ _ _ |- _ =>
            cbv [ModOps.weight] in H; apply H
          end).
    subst s. apply partition_bounded_by_partition_ones.
    auto with zarith.
  Qed.

  (* We wrap the tactic in [once] so it doesn't take forever to fail *)
  Ltac handle_side_conditions :=
    once
      (lazymatch goal with
       | |- API.Wf (res ?op)
         => generalize (res op), (res_eq op);
            (* Kludge around auto being bad (COQBUG(https://github.com/coq/coq/issues/14190)) and eauto not respecting Hint Opaque *)
            typeclasses eauto with wf_op_cache;
            let e := lazymatch goal with | |- forall res, ?e = _ -> API.Wf _ => e end in
            idtac "Warning: Falling back to manually proving pipeline well-formedness for" e;
            PipelineTactics.prove_pipeline_wf ()
       | |- context [Field.tight_bounds] => rewrite tight_bounds_eq
       | |- context [Field.loose_bounds] => rewrite loose_bounds_eq
       | _ => idtac
       end;
       lazymatch goal with
       | |- context [expr.interp] =>
         cbv [expr.Interp] in *; autounfold with solinas_specs in *
       | _ => eauto with helpers
       end).

  Hint Resolve relax_list_Z_bounded_by partition_bounded_by : bounds.

  Ltac simpl_map_unsigned :=
    lazymatch goal with
    | |- context [map Interface.word.unsigned
                      (map Interface.word.of_Z _)] =>
      rewrite map_unsigned_of_Z;
      erewrite MaxBounds.map_word_wrap_bounded
        by eauto with bounds
    | |- context [map Byte.byte.unsigned
                      (map Byte.byte.of_Z _)] =>
      rewrite byte_map_unsigned_of_Z;
      erewrite map_byte_wrap_bounded
        by eauto with bounds
    end.
  Ltac FtoZ :=
    apply F.eq_of_Z_iff; rewrite ?F.to_Z_of_Z;
    cbv [M] in M_eq; rewrite ?M_eq; pull_Zmod.

  Ltac loosen_bounds := lazymatch goal with
  | |- forall _, list_Z_bounded_by ?thesebounds _ -> _ => simpl; intros; eapply relax_list_Z_bounded_by; [| eauto];
    simpl; try apply tight_bounds_tighter_than; try apply loose_bounds_tighter_than
  | _ => idtac
  end.

  Ltac bounds_length := simpl; intros; erewrite length_list_Z_bounded_by; eauto; try apply length_tight_bounds; try apply length_loose_bounds.

  Lemma mul_func_correct :
    valid_func (res mul_op _) ->
    forall functions,
      spec_of_BinOp bin_mul ((mul,mul_func) :: functions).
  Proof using M_eq check_args_ok mul_func_eq ok
        tight_bounds_tighter_than.
    intros. cbv [spec_of_BinOp bin_mul]. rewrite mul_func_eq.
    pose proof carry_mul_correct
         _ _ _ _ _ ltac:(eassumption) _ (res_eq mul_op)
      as Hcorrect.
    eapply list_binop_correct with (res:=res mul_op);
    handle_side_conditions; [ | | loosen_bounds | bounds_length ].
    { (* output *value* is correct *)
      intros.
      specialize_correctness_hyp Hcorrect.
      destruct Hcorrect. simpl_map_unsigned.
      FtoZ; congruence. }
    { (* output *bounds* are correct *)
      intros. apply Hcorrect; auto. }
  Qed.

  Lemma square_func_correct :
    valid_func (res square_op _) ->
    forall functions,
      spec_of_UnOp un_square ((square,square_func) :: functions).
  Proof using M_eq check_args_ok ok square_func_eq
        tight_bounds_tighter_than.
    intros. cbv [spec_of_UnOp un_square]. rewrite square_func_eq.
    pose proof carry_square_correct
         _ _ _ _ _ ltac:(eassumption) _ (res_eq square_op)
      as Hcorrect.
    eapply list_unop_correct with (res:=res square_op);
      handle_side_conditions; [ | | loosen_bounds| bounds_length ].
    { (* output *value* is correct *)
      intros. specialize_correctness_hyp Hcorrect.
      destruct Hcorrect. simpl_map_unsigned.
      rewrite F.pow_2_r. FtoZ; congruence. }
    { (* output *bounds* are correct *)
      intros. apply Hcorrect; auto. }
  Qed.

  Lemma add_func_correct :
    valid_func (res add_op _) ->
    forall functions,
      spec_of_BinOp bin_add ((Field.add,add_func) :: functions).
  Proof using M_eq check_args_ok add_func_eq ok
        tight_bounds_tighter_than loose_bounds_tighter_than.
    intros. cbv [spec_of_BinOp bin_add]. rewrite add_func_eq.
    pose proof add_correct
         _ _ _ _ _ ltac:(eassumption) _ (res_eq add_op)
      as Hcorrect.
    eapply list_binop_correct with (res:=res add_op);
    handle_side_conditions; [ | | loosen_bounds | bounds_length ].
    { (* output *value* is correct *)
      intros.
      specialize_correctness_hyp Hcorrect.
      destruct Hcorrect. simpl_map_unsigned.
      FtoZ; congruence. }
    { (* output *bounds* are correct *)
      intros. apply Hcorrect; auto. }
  Qed.

  Lemma sub_func_correct :
    valid_func (res sub_op _) ->
    forall functions,
      spec_of_BinOp bin_sub ((Field.sub,sub_func) :: functions).
  Proof using M_eq check_args_ok sub_func_eq ok
        tight_bounds_tighter_than loose_bounds_tighter_than.
    intros. cbv [spec_of_BinOp bin_sub]. rewrite sub_func_eq.
    pose proof sub_correct
         _ _ _ _ _ ltac:(eassumption) _ (res_eq sub_op)
      as Hcorrect.
    eapply list_binop_correct with (res:=res sub_op);
    handle_side_conditions; [ | | loosen_bounds | bounds_length ].
    { (* output *value* is correct *)
      intros.
      specialize_correctness_hyp Hcorrect.
      destruct Hcorrect. simpl_map_unsigned.
      rewrite <-F.of_Z_sub. FtoZ. congruence. }
    { (* output *bounds* are correct *)
      intros. apply Hcorrect; auto. }
  Qed.

  Lemma opp_func_correct :
    valid_func (res opp_op _) ->
    forall functions,
      spec_of_UnOp un_opp ((Field.opp, opp_func) :: functions).
  Proof using M_eq check_args_ok loose_bounds_tighter_than opp_func_eq ok.
    intros. cbv [spec_of_UnOp un_opp]. rewrite opp_func_eq.
    pose proof opp_correct
         _ _ _ _ _ ltac:(eassumption) _ (res_eq opp_op)
      as Hcorrect.

    eapply list_unop_correct with (res:=res opp_op);
      handle_side_conditions; [ | | loosen_bounds | bounds_length ].
    { (* output *value* is correct *)
      intros. specialize_correctness_hyp Hcorrect.
      destruct Hcorrect. simpl_map_unsigned.
      FtoZ. rewrite Z.sub_0_l; congruence. }
    { (* output *bounds* are correct *)
      intros. apply Hcorrect; auto. }
  Qed.

  Lemma scmula24_func_correct :
    valid_func (res scmula24_op _) ->
    forall functions,
      spec_of_UnOp un_scmula24 ((scmula24, scmula24_func) :: functions).
  Proof using M_eq check_args_ok ok scmula24_func_eq
        tight_bounds_tighter_than.
    intros. cbv [spec_of_UnOp un_scmula24]. rewrite scmula24_func_eq.
    pose proof carry_scmul_const_correct
         _ _ _ _ _ (ltac:(eassumption)) (F.to_Z a24) _
         (res_eq scmula24_op)
      as Hcorrect.

    eapply list_unop_correct with (res:=res scmula24_op);
      handle_side_conditions; [ | | loosen_bounds | bounds_length ].
    { (* output *value* is correct *)
      intros. specialize_correctness_hyp Hcorrect.
      destruct Hcorrect. simpl_map_unsigned.
      FtoZ. congruence. }
    { (* output *bounds* are correct *)
      intros. apply Hcorrect; auto. }
  Qed.

  Lemma list_Z_bounded_by_unsigned (xs : list (@Interface.word.rep _ word)) :
    list_Z_bounded_by
      (Primitives.saturated_bounds (List.length xs) width)
      (map Interface.word.unsigned xs).
  Proof using parameters_sentinel ok.
    induction xs; cbn; [reflexivity|].
    eapply list_Z_bounded_by_cons; split; [|assumption].
    eapply Bool.andb_true_iff; split; eapply Z.leb_le;
    cbv [Primitives.word_bound]; cbn.
    { eapply Properties.word.unsigned_range. }
    { eapply Le.Z.le_sub_1_iff, Properties.word.unsigned_range. }
  Qed.

  Lemma felem_copy_func_correct :
    valid_func (res felem_copy_op _) ->
    forall functions,
      spec_of_felem_copy ((felem_copy, felem_copy_func) :: functions).
  Proof using M_eq check_args_ok ok felem_copy_func_eq
        tight_bounds_tighter_than parameters_sentinel ok
to_bytes_func_eq to_bytes_func sub_func_eq sub_func square_func_eq
square_func scmula24_func_eq scmula24_func opp_func_eq opp_func mul_func_eq
mul_func loose_bounds_tighter_than from_word_func_eq from_word_func
from_bytes_func_eq from_bytes_func add_func_eq.
    intros. cbv [spec_of_felem_copy]. rewrite felem_copy_func_eq.
    pose proof copy_correct _ _ _ _ _ ltac:(eassumption) _ (res_eq felem_copy_op)
      as Hcorrect.

    eapply felem_copy_correct;
      repeat handle_side_conditions; [ | ]; intros.
    { (* output *value* is correct *)
      unshelve erewrite (proj1 (Hcorrect _ _)); cycle 1.
      { rewrite map_map, List.map_ext_id; trivial; intros.
        rewrite ?Word.Interface.word.of_Z_unsigned; trivial. }
      { subst n. exact (list_Z_bounded_by_unsigned x). } }
    { (* output *bounds* are correct *)
      intros. apply Hcorrect; auto. }
  Qed.

  Lemma from_word_func_correct :
    valid_func (res from_word_op _) ->
    forall functions,
      spec_of_from_word ((from_word, from_word_func) :: functions).
  Proof using M_eq check_args_ok from_word_func_eq ok
        tight_bounds_tighter_than.
    intros. cbv [spec_of_from_word]. rewrite from_word_func_eq.
    epose proof encode_word_correct _ _ _ _ _ ltac:(eassumption) _ (res_eq from_word_op)
      as Hcorrect.
    cbv [expr.Interp] in *; autounfold with solinas_specs in *; cbn [ZRange.lower ZRange.upper] in *.

    eapply from_word_correct;
      repeat handle_side_conditions.
    { (* value *)
      intros.
      destruct (Hcorrect (Interface.word.unsigned w)); clear Hcorrect.
      { pose proof Properties.word.unsigned_range w.
        eapply Bool.andb_true_iff; split; eapply Zle_is_le_bool; Lia.lia. }
      rewrite <- M_eq in *; cbv [M] in *; eapply F.eq_of_Z_iff in H0.
      rewrite <-H0.
      unfold feval.
      unfold Signature.field_representation.
      unfold Representation.eval_words, Representation.frep.
      cbv [Representation.eval_words].
      Morphisms.f_equiv. Morphisms.f_equiv.
      rewrite map_unsigned_of_Z, List.map_ext_id; trivial.
      intros x Hx.
      eapply relax_list_Z_bounded_by, MaxBounds.max_bounds_range_iff in H1;
        try eapply tight_bounds_tighter_than; destruct H1.
      eapply List.Forall_In in H2; eauto.
      rewrite MakeAccessSizes.bits_per_word_eq_width in H2.
      unfold Interface.word.wrap; rewrite Z.mod_small; trivial. }
    { intros.
      destruct (Hcorrect (Interface.word.unsigned w)); clear Hcorrect.
      { pose proof Properties.word.unsigned_range w.
        eapply Bool.andb_true_iff; split; eapply Zle_is_le_bool; Lia.lia. }
      rewrite <- M_eq in *; cbv [M] in *; eapply F.eq_of_Z_iff in H0.
      trivial. }
    { eauto using relax_list_Z_bounded_by, tight_bounds_tighter_than. }
  Qed.

  Lemma from_bytes_func_correct :
    valid_func (res from_bytes_op _) ->
    forall functions,
      spec_of_from_bytes ((Field.from_bytes,from_bytes_func) :: functions).
  Proof using M_eq check_args_ok from_bytes_func_eq ok
        tight_bounds_tighter_than.
    intros. cbv [spec_of_from_bytes]. rewrite from_bytes_func_eq.
    pose proof UnsaturatedSolinas.from_bytes_correct
         _ _ _ _ _ ltac:(eassumption) _ (res_eq from_bytes_op) (eq_refl true)
      as Hcorrect.

    eapply Signature.from_bytes_correct with (res:=res from_bytes_op);
      handle_side_conditions; [ loosen_bounds | bounds_length | | | ].
    { intros. erewrite length_list_Z_bounded_by, length_byte_bounds; trivial. }
    { (* output *value* is correct *)
      intros. specialize_correctness_hyp Hcorrect.
      destruct Hcorrect.
      FtoZ. simpl_map_unsigned. congruence. }
    { (* output *bounds* are correct *)
      intros. apply Hcorrect; auto. }
  Qed.

  Lemma to_bytes_func_correct :
    valid_func (res to_bytes_op _) ->
    forall functions,
      spec_of_to_bytes ((Field.to_bytes, to_bytes_func) :: functions).
  Proof using M_eq check_args_ok ok to_bytes_func_eq.
    intros. cbv [spec_of_to_bytes]. rewrite to_bytes_func_eq.
    pose proof UnsaturatedSolinas.to_bytes_correct
         _ _ _ _ _ ltac:(eassumption) _ (res_eq to_bytes_op) (eq_refl true)
      as Hcorrect.

    eapply Signature.to_bytes_correct with (res:=res to_bytes_op);
      handle_side_conditions; [ | | | ].
    {
      intros. eapply relax_list_Z_bounded_by; [| eauto]. apply byte_bounds_tighter_than.
    }
    {
      intros. erewrite length_list_Z_bounded_by; [| eauto]. apply length_byte_bounds.
    }
    { (* output *value* is correct *)
      intros. specialize_correctness_hyp Hcorrect.
      rewrite Hcorrect.
      rewrite F.to_Z_of_Z, <-M_eq.
      reflexivity. }
    { (* output *bounds* are correct *)
      intros. rewrite Hcorrect by auto.
      cbn [bytes_in_bounds Representation.frep
                           Signature.field_representation].
      erewrite ByteBounds.byte_map_unsigned_of_Z,
      ByteBounds.map_byte_wrap_bounded
        by apply ByteBounds.partition_bounded_by.
      apply partition_bounded_by_prime_bytes_bounds.
      apply Z.mod_pos_bound.
      apply modulus_fits_in_bytes. }
  Qed.

End UnsaturatedSolinas.

(* Prototyping full pipeline: *)

Require Import Coq.Strings.String.
Require Import Crypto.Bedrock.Field.Translation.Proofs.ValidComputable.Func.

(* TODO: move somewhere common *)
Definition field_parameters_prefixed
           M_pos a24 (prefix: string) : FieldParameters :=
  Build_FieldParameters
    M_pos a24
    (prefix ++ "mul")
    (prefix ++ "add")
    (prefix ++ "sub")
    (prefix ++ "opp")
    (prefix ++ "square")
    (prefix ++ "scmula24")
    (prefix ++ "inv")
    (prefix ++ "from_bytes")
    (prefix ++ "to_bytes")
    (prefix ++ "select_znz")
    (prefix ++ "copy")
    (prefix ++ "from_word")
.

Import Coq.Program.Tactics.
Local Ltac begin_derive_bedrock2_func :=
  lazymatch goal with
  | |- context [spec_of_BinOp bin_mul] => rapply mul_func_correct
  | |- context [spec_of_UnOp un_square] => rapply square_func_correct
  | |- context [spec_of_BinOp bin_add] => rapply add_func_correct
  | |- context [spec_of_BinOp bin_sub] => rapply sub_func_correct
  | |- context [spec_of_UnOp un_opp] => rapply opp_func_correct
  | |- context [spec_of_UnOp un_scmula24] => rapply scmula24_func_correct
  | |- context [spec_of_from_bytes] => rapply from_bytes_func_correct
  | |- context [spec_of_to_bytes] => rapply to_bytes_func_correct
  | |- context [spec_of_felem_copy] => rapply felem_copy_func_correct
  | |- context [spec_of_from_word] => rapply from_word_func_correct
  end.

Ltac derive_bedrock2_func op :=
  begin_derive_bedrock2_func;
  (* this goal fills in the evar, so do it first for [abstract] to be happy *)
  try lazymatch goal with
      | |- _ = b2_func _ => vm_compute; reflexivity
      end;
  (* solve all the remaining goals *)
  lazymatch goal with
  | |- _ = @ErrorT.Success ?ErrT unit tt =>
    abstract (vm_cast_no_check (@eq_refl _ (@ErrorT.Success ErrT unit tt)))
  | |- list_Z_tighter_than _ _ =>
    abstract (vm_cast_no_check (@eq_refl bool true))
  | |- valid_func _ =>
    eapply valid_func_bool_iff;
    abstract vm_cast_no_check (eq_refl true)
  | |- _ = m _ _ => vm_compute; reflexivity
  | |- _ = default_varname_gen => vm_compute; reflexivity
  end.

(*
Require Import Crypto.Bedrock.Field.Translation.Parameters.Defaults64.

Section Tests.
  Definition n := 5%nat.
  Definition s := (2^255)%Z.
  Definition c := [(1, 19)]%Z.

  Existing Instances Defaults64.default_parameters default_parameters_ok.
  Definition prefix : string := "fe25519_"%string.

  Instance field_parameters : FieldParameters.
  Proof using Type.
    let M := (eval vm_compute in (Z.to_pos (m s c))) in
    (* Curve25519 "A" parameter (see section 4.1 of RFC 7748) *)
    let a := constr:(F.of_Z M 486662) in
    let prefix := constr:("fe25519_"%string) in
    eapply
      (field_parameters_prefixed
         M ((a - F.of_Z _ 2) / F.of_Z _ 4)%F prefix).
  Defined.

  Instance fe25519_ops : unsaturated_solinas_ops n s c.
  Proof using Type. Time constructor; make_computed_op. Defined.

  Derive fe25519_mul
         SuchThat (forall functions,
                      spec_of_BinOp bin_mul
                        (field_representation:=field_representation n s c)
                        (fe25519_mul :: functions))
         As fe25519_mul_correct.
  Proof. Time derive_bedrock2_func mul_op. Qed.

  Derive fe25519_square
         SuchThat (forall functions,
                      spec_of_UnOp un_square
                        (field_representation:=field_representation n s c)
                        (fe25519_square :: functions))
         As fe25519_square_correct.
  Proof. Time derive_bedrock2_func square_op. Qed.

  Derive fe25519_add
         SuchThat (forall functions,
                      spec_of_BinOp bin_add
                        (field_representation:=field_representation n s c)
                        (fe25519_add :: functions))
         As fe25519_add_correct.
  Proof. Time derive_bedrock2_func add_op. Qed.

  Derive fe25519_sub
         SuchThat (forall functions,
                      spec_of_BinOp bin_sub
                        (field_representation:=field_representation n s c)
                        (fe25519_sub :: functions))
         As fe25519_sub_correct.
  Proof. Time derive_bedrock2_func sub_op. Qed.

  Derive fe25519_opp
         SuchThat (forall functions,
                      spec_of_UnOp un_opp
                        (field_representation:=field_representation n s c)
                        (fe25519_opp :: functions))
         As fe25519_opp_correct.
  Proof. Time derive_bedrock2_func opp_op. Qed.

  Derive fe25519_scmula24
         SuchThat (forall functions,
                      spec_of_UnOp un_scmula24
                        (field_representation:=field_representation n s c)
                        (fe25519_scmula24 :: functions))
         As fe25519_scmula24_correct.
  Proof. Time derive_bedrock2_func scmula24_op. Qed.

  Derive fe25519_from_bytes
         SuchThat (forall functions,
                      spec_of_from_bytes
                        (field_representation:=field_representation n s c)
                        (fe25519_from_bytes :: functions))
         As fe25519_from_bytes_correct.
  Proof. Time derive_bedrock2_func from_bytes_op. Qed.

  Derive fe25519_to_bytes
         SuchThat (forall functions,
                      spec_of_to_bytes
                        (field_representation:=field_representation n s c)
                        (fe25519_to_bytes :: functions))
         As fe25519_to_bytes_correct.
  Proof. Time derive_bedrock2_func to_bytes_op. Qed.
End Tests.

(* Uncomment print statements below to see generated bedrock2 *)
(*
Print fe25519_mul.
Print fe25519_square.
Print fe25519_add.
Print fe25519_sub.
Print fe25519_opp.
Print fe25519_scmula24.
Print fe25519_from_bytes.
Print fe25519_to_bytes.
*)
*)

author: mit-plv

repo: fiat-crypto

save_path: github-repos/coq/mit-plv-fiat-crypto


text:
Require Import List.
Require Import alternate.

Import ListNotations.

Lemma alternate_alternation :
  forall (l1 l2 l3 : list nat), alternate l1 l2 = l3 -> alternation l1 l2 l3.
Proof.
intro l1.
induction l1.
- intros.
  simpl in H.
  rewrite H.
  apply alternation_nil.
- intros.
  destruct l2.
  * simpl in H.
    rewrite <- H.
    apply alternation_step.
    apply alternation_nil.
  * simpl in H.
    rewrite <- H.
    apply alternation_step.
    apply alternation_step.
    apply IHl1.
    reflexivity.
Qed.

Lemma alternation_alternate :
  forall (l1 l2 l3 : list nat), alternation l1 l2 l3 -> alternate l1 l2 = l3.
Proof.
induction l1.
- intros.
  inversion H; subst.
  simpl.
  reflexivity.
- intros.
  destruct l2.
  * simpl.
    inversion H; subst.
    inversion H4; subst.
    reflexivity.
  * simpl.
    inversion H; subst.
    inversion H4; subst.
    apply IHl1 in H5.
    rewrite H5.
    reflexivity.
Qed.

Lemma alternate_correct :
   forall (l1 l2 l3 : list nat), alternate l1 l2 = l3 <-> alternation l1 l2 l3.
Proof.
intros.
split.
- apply alternate_alternation.
- apply alternation_alternate.
Qed.

author: palmskog

repo: coqc-quick-example


text:
(** * Syntax of MMLL
This file defines the syntax of formulas in MMLL
(type [oo]). Predicate [isFormula] determines when a term is a valid
MMLL formula (ruling out exotic terms). Proofs usually proceed by
induction on the fact that a term satisfies this property.
 *)

Require Export LL.Misc.UtilsTactics.
Require Export LL.Misc.Permutations.
Require Export LL.Misc.Hybrid.
Require Export LL.Misc.Database.
Require Export LL.SL.MMLL.Signature.

Require Import Coq.Logic.FunctionalExtensionality.

Export ListNotations.
Set Implicit Arguments.

(** ** External definitions for the Object Logic (OL)
The class [OLSig] specifies the external definitions for terms and
atomic propositions of the object logic. The syntax is parametric on:

 - [atm] : type for atomic propositions (judgments at the Object Logic level)
 - [con] : type for syntactic constructors at the OL level
 - [uniform_atm] : predicate ruling out exotic terms at the OL level
 *)

Class OLSig :=
  {
    (* Signature for atoms (judgments at the OL level) *)
    atm:Set;
    (* Type for constants (constructors for OL syntax) *)
    con:Set;
    (* predicate ruling out exotic terms for atoms *)
    uniform_atm : (expr con -> atm) -> Prop
  }.

Section LLSyntax.

  Context `{OLS: OLSig}.
  Context `{SI: SigMMLL}.

  (** Connectives of the logic *)
  Inductive oo : Set :=
  | atom : atm -> oo
  | perp : atm -> oo
  | Top : oo
  | One : oo
  | Zero : oo
  | Bot : oo
  | AAnd : oo -> oo -> oo
  | MAnd : oo -> oo -> oo
  | AOr : oo -> oo -> oo
  | MOr : oo -> oo -> oo
  | Bang : subexp -> oo -> oo
  | Quest : subexp -> oo -> oo
  | All : (expr con -> oo) -> oo
  | Some : (expr con -> oo) -> oo.

  (** Complexity of formulas *)
  Fixpoint complexity (X:oo) :=
    match X with
    | atom A   => 1
    | perp A   => 1
    | One => 1
    | Bot => 1
    | Zero => 1
    | Top => 1
    | MAnd F G => 1+ complexity F + complexity G
    | AAnd F G => 1+ complexity F + complexity G
    | MOr F G => 1+ complexity F + complexity G
    | AOr F G => 1+ complexity F + complexity G
    | Bang a F   => 1+ complexity F
    | Quest a F  => 1+ complexity F
    | Some FX => 1+ complexity (FX (VAR con 0))
    | All FX => 1+ complexity (FX (VAR con 0))
    end.

     (** Complexity on list of formulas *)
  Fixpoint complexityL (L: list oo) :=
    match L with
    | nil => 0
    | a :: L' => complexity a + complexityL L'
    end.

  Lemma Complexity0 : forall F, complexity F > 0.
    induction F;simpl;lia.
  Qed.

  Lemma ComplexityL0 : forall L, complexityL L =0 -> L = [].
    intros;destruct L;simpl;auto.
    simpl in H.
    generalize (Complexity0 o);intros.
    lia.
  Qed.

  (** Classical linear logic dualities *)
  Fixpoint dual (X: oo) :=
    match X with
    | atom A   => perp A
    | perp A   => atom A
    | One => Bot
    | Bot => One
    | Zero => Top
    | Top => Zero
    | MAnd F G => MOr (dual  F) (dual G)
    | AAnd F G => AOr (dual  F) (dual G)
    | MOr F G => MAnd (dual  F) (dual G)
    | AOr F G => AAnd (dual  F) (dual G)
    | Bang a F   => Quest a (dual F)
    | Quest a F  => Bang a (dual   F)
    | Some X => All (fun x => dual  (X x))
    | All X => Some (fun x => dual (X x))
    end.

  (** Negation is involutive *)
  Theorem ng_involutive: forall F: oo, F = dual (dual F).
  Proof.
    intro.
    induction F; simpl; auto;
      try( try(rewrite <- IHF1); try(rewrite <- IHF2); try(rewrite <- IHF);auto);
      try(assert (o = fun x =>  dual (dual (o x))) by
             (extensionality e; apply H); rewrite <- H0; auto).
  Qed.

  Lemma DualComplexity : forall F, complexity F = complexity (dual F) .
    intros.
    induction F;intros;auto;
      try solve
          [simpl; try rewrite IHF; try rewrite IHF1; try rewrite IHF2;auto].
  Qed.

  (**  Linear Implication *)
  Definition Limp (F G : oo) : oo := MOr (dual F) G .
  Definition TypedFormula : Type := subexp * oo.

  (** Uniform Predicate (ruling out exotic terms) *)
  Inductive uniform_oo: (expr con -> oo) -> Prop :=
  | uniform_atom: forall (a: expr con -> atm),
      uniform_atm a -> uniform_oo (fun x => (atom (a x)))
  | uniform_perp: forall (a: expr con -> atm),
      uniform_atm a -> uniform_oo (fun x => (perp (a x)))
  | uniform_Top: uniform_oo (fun x => Top)
  | uniform_One: uniform_oo (fun x => One)
  | uniform_Bot: uniform_oo (fun x => Bot)
  | uniform_Zero: uniform_oo (fun x => Zero)
  | uniform_AAnd: forall (A B: expr con -> oo),
      uniform_oo A -> uniform_oo B -> uniform_oo (fun x => (AAnd (A x) (B x)))
  | uniform_MAnd: forall (A B: expr con -> oo),
      uniform_oo A -> uniform_oo B -> uniform_oo (fun x => (MAnd (A x) (B x)))
  | uniform_AOr: forall (A B: expr con -> oo),
      uniform_oo A -> uniform_oo B -> uniform_oo (fun x => (AOr (A x) (B x)))
  | uniform_MOr: forall (A B: expr con -> oo),
      uniform_oo A -> uniform_oo B -> uniform_oo (fun x => (MOr (A x) (B x)))
  | uniform_Bang: forall (A: expr con -> oo) a,
      uniform_oo A -> uniform_oo (fun x => (Bang a (A x)))
  | uniform_Quest: forall (A: expr con -> oo) a,
      uniform_oo A -> uniform_oo (fun x => (Quest a (A x)))
  | uniform_All: forall (A: expr con -> expr con -> oo),
      (forall y:expr con, uniform_oo (fun x => (A y x))) ->
      uniform_oo (fun x => (All (fun y => (A y x))))
  | uniform_Some: forall (A: expr con -> expr con -> oo),
      (forall y:expr con, uniform_oo (fun x => (A y x))) ->
      uniform_oo (fun x => (Some (fun y => (A y x)))).

  (** Well formedness condition  *)
  Inductive isFormula: oo -> Prop  :=
  | wf_atm : forall (P1:atm), isFormula (atom P1)
  | wf_perp : forall (P1:atm), isFormula (perp P1)
  | wf_Top : isFormula Top
  | wf_One : isFormula One
  | wf_Zero : isFormula Zero
  | wf_Bot : isFormula Bot
  | wf_AAnd : forall (A1 A2 :oo), isFormula A1  -> isFormula A2  -> isFormula (AAnd A1 A2)
  | wf_MAnd : forall (A1 A2 :oo), isFormula A1  -> isFormula A2  -> isFormula (MAnd A1 A2)
  | wf_AOr : forall (A1 A2 :oo), isFormula A1  -> isFormula A2  -> isFormula (AOr A1 A2)
  | wf_MOr : forall (A1 A2 :oo), isFormula A1  -> isFormula A2  -> isFormula (MOr A1 A2)
  | wf_Bang : forall (A1 :oo) a, isFormula A1 -> isFormula (Bang a A1)
  | wf_Quest : forall (A1 :oo) a, isFormula A1 -> isFormula (Quest a A1)
  | wf_All : forall (A : expr con -> oo), uniform_oo A -> (forall t: expr con, isFormula (A t)) -> isFormula (All A)
  | wf_Some : forall (A : expr con -> oo), uniform_oo A -> (forall t: expr con, isFormula (A t)) -> isFormula (Some A).

  Hint Constructors isFormula : core.

  Lemma ComplexityUniformEq : forall FX x y , uniform_oo FX ->
                                            proper x -> proper y ->
                                            complexity (FX x) =  complexity (FX y).
    intros.
    induction H;subst;simpl;firstorder.
  Qed.

   Lemma ComplexityPerm: forall M N, Permutation M N ->
                                        complexityL M =  complexityL N.
    intros.
    induction H;subst;simpl;lia.
  Qed.

    Global Instance permComplexity   :
   Proper ((@Permutation oo) ==> eq) (complexityL).
    Proof.
    unfold Proper; unfold respectful.
      intros.
      apply ComplexityPerm;auto.
  Qed.

  (** Well formendness conditions for lists and arrows *)
  Definition isFormulaL  (L:list oo)  := Forall isFormula L.
  Definition multiset := list.

  Global Instance perm_isFormulaL :
      Proper (@Permutation oo ==> Basics.impl)
             (isFormulaL  ).
    Proof.
      unfold Proper; unfold respectful; unfold Basics.impl .
      intros.
      unfold isFormulaL.
      rewrite <- H;auto.
    Qed.

  Lemma isFormulaIn : forall F L,
      isFormulaL L -> In F L -> isFormula F.
  Proof.
    intros. eapply @ForallIn with (F:=F) in H;auto.
  Qed.

  (** Arrows for the focused system
      - [UP] : negative phase
      - [DW] : positive phase
   *)
  Inductive Arrow  :=
  | UP (l : list oo) (* negative phase *)
  | DW (F : oo). (* positive phase *)

  (** Transforming arrows into lists of formulas *)
  Definition Arrow2LL (A: Arrow) : list oo :=
    match A  with
    | UP l => l
    | DW F => [F]
    end.

  (** Checking when a formulas has to lose focusing *)
  Inductive negativeFormula : oo -> Prop :=
  | RelNA1 : forall A,  negativeFormula (atom A)
  | RelTop : negativeFormula Top
  | RelBot : negativeFormula Bot
  | RelPar : forall F G, negativeFormula (MOr F G)
  | RelWith : forall F G, negativeFormula (AAnd F G)
  | RelQuest : forall F a, negativeFormula (Quest a F)
  | RelForall : forall FX, negativeFormula (All FX).

  (** Positive formulas (focusing persists *)
  Inductive positiveFormula : oo -> Prop :=
  | PosAt : forall A,  positiveFormula (perp A)
  | PosOne : positiveFormula One
  | PosZero : positiveFormula Zero
  | PosTensor : forall F G, positiveFormula (MAnd F G)
  | PosPlus : forall F G, positiveFormula (AOr F G)
  | PosBang : forall F a, positiveFormula (Bang a F)
  | PosEx : forall FX, positiveFormula (Some FX).

  (** Checking when a formulas has to be stored *)
  Inductive positiveLFormula : oo -> Prop :=
  | PosLAt : forall A,  positiveLFormula (atom A)
  | PosLPe : forall A,  positiveLFormula (perp A)
  | PosLOne : positiveLFormula One
  | PosLZero : positiveLFormula Zero
  | PosLTensor : forall F G, positiveLFormula (MAnd F G)
  | PosLPlus : forall F G, positiveLFormula (AOr F G)
  | PosLBang : forall F a, positiveLFormula (Bang a F)
  | PosLEx : forall FX, positiveLFormula (Some FX).

Theorem PositiveToLPositive : forall F,
      positiveFormula F -> positiveLFormula F.
    intros.
    inversion H;constructor.
  Qed.

  (** Every formula is either  a positive formula, or it must be released *)
  Theorem PositiveOrNegative : forall F,
      positiveFormula F \/ negativeFormula F.
    intros.
    destruct F;try (left;constructor);try(right;constructor).
  Qed.

Theorem PositiveNegativeSplit : forall M, exists M1 M2,
    Forall positiveFormula M1 /\ Forall negativeFormula M2 /\ Permutation M (M1++M2).
  Proof with sauto.
    induction M; intros...
    - exists nil.
      exists nil...
    - destruct (PositiveOrNegative a)...
      { exists (a::x).
        exists x0...
        rewrite H2... }
      { exists x.
        exists (a::x0)...
        rewrite H2... }
  Qed.

  (** Positive formulas cannot be released *)
   Theorem PositiveNotNegative: forall F,
      positiveFormula F -> ~ negativeFormula F.
    intros F H Hneg.
    inversion H;subst;inversion Hneg.
  Qed.

 Theorem NegativeNotPositive : forall F,
      negativeFormula F -> ~ positiveFormula F.
    intros F H Hneg.
    inversion H;subst;inversion Hneg.
  Qed.

  (** The dual of a positive formula is a release formula *)
Theorem PositiveDualNegative : forall F,
      positiveFormula F -> negativeFormula (dual F).
    intros F Hpos.
    inversion Hpos;subst;constructor.
  Qed.

  Theorem NegativeDualPositive : forall F, negativeFormula F -> positiveFormula (dual F).
    intros F Hrel.
    inversion Hrel;subst;constructor.
  Qed.

  (** Postive atoms *)
  Inductive IsPositiveAtom : oo -> Prop :=
  | IsPAP : forall A, IsPositiveAtom (atom A).

  (** Negative atoms *)
  Inductive IsNegativeAtom : oo -> Prop :=
  | IsNAP : forall A, IsNegativeAtom (perp A).

Local Hint Constructors IsPositiveAtom IsNegativeAtom : core.

  Theorem NegativeAtomDec : forall F,
      IsNegativeAtom F \/ ~ IsNegativeAtom F.
    induction F;auto; try solve[right;intro H'; inversion H'].
  Qed.

  Theorem PositiveAtomDec : forall F,
      IsPositiveAtom F \/ ~ IsPositiveAtom F.
    destruct F;auto;right;intro H';inversion H'.
  Qed.

  (** List of positive atoms *)
  Definition IsPositiveAtomL  L : Prop := Forall IsPositiveAtom L.

 Lemma NotAsynchronousPosAtoms :
    forall F, positiveLFormula F -> positiveFormula F \/ IsPositiveAtom F.
    intros.
    inversion H;auto; first [left;constructor
                             | right;constructor ].
  Qed.

Theorem PositiveAtomToNegativeFormula : forall F,
      IsPositiveAtom F -> negativeFormula F.
    intros.
    inversion H;constructor.
  Qed.

Theorem NetagiveAtomToPositiveFormula : forall F,
      IsNegativeAtom F -> positiveFormula F.
    intros.
    inversion H;constructor.
  Qed.

Theorem PositiveAtomToPositiveLFormula : forall F,
      IsPositiveAtom F -> positiveLFormula F.
    intros.
    inversion H;constructor.
  Qed.

Theorem positiveNotAtom F: positiveFormula F -> IsPositiveAtom F -> False.
Proof.
  intros.
  inversion H0;subst.
  inversion H.
 Qed.

  End LLSyntax.

Global Hint Constructors uniform_oo : core.
Global Hint Resolve Complexity0
                    DualComplexity: core.

Module LLNotations .
  Notation "'⊥'" := Bot.
  Notation "'⊤'" := Top.
  Notation "'1'" := One.
  Notation "'0'" := Zero.
  Notation "A ⊗ B" := (MAnd A B ) (at level 50) .
  Notation "A ⅋ B" := (MOr A B) (at level 50) .
  Notation "A ⊕ B" := (AOr A B) (at level 50) .
  Notation "A & B" := (AAnd A B) (at level 50) .
  Notation "! A" := (Bang A) (at level 50) .
  Notation "? A" := (Quest A) (at level 50) .
  Notation " A ^ " := (dual A) (at level 10) .
  Notation "'∀{' FX '}'" := (All FX) (at level 10) .
  Notation "'∃{' FX '}'" := (Some FX) (at level 10) .
End LLNotations .

Global Hint Constructors IsPositiveAtom : core.

Global Hint Constructors
    negativeFormula
    positiveFormula
    positiveLFormula
    uniform_oo isFormula IsPositiveAtom
    IsNegativeAtom: core.

Global Hint Resolve
     PositiveToLPositive
     PositiveAtomToNegativeFormula
     PositiveAtomToPositiveLFormula
     NetagiveAtomToPositiveFormula
     positiveNotAtom: core.

Global Hint Unfold isFormulaL :core.

repo: LLFramework


text:
From Hammer Require Import Hammer.

Definition injective {X Y:Type} (f:X->Y) :=
forall x1 x2:X, f x1 = f x2 -> x1 = x2.
Definition surjective {X Y:Type} (f:X->Y) :=
forall y:Y, exists x:X, f x = y.
Definition bijective {X Y:Type} (f:X->Y) :=
injective f /\ surjective f.

Inductive invertible {X Y:Type} (f:X->Y) : Prop :=
| intro_invertible: forall g:Y->X,
(forall x:X, g (f x) = x) -> (forall y:Y, f (g y) = y) ->
invertible f.

Require Import Description.
Require Import FunctionalExtensionality.

Lemma unique_inverse: forall {X Y:Type} (f:X->Y), invertible f ->
exists! g:Y->X, (forall x:X, g (f x) = x) /\
(forall y:Y, f (g y) = y).
Proof. hammer_hook "FunctionProperties" "FunctionProperties.unique_inverse".
intros.
destruct H.
exists g.
red; split.
tauto.
intros.
destruct H1.
extensionality y.
transitivity (g (f (x' y))).
rewrite H2.
reflexivity.
rewrite H.
reflexivity.
Qed.

Definition function_inverse {X Y:Type} (f:X->Y)
(i:invertible f) : { g:Y->X | (forall x:X, g (f x) = x) /\
(forall y:Y, f (g y) = y) }
:=
(constructive_definite_description _
(unique_inverse f i)).

Lemma bijective_impl_invertible: forall {X Y:Type} (f:X->Y),
bijective f -> invertible f.
Proof. hammer_hook "FunctionProperties" "FunctionProperties.bijective_impl_invertible".
intros.
destruct H.
assert (forall y:Y, {x:X | f x = y}).
intro.
apply constructive_definite_description.
pose proof (H0 y).
destruct H1.
exists x.
red; split.
assumption.
intros.
apply H.
transitivity y.
auto with *.
auto with *.
pose (g := fun y:Y => proj1_sig (X0 y)).
pose proof (fun y:Y => proj2_sig (X0 y)).
simpl in H1.
exists g.
intro.
apply H.
unfold g; rewrite H1.
reflexivity.
intro.
unfold g; apply H1.
Qed.

Lemma invertible_impl_bijective: forall {X Y:Type} (f:X->Y),
invertible f -> bijective f.
Proof. hammer_hook "FunctionProperties" "FunctionProperties.invertible_impl_bijective".
intros.
destruct H.
split.
red; intros.
congruence.
red; intro.
exists (g y).
apply H0.
Qed.

author: lukaszcz

repo: coqhammer-eval


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

(***
Modulus : 2^383 - 31
Base: 25 + 8/15
***)

Definition curve : CurveParameters :=
  {|
    sz := 15%nat;
    base := 25 + 8/15;
    bitwidth := 32;
    s := 2^383;
    c := [(1, 31)];
    carry_chains := Some [seq 0 (pred 15); [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.


text:
Require Import Arith Omega Nat.
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job
               prosa.classic.model.arrival.basic.task_arrival
               prosa.classic.model.schedule.uni.schedulability
               prosa.classic.model.schedule.uni.schedule_of_task
               prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.basic.platform_tdma
               prosa.classic.model.schedule.uni.end_time.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.

Set Bullet Behavior "Strict Subproofs".

Module WCRT_OneJobTDMA.

Import Job  TaskArrival ScheduleOfTask  ResponseTime Platform_TDMA end_time Schedulability.

  (* In this section, we prove that any job j of task tsk will be completed by
     the computed value WCRT of the exact response-time analysis under TDMA scheduling policy
     on an uniprocessor, assuming that all its previous jobs have been completed by its arrival time. *)
  Section WCRT_analysis.

    (** System model *)
    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task -> time.
    Variable task_period: sporadic_task -> time.
    Variable task_deadline: sporadic_task -> time.

    Context {Job: eqType}.
    Variable job_arrival: Job -> time.
    Variable job_cost: Job -> time.
    Variable job_deadline: Job -> time.
    Variable job_task: Job -> sporadic_task.

    (* Consider any arrival sequence... *)
    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_sporadic_tasks:
    sporadic_task_model task_period job_arrival job_task arr_seq.

    (* ..., any uniprocessor... *)
    Variable sched: schedule Job.
    (* ... where jobs do not execute before their arrival times nor after completion. *)
    Hypothesis H_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute job_arrival sched.
    Hypothesis H_completed_jobs_dont_execute:
      completed_jobs_dont_execute job_cost sched.

    (* Consider any TDMA slot assignment... *)
    Variable task_time_slot: TDMA_slot sporadic_task.
    (* ... and any slot order. *)
    Variable slot_order: TDMA_slot_order sporadic_task.

    (* ... and any sporadic task set. *)
    Variable ts: {set sporadic_task}.
    Hypothesis H_valid_task_parameters:
    valid_sporadic_taskset task_cost task_period task_deadline ts.

    (* Consider any task in task set... *)
    Variable tsk:sporadic_task.
    Hypothesis H_task_in_task_set: tsk \in ts.

    (* ... and any job belongs to it. *)
    Variable j:Job.
    Hypothesis H_job_task: job_task j =tsk.
    Hypothesis job_in_arr_seq: arrives_in arr_seq j.
    Hypothesis H_valid_job:
      valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

    (* For simplicity, let us use local names for some definitions and refer them to local variables. *)
    Let time_slot:= task_time_slot tsk.
    Let slot_offset:= Task_slot_offset ts slot_order tsk task_time_slot.
    Let tdma_cycle:= TDMA_cycle ts task_time_slot.
    Let is_scheduled_at t:=
      scheduled_at sched j t.
    Let in_time_slot_at t:=
        Task_in_time_slot ts slot_order tsk task_time_slot t.
    Let pending_at:=
      pending job_arrival job_cost sched j.

    (* Recall definitions of end time predicate... *)
    Let job_end_time_predicate:= end_time_predicate sched j.
    (* ... and completes_at *)
    Let job_completes_at:=
    completes_at job_arrival job_cost sched j.

    (* Then, let's give some local definition for clarity. *)
    (* We define a formula that allows to calculate the distance
      between time t and the previous start of tsk's time slot *)
    Let from_start_of_slot t:=
      ( t + tdma_cycle- slot_offset %% tdma_cycle) %% tdma_cycle.

    (* ... and a formula that allows to calculate the distance
      between time t and the next start of its time slot *)
    Let to_next_slot t:=
      tdma_cycle - from_start_of_slot t.

    (* and a formula that allows to calculate the duration to finish
      a job if it is right at the start of its time slot and has
      an execution cost c *)
    Let duration_to_finish_from_start_of_slot_with c:duration :=
      (div_ceil c time_slot -1) * (tdma_cycle - time_slot) + c.

    (* a formula that allows to calculate the duration between time t and the end of slot
       in case of time t in time slot *)
    Let to_end_of_slot t:=
      time_slot - from_start_of_slot t.

    (* Given the arrival time arr and job cost c, we define a formula for calculating the response time.
       This formula will be shown to be correct w.r.t. end_time_predicate *)
    Definition formula_rt (arr:instant) (c:duration):=
      if c ==0 then 0 else
      if in_time_slot_at arr then
              if c <= to_end_of_slot arr then
                   c
              else to_next_slot arr +
                    duration_to_finish_from_start_of_slot_with (c - to_end_of_slot arr)
        else
            to_next_slot arr + duration_to_finish_from_start_of_slot_with c.

    (* and the response time formula for job *)
    Definition job_response_time_tdma_in_at_most_one_job_is_pending:=
      formula_rt (job_arrival j) (job_cost j).

    (* Now, let's assume that task time slot is valid, and... *)
    Hypothesis H_valid_time_slot: is_valid_time_slot tsk task_time_slot.

    (* ... the schedule respects TDMA scheduling policy. *)
    Hypothesis TDMA_policy:
      Respects_TDMA_policy job_arrival job_cost job_task arr_seq sched ts task_time_slot slot_order.

    (* Assume that all previous jobs of same task have completed
        before the arrive of this job of this task *)
    Hypothesis all_previous_jobs_of_same_task_completed :
      forall j_other,
        arrives_in arr_seq j_other ->
        job_task j = job_task j_other ->
        job_arrival j_other < job_arrival j ->
        completed_by job_cost sched j_other (job_arrival j).

    (** First, we prove some basic lemmas about pending. *)
    Section BasicLemmas.
      (* We can prove that there is at most one job of a task is pending at
        any instant t *)
      Lemma at_most_one_job_is_pending:
        forall j_other (t : time),
          arrives_in arr_seq j_other ->
          job_arrival j_other < job_arrival j ->
          pending job_arrival job_cost sched j t ->
          pending job_arrival job_cost sched j_other t ->
          job_task j = job_task j_other -> j = j_other.
      Proof.
        move=> j_other t ARRJO ARRBF /andP [ARREDJ /negP NCOMJ] /andP [ARREDJO /negP NCOMJO] EQTSK.
        apply all_previous_jobs_of_same_task_completed in ARRBF;auto;
        apply completion_monotonic with (t':=t) in ARRBF;auto;try contradiction;
        apply scheduler_completed_jobs_dont_execute,job_arrival_times_are_consistent.
      Qed.

      (*Lemma: it respects TDMA policy for a particular case (job must be
        finished before the next job's arrival), that is, the job can be always
        scheduled at time t iff it is in its time slot at time t *)
      Lemma TDMA_policy_case_RT_le_Period:
        forall t,
          pending_at t ->
          reflect (in_time_slot_at  t) (is_scheduled_at t).
      Proof.
      intros* PEN.
      apply/introP.
      - rewrite /is_scheduled_at /in_time_slot_at -H_job_task.
        by apply TDMA_policy.
      - intro NSCHED. have BACKLOG:backlogged job_arrival job_cost sched j t by apply/andP.
        apply TDMA_policy in BACKLOG;auto.
        destruct BACKLOG as [NINSLOT | SCHED].
        + by rewrite H_job_task in NINSLOT.
        + destruct SCHED as [j_other [ARRJO [ARRBF [SAME SCHEDJO]]]].
          apply (at_most_one_job_is_pending _ t) in ARRJO;trivial.
          * by rewrite -ARRJO in SCHEDJO;move/negP in NSCHED.
          * by apply scheduled_implies_pending.
      Qed.

      (* Job is pending at its arrival *)
      Lemma pendingArrival: pending_at (job_arrival j).
      Proof.
        rewrite /pending_at /pending.
        apply /andP. split.
        - rewrite /has_arrived. auto.
        - rewrite /completed_by /service /service_during.
          rewrite ->cumulative_service_before_job_arrival_zero
          with (job_arrival0:=job_arrival). rewrite -ltnNge.
          apply H_valid_job. apply H_jobs_must_arrive_to_execute. auto.
      Qed.

      (* Job is pending at t.+1 if
          it is pending but isn't scheduled at t *)
      Lemma pendingSt:
        forall t,
          pending_at t ->
          is_scheduled_at t = false ->
          pending_at t.+1.
      Proof.
        rewrite /pending_at /pending.
        move=> t /andP [ARR NCOMP] NSCHED.
        apply /andP. split.
        - rewrite /has_arrived. auto.
        - rewrite /completed_by /service /service_during big_nat_recr /service_at /=.
          rewrite /is_scheduled_at in NSCHED. rewrite NSCHED /= addn0. auto. auto.
      Qed.

      (* Job is pending at t.+1 if
         it is both pending and scheduled at instant t
         but there are 2 cost left at instant t *)
      Lemma pendingSt_Sched:
        forall t c,
          pending_at t ->
          service sched j t + c.+2 =job_cost j ->
          is_scheduled_at t = true ->
          pending_at t.+1.
      Proof.
        rewrite /pending_at /pending.
        move=> t c /andP [ARR NCOMP] COST SCHED.
        apply /andP. split.
        - rewrite /has_arrived; auto.
        - rewrite /completed_by /service /service_during big_nat_recr /service_at /=;
          rewrite /is_scheduled_at in SCHED. rewrite SCHED /= -COST; apply/eqP;
          rewrite /service /service_during /service_at;ssromega. trivial.
      Qed.

    End BasicLemmas.

    (** Next, we prove some generic lemmas about the response time formula and the end time predicate. *)
    Section formula_predicate_eq.

      (* Lemma: duration to next start of time slot is always positive *)
      Lemma to_next_slot_pos:
        forall t, to_next_slot t>0.
      Proof.
        intros t.
        rewrite /to_next_slot /from_start_of_slot ltn_subRL addn0.
        apply ltn_pmod. by apply (TDMA_cycle_positive ts tsk).
      Qed.

      (* Lemma: if the duration to next start of slot is a+1 at instant t
              imply the duration to next start of slot is a at instant t+1 *)
      Lemma lt_to_next_slot_1LR:
        forall a t,
          a.+1 < to_next_slot t ->
          a < to_next_slot t.+1.
      Proof.
        intros*.
        rewrite /to_next_slot /from_start_of_slot.
        set cycle_sub:=tdma_cycle - slot_offset %% tdma_cycle.
        assert (H_tdma_cycle_p: tdma_cycle>0) by (apply (TDMA_cycle_positive ts tsk); done).
        repeat (rewrite -addnBA;last (apply ltnW; by apply ltn_pmod)).
        fold cycle_sub. repeat rewrite ltn_subRL.
        rewrite addSn addnS.
        case (modulo_cases (t + cycle_sub) tdma_cycle.-1); intros h1 h2.
        - rewrite prednK // in h1. ssromega.
        - destruct h1 as [h1 _]. rewrite prednK // in h1. ssromega.
      Qed.

      (* Lemma: if the duration to next start of slot is a+b at instant t
              imply the duration to next start of slot is a at instant t+b *)
      Lemma lt_to_next_slot_LR:
        forall b a t,
          a+b < to_next_slot t ->
          a < to_next_slot (t+b).
      Proof.
        intro b.
        induction b as [| b' IHb']; intros* h1.
        - rewrite addn0 in h1. rewrite addn0 //.
        - rewrite addnS.
          apply lt_to_next_slot_1LR, IHb'.
          by rewrite addSn -addnS.
      Qed.

      (* Lemma: if the job cannot be scheduled at instant t and the duration to
              next start is at least 1, thus the job cannot be scheduled at instant
              t+1 *)
      Lemma S_t_not_sched:
        forall t, pending_at t ->
         is_scheduled_at t = false ->
         1 < to_next_slot t ->
         is_scheduled_at t.+1 = false.
      Proof.
        intros* PEN NSCHED.
        assert (H_tdma_cycle_p: tdma_cycle>0). by apply (TDMA_cycle_positive ts tsk).
        have PEN2:pending_at t by trivial.
        apply TDMA_policy_case_RT_le_Period in PEN. move:NSCHED => h1 h2. have NSCHED :is_scheduled_at t = false by auto.
        move:h1=>/PEN /negP h1.
        apply/(TDMA_policy_case_RT_le_Period t.+1). by apply pendingSt.
        apply/negP.
        revert h1. rewrite /in_time_slot_at /Task_in_time_slot.
        fold tdma_cycle slot_offset time_slot.
        repeat rewrite -leqNgt.
        set cycle_sub:=tdma_cycle - slot_offset %% tdma_cycle.
        repeat (rewrite -addnBA;last (by apply ltnW, ltn_pmod)).
        fold cycle_sub.
        rewrite /to_next_slot /from_start_of_slot -addnBA in h2.
        - fold cycle_sub in h2. rewrite ltn_subRL in h2.
          case (modulo_cases (t + cycle_sub) tdma_cycle.-1).
          + intros h3 h4. rewrite prednK // in h3. rewrite h3. ssromega.
          + intros [h31 h32] h4. rewrite prednK // in h32. ssromega.
        - by apply ltnW, ltn_pmod.
      Qed.

      (* Lemma: if the job cannot be scheduled at instant t and the duration to
              next start is at least d, thus the job cannot be scheduled at instant
              t+d and is pending at t+d *)
      Lemma duration_not_sched:
        forall t,
          pending_at t ->
          is_scheduled_at t = false ->
          forall d, d < to_next_slot t ->
                    is_scheduled_at (t+d) = false /\ pending_at (t+d).
      Proof.
        intros t PEN h1 d h2. generalize dependent t.
        induction d as [| d' IHd'];intros t PEN.
        - by rewrite addn0.
        - rewrite addnS -addSn. intros NSCHED SD. apply IHd'. by apply pendingSt.
          apply S_t_not_sched;auto. ssromega. by apply lt_to_next_slot_1LR.
      Qed.

      (* Lemma: if the job is pending but cannot be scheduled at instant t
        thus that the job is pending at t+ to_next_slot t *)
      Lemma pending_Nsched_sched:
        forall t,
          pending_at t ->
          is_scheduled_at t = false ->
          pending_at (t+ to_next_slot t).
      Proof.
        intros* PEN NSCHED.
        have NEXT: to_next_slot t > 0 by apply to_next_slot_pos.
        apply duration_not_sched with (d:= (to_next_slot t).-1)in PEN.
        replace (to_next_slot t) with ((to_next_slot t).-1 .+1).
        rewrite addnS. apply pendingSt. apply PEN. apply PEN.
        ssromega. auto. ssromega.
      Qed.

      (* Lemma: It must be schedulable at next start of its time slot *)
      Lemma at_next_start_of_slot_schedulabe:
        forall t,
          pending_at t ->
          is_scheduled_at t = false ->
          is_scheduled_at (t+to_next_slot t) = true.
      Proof.
        assert (H_tdma_cycle_p: tdma_cycle>0) by (apply (TDMA_cycle_positive ts tsk); done).
        intros* PEN NSCHED_t.
        apply/TDMA_policy_case_RT_le_Period. by apply pending_Nsched_sched.
        rewrite /in_time_slot_at /Task_in_time_slot /to_next_slot /from_start_of_slot.
        repeat rewrite -addnBA.
        - set haha:= t + (tdma_cycle - slot_offset %% tdma_cycle).
          rewrite addnAC -modnDml subnKC.
          + by rewrite modnn.
          + by apply ltnW, ltn_pmod.
        - by apply ltnW, ltn_pmod.
        - by apply ltnW, ltn_pmod.
      Qed.

      (* Lemma: if the job cannot be scheduled at instant t and its residue cost is not
              0, so it has the same residue cost at instant t+1.
              the end time of this job is fixed whenever we calculate it *)
      Lemma formula_not_sched_St: forall t c, pending_at t ->
            is_scheduled_at t = false ->
            t + formula_rt t c.+1 = t.+1 + formula_rt t.+1 c.+1.
      Proof.
      intros* PEN h1.
      have PENS: pending_at t.+1 by apply pendingSt.
      assert (H_tdma_cycle_p: tdma_cycle>0). by apply (TDMA_cycle_positive ts tsk).
      assert (H_tdma_cycle_le_slot: tdma_cycle>= time_slot).
      by apply (TDMA_cycle_ge_each_time_slot ts tsk) with(task_time_slot:= task_time_slot).
      assert (Hoffset: slot_offset %% tdma_cycle <= tdma_cycle). by apply ltnW, ltn_pmod.
      have NSLOT: in_time_slot_at t = false. apply /negP /TDMA_policy_case_RT_le_Period;auto.
      by rewrite h1.
      rewrite /formula_rt /to_end_of_slot NSLOT gtn_eqF //. move:NSLOT. move /negP.
      rewrite /in_time_slot_at /Task_in_time_slot.
      move/negP. rewrite -ltnNge -/time_slot -/tdma_cycle -/slot_offset. intro NSLOT.
      case_eq (in_time_slot_at t.+1);
           rewrite /in_time_slot_at /Task_in_time_slot -/time_slot -/tdma_cycle -/slot_offset;
           intro Hcases.
      - rewrite -addnBA // in NSLOT. rewrite -addnBA // in Hcases.
        case (modulo_cases (t + (tdma_cycle - slot_offset %% tdma_cycle)) tdma_cycle.-1); intro mod_case;
        repeat (rewrite prednK // in mod_case).
          + rewrite addSn mod_case in Hcases. ssromega.
          + destruct mod_case as [case1 case2].
            rewrite /to_next_slot  /from_start_of_slot. repeat (rewrite -addnBA //).
            rewrite case2 Hcases. repeat rewrite addSn case1 -subn1 subKn //.
            repeat rewrite subn0.
            case Hc_slot:(c < time_slot); rewrite /duration_to_finish_from_start_of_slot_with.
            * by rewrite ceil_eq1 //; ssromega.
            * rewrite ceil_suba //; try ssromega.
              rewrite subn1 mulnBl mul1n addnA -addSn addn1.
               apply/eqP. rewrite eqn_add2l subnBA // addnA. repeat rewrite addnBA; try ssromega.
              -- by rewrite addKn addnAC addnK.
              -- apply leq_trans with (n:=tdma_cycle - time_slot + time_slot).
                 ++ ssromega.
                 ++ apply leq_add.
                    ** apply leq_pmull, ceil_neq0; try ssromega. rewrite ltn_subRL addn0. ssromega.
                    ** apply leqnn.
      - rewrite Hcases. repeat rewrite addnA. apply/eqP. repeat rewrite eqn_add2r.
        rewrite -addn1 -addnA eqn_add2l /to_next_slot /from_start_of_slot.
        move:Hcases. repeat rewrite -addnBA //. intro Hcases.
        case (modulo_cases (t + (tdma_cycle - slot_offset %% tdma_cycle)) tdma_cycle.-1);
        intro mod_case; rewrite prednK // in mod_case.
        + rewrite add1n addn1 addSn mod_case.
          do 2 rewrite -addn1.
          set nb:=t + (tdma_cycle - slot_offset %% tdma_cycle) .
          by rewrite subnDA subn1 addn1 prednK // ltn_subRL addn0 ltn_mod.
        + destruct mod_case as [case1 case2].
          rewrite addSn case1 in Hcases.
          assert (H_slot_pos: time_slot > 0) by assumption. ssromega.
      Qed.

      (* Lemma: if the job can be scheduled at instant t and its residue cost is not
              0 (c+1), so its residue cost will be consume 1 unit and remain c at
              instant t+1.
              the end time of this job is fixed whenever we calculate it *)

      Lemma formula_sched_St:
        forall t c,
          is_scheduled_at t = true ->
          t + formula_rt t c.+1 = t.+1 + formula_rt t.+1 c.
      Proof.
        assert (H_tdma_cycle_p: tdma_cycle>0). by apply (TDMA_cycle_positive ts tsk).
        assert (H_tdma_cycle_ge_slot: tdma_cycle>= time_slot). by apply (TDMA_cycle_ge_each_time_slot ts tsk).
        assert (Hoffset: slot_offset %% tdma_cycle <= tdma_cycle). by apply ltnW, ltn_pmod.
        intros* h1. have PEN:pending_at t by apply scheduled_implies_pending.
        have NSLOT: in_time_slot_at t = true. apply /TDMA_policy_case_RT_le_Period;auto.
        rewrite /formula_rt /to_end_of_slot NSLOT gtn_eqF //. move:NSLOT.
        rewrite /in_time_slot_at /Task_in_time_slot.
        rewrite -/time_slot -/tdma_cycle -/slot_offset. intro NSLOT.
        case (in_time_slot_at t.+1) eqn:Hcases; revert Hcases;
          rewrite /in_time_slot_at /Task_in_time_slot;
          fold time_slot tdma_cycle slot_offset; (rewrite -addnBA;last exact); intro Hcases;rewrite Hcases.
          rewrite /from_start_of_slot.
          case (c < time_slot - (t + tdma_cycle - slot_offset %% tdma_cycle) %% tdma_cycle) eqn: Hc.
            - destruct c; simpl.
              + ssromega.
              + case (modulo_cases (t + (tdma_cycle - slot_offset %% tdma_cycle)) tdma_cycle.-1); intro mod_case.
                * repeat rewrite -addnBA //. rewrite prednK // in mod_case. repeat rewrite addSn mod_case.
                  case (c < time_slot - ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1) eqn:Hc1; try ssromega.
                  rewrite ltn_subRL addSn in Hc1. rewrite ltn_subRL addnS -addnBA // in Hc.
                  ssromega.
                * repeat rewrite -addnBA //.
                  case (c < time_slot - ((t.+1 + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle)) eqn:Hc1; try ssromega.
                  rewrite prednK // in mod_case. destruct mod_case.
                  rewrite addSn in Hc1. ssromega.
            - destruct c; repeat rewrite -addnBA // in Hc;rewrite -addnBA // in NSLOT;simpl.
              + ssromega.
              + repeat rewrite -addnBA // addSn.
                case (modulo_cases (t + (tdma_cycle - slot_offset %% tdma_cycle)) tdma_cycle.-1);
                intro mod_case; rewrite prednK // in mod_case.
                * case (c < time_slot - ((t + (tdma_cycle - slot_offset %% tdma_cycle)).+1 %% tdma_cycle)) eqn:Hc1; try ssromega.
                  rewrite /to_next_slot /from_start_of_slot. repeat rewrite -addnBA //. rewrite addSn.
                  rewrite mod_case -addSn addnA addnA.
                  replace (t.+1 +(tdma_cycle - ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1)) with
                  (t + (tdma_cycle - (t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle)).
                  -- apply/eqP. rewrite eqn_add2l.
                     replace (c.+2 - (time_slot - (t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle)) with
                     (c.+1 - (time_slot - ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1)); trivial.
                     symmetry.
                     replace ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1 with
                              (((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle)+1) by ssromega.
                     rewrite subnDA. repeat (rewrite subnBA;try ssromega).
                     by rewrite addn1.
                  -- rewrite -addn1. apply/eqP. rewrite -addnA eqn_add2l.
                     replace ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1 with
                             (((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle)+1) by ssromega.
                     rewrite subnDA addnC addnBA.
                     ++ rewrite add1n subn1 //.
                     ++ rewrite ltn_subRL addn0. by apply ltn_pmod.
                * case (c < time_slot - ((t + (tdma_cycle - slot_offset %% tdma_cycle)).+1 %% tdma_cycle)) eqn:Hc1;
                  destruct mod_case as [case1 case2].
                  -- rewrite leq_eqVlt in H_tdma_cycle_ge_slot. revert H_tdma_cycle_ge_slot.
                     move/orP. intros [Hts | Hts]; try ssromega.
                     move/eqP in Hts. rewrite case2.
                     rewrite /duration_to_finish_from_start_of_slot_with Hts.
                     replace (tdma_cycle - tdma_cycle) with 0 by ssromega.
                     rewrite muln0 /to_next_slot /from_start_of_slot -addnBA // case2.
                     replace (tdma_cycle - tdma_cycle.-1)  with 1 by ssromega. ssromega.
                  -- rewrite case1 case2. rewrite leq_eqVlt in H_tdma_cycle_ge_slot.
                     revert H_tdma_cycle_ge_slot. move/orP.
                     intros [Hts | Hts]; try ssromega. move/eqP in Hts. apply /eqP.
                     rewrite -addnS eqn_add2l /duration_to_finish_from_start_of_slot_with /to_next_slot /from_start_of_slot.
                     repeat rewrite Hts.
                     replace (tdma_cycle - tdma_cycle) with 0 by ssromega.
                     repeat rewrite muln0 -addnBA //.
                     rewrite addSn case1 case2 add0n subn0 add0n.
                     replace (tdma_cycle - tdma_cycle.-1)  with 1 by ssromega.
                     rewrite add1n subn1 //= addnBA; try ssromega.
                     by rewrite addKn.
          - move/negP /negP in Hcases. rewrite -ltnNge in Hcases. rewrite -addnBA in NSLOT.
            rewrite /from_start_of_slot.
            case (c < time_slot - (t + tdma_cycle - slot_offset %% tdma_cycle) %% tdma_cycle)eqn:Hc.
            + destruct c; simpl; try ssromega.
              rewrite /to_next_slot /from_start_of_slot.
             case (modulo_cases (t + (tdma_cycle - slot_offset %% tdma_cycle)) tdma_cycle.-1); intro mod_case;
             rewrite prednK // in mod_case. rewrite addSn mod_case leq_eqVlt in Hcases.
             move: Hcases => /orP [Hcase | Hcase]; try ssromega.
             * rewrite -addn1 in Hcase.
               replace ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+2 with
                       (((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1 +1) in Hcase; try ssromega.
               rewrite eqn_add2r in Hcase. move/eqP in Hcase.
               rewrite Hcase -addnBA // subSnn in Hc. ssromega.
             * destruct mod_case as [case1 case2].
               rewrite addSn case1 in Hcases. ssromega.
           + destruct c; simpl.
             * rewrite ltn_subRL addn0 -addnBA // in Hc. ssromega.
             * rewrite /to_next_slot /from_start_of_slot.
               case (modulo_cases (t + (tdma_cycle - slot_offset %% tdma_cycle)) tdma_cycle.-1) ;intro mod_case;
               rewrite prednK // in mod_case.
               -- rewrite addSn mod_case leq_eqVlt in Hcases.
                  move:Hcases =>/orP [Hcase|Hcase]; try ssromega.
                  rewrite -addn1 in Hcase.
                  replace ((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+2 with
                          (((t + (tdma_cycle - slot_offset %% tdma_cycle)) %% tdma_cycle).+1 +1) in Hcase; try ssromega.
                  rewrite eqn_add2r in Hcase.
                  move/eqP in Hcase.
                  repeat rewrite -addnBA //.
                  rewrite addSn addSn mod_case Hcase subSnn subn1 /= subnS -addnS -addSn prednK // ltn_subRL addn0.
                  by apply ltn_pmod.
               -- destruct mod_case as [case1 _]. rewrite addSn case1 in Hcases. ssromega.
            + trivial.
      Qed.

      (* Lemma: if the job cannot be scheduled at instant t and its cost is not
                null, it will have the same cost at instant t+d, where
                d < the duration to the start of the next slot from t *)
      Lemma formula_not_sched_interval:
        forall t c,
          pending_at t ->
          is_scheduled_at t = false ->
          forall d, d < to_next_slot t ->
                    t + formula_rt t c.+1 = t + d + formula_rt (t + d) c.+1.
      Proof.
        intros* h1.
        induction d as [| d' IHd']; intro h2.
        - by repeat rewrite addn0.
        - rewrite addnS -formula_not_sched_St.
          + auto.
          + apply duration_not_sched; auto.
          + apply duration_not_sched; auto.
      Qed.

      (* Lemma: if the job cannot be scheduled at instant t and its cost is not
                null, then its cost will be the same at the start of the next slot *)
      Lemma formula_not_sched_to_next_slot:
        forall t c, pending_at t ->
          is_scheduled_at t = false ->
          t + formula_rt t c.+1 = t + to_next_slot t + formula_rt (t + to_next_slot t) c.+1.
      Proof.
        intros* PEN h1.
        assert (H2ns:to_next_slot t>0) by apply to_next_slot_pos.
        rewrite (formula_not_sched_interval _ _ _ _ (to_next_slot t).-1) //.
        - rewrite formula_not_sched_St.
          + replace (t + (to_next_slot t).-1).+1 with (t + to_next_slot t).
            * reflexivity.
            * rewrite -addnS. ssromega.
          + apply duration_not_sched;auto. ssromega.
          + apply duration_not_sched;auto. ssromega.
         - ssromega.
      Qed.

      (* Lemma: if the job cannot be scheduled at instant t and its residue cost is not
                null, and it will remain the same at the next start of slot + 1 *)
      Lemma job_not_sched_to_cunsume_1unit:
        forall t c, pending_at t ->
          is_scheduled_at t = false ->
          t + formula_rt t c.+1 = (t + to_next_slot t).+1 + formula_rt (t + to_next_slot t).+1 c.
      Proof.
        intros* PEN h1.
        assert (Hsched:is_scheduled_at (t+to_next_slot t) = true)
            . apply at_next_start_of_slot_schedulabe;auto.
        apply formula_sched_St with (c:=c) in Hsched.
        rewrite -Hsched formula_not_sched_to_next_slot //.
      Qed.

      (* Lemma: if the job cannot be scheduled at instant t and its cost is not
                null, it will have the same cost at instant t+d, where
                d < the duration to the start of the next slot from t.
                lemma on end time predicate with forward direction *)
      Lemma end_time_predicate_not_sched_eq:
        forall d c t e ,
          pending_at t ->
          is_scheduled_at t = false ->
          job_end_time_predicate t c.+1 e ->
          d < to_next_slot t ->
          job_end_time_predicate (t+d) c.+1 e.
      Proof.
        intro d.
        induction d as [| d' IHd'];intros c t e PEN h1 h2 h3.
        - by rewrite addn0.
        - rewrite addnS. apply end_time_predicate_not_sched.
          + apply duration_not_sched with (d:=d')in h1.
            * rewrite /is_scheduled_at in h1. destruct h1 as [h11 h12]. by rewrite h11.
            * auto.
            * auto.
          + apply IHd'; auto.
      Qed.

      (* Lemma: if the job cannot be scheduled at instant t and its cost is not
                null, it will have the same cost at instant t+d, where
                d < the duration to the start of the next slot from t.
                lemma on end time predicate with reverse direction *)
      Lemma end_time_predicate_not_sched_eq_rev:
        forall d c t e ,
          pending_at t ->
          is_scheduled_at t = false ->
          job_end_time_predicate (t+d) (S c) e ->
          d < to_next_slot t ->
          job_end_time_predicate t (S c) e.
      Proof.
        intro d.
        induction d as [| d' IHd'];intros c t e PEN h1 h2 h3.
        - by rewrite addn0 in h2.
        - rewrite addnS in h2. apply S_C_not_sched in h2.
          + apply IHd'; auto.
          + apply duration_not_sched with (d:=d') in h1; auto.
            rewrite /is_scheduled_at in h1. destruct h1 as [h11 h12].
            by rewrite h11.
      Qed.

      (* Lemma: if the job cannot be scheduled at instant t and its cost is not
                null, it will have the same cost at instant t+d, where
                d < the duration to the start of the next slot from t.
               lemma on end time predicate *)
      Lemma end_time_predicate_eq:
        forall t c e,
          pending_at t ->
          is_scheduled_at t = false ->
            job_end_time_predicate t c.+1 e <->
            job_end_time_predicate ((t+to_next_slot t).+1) c e.
      Proof.
        intros t c e PEN h1.
        assert (H1:is_scheduled_at t = false) by assumption.
        assert (H2ns:to_next_slot t>0) by apply to_next_slot_pos.
        assert (Hfact: (to_next_slot t).-1 < to_next_slot t). by rewrite prednK.
        split; intro h2.
        - apply (end_time_predicate_sched j sched (t + to_next_slot t) c e).
          by apply at_next_start_of_slot_schedulabe.
          apply duration_not_sched with (d:=(to_next_slot t).-1) in h1; try done.
          replace (t + to_next_slot t) with (t + (to_next_slot t).-1.+1) by (rewrite prednK; done).
          rewrite addnS.
          apply end_time_predicate_not_sched.
          + rewrite /is_scheduled_at in h1. destruct h1 as [h11 h12]. by rewrite h11.
          + by apply end_time_predicate_not_sched_eq.
        - apply S_C_sched in h2.
          + replace (t + to_next_slot t) with (t + (to_next_slot t).-1.+1) in h2 by (rewrite prednK; done).
            rewrite addnS in h2. apply S_C_not_sched in h2.
            * by apply end_time_predicate_not_sched_eq_rev with (d:=(to_next_slot t).-1) in h2.
            * apply duration_not_sched with (d:=(to_next_slot t).-1) in h1; try done.
              rewrite /is_scheduled_at in h1. destruct h1 as [h11 h12]. by rewrite h11.
           + by apply at_next_start_of_slot_schedulabe.
      Qed.

      (* Lemma: service received dont change if the job isn't scheduled *)
      Lemma service_is_zero_in_Nsched_duration:
        forall d t,
          pending_at t ->
          scheduled_at sched j t = false ->
          d <= to_next_slot t ->
          service sched j ( t + d) = service sched j t.
      Proof.
        intro d.
        induction d as [| d GD];intros* PEN NSCHED D.
        - by rewrite addn0.
        - have NSTD: scheduled_at sched j (t+d) = false by apply duration_not_sched.
          rewrite addnS /service /service_during big_nat_recr /service_at;trivial. rewrite NSTD /= addn0.
          apply GD;auto.
      Qed.

      (* Lemma: job completes at end time
        this lemma allows to valide the response time formula defined above *)
      Lemma completes_at_end_time_pre:
        forall c t , pending_at t -> service sched j t + c = job_cost j ->
        end_time_predicate sched j t c (t + formula_rt t c).
      Proof.
        intro c.
        induction c as [| c IHc];intros ARR PEN SC.
        - rewrite /formula_rt /= addn0; apply (C0_ sched j).
        - case l:(is_scheduled_at ARR).
          + destruct c as [|c];apply (S_C_sched sched j);rewrite // formula_sched_St //.
            * rewrite  /formula_rt /= addn0;apply C0_.
            * apply IHc.
                -- by apply pendingSt_Sched with (c:=c).
                -- rewrite /is_scheduled_at in l;
                   rewrite -SC /service /service_during /service_at big_nat_recr //.
                   rewrite l /=;ssromega.
          + apply end_time_predicate_eq;try exact l.
            * exact PEN.
            * destruct c as [|c];rewrite job_not_sched_to_cunsume_1unit //.
              -- rewrite  /formula_rt /= addn0; apply C0_.
              -- have SCHED: scheduled_at sched j (ARR + to_next_slot ARR) = true
                 by apply at_next_start_of_slot_schedulabe. apply IHc.
                ++ have PENX: pending_at (ARR+to_next_slot ARR) by apply pending_Nsched_sched.
                   apply pendingSt_Sched with (c:=c);try trivial.
                   by rewrite service_is_zero_in_Nsched_duration.
                ++ rewrite <-service_is_zero_in_Nsched_duration with (d:=to_next_slot ARR) in SC;auto.
                   rewrite -SC /service /service_during /service_at big_nat_recr;auto. rewrite SCHED /=.
                   ssromega.
      Qed.

    End formula_predicate_eq.

    (** Then we prove that job j completes at instant (arrival + response time) by
       (1) assuming that all its previous jobs have been completed by its arrival time and
       (2) basing on the basic and generic lemmas above. *)
    Lemma completes_at_end_time:
          job_completes_at (job_arrival j + job_response_time_tdma_in_at_most_one_job_is_pending).
    Proof.
    apply completes_at_end_time_pre.
    by apply pendingArrival.
    rewrite /service /service_during.
    by rewrite ->cumulative_service_before_job_arrival_zero with (job_arrival0:=job_arrival).
    Qed.

    (** Finally, we prove that job can be finished within the formula WCRT. *)
    Section ValidWCRT.

      (* Recall the definition of task_cost is exactly WCET, which is the worst-case execution time
          with respect to a job *)
      Let WCET := task_cost tsk.

      (* We define a formula for calculating the worst-case response time, which means
        job arrives at the end of its time slot with WCET *)
      Definition WCRT_formula cycle s wcet:=
        (div_ceil wcet s)*(cycle - s) + wcet.
      Definition WCRT:=
        WCRT_formula tdma_cycle time_slot WCET.

      (* Assume that job cost is always less than or equal to its task cost *)
      Hypothesis H_job_cost_le_task_cost: job_cost_le_task_cost task_cost job_cost job_task j.

      (* We prove that response time is always less than or equal to WCRT *)
      Lemma response_time_le_WCRT:
        job_response_time_tdma_in_at_most_one_job_is_pending <= WCRT.
      Proof.
        rewrite /job_response_time_tdma_in_at_most_one_job_is_pending /WCRT /formula_rt /to_end_of_slot.
        unfold Task_in_time_slot in in_time_slot_at.
        fold  tdma_cycle in in_time_slot_at. fold time_slot in in_time_slot_at. fold slot_offset in in_time_slot_at.
        have cost_pos: job_cost j > 0 by apply H_valid_job.
        case test_in_slot:(in_time_slot_at (job_arrival j)).
        - case test_cost:(job_cost j <= time_slot - from_start_of_slot (job_arrival j)).
          + set other := div_ceil (job_cost j) time_slot * (tdma_cycle - time_slot).
            apply leq_trans with (n:=div_ceil WCET time_slot * (tdma_cycle - time_slot) + job_cost j).
            * rewrite gtn_eqF //. apply leq_addl.
            * rewrite leq_add2l /WCET -H_job_task //.
          + assert (Hmod:(job_arrival j + tdma_cycle - slot_offset %% tdma_cycle)%% tdma_cycle < tdma_cycle)
            by (apply ltn_pmod; apply TDMA_cycle_positive with (task:=tsk); done).
            assert (hcm:tdma_cycle - time_slot <=div_ceil (job_cost j - (time_slot -
            from_start_of_slot (job_arrival j))) time_slot * (tdma_cycle - time_slot)).
            * apply leq_pmull, ceil_neq0; try apply H_valid_time_slot.
              apply negbT in test_cost; rewrite<-ltnNge in test_cost; by rewrite subn_gt0.
            * unfold duration_to_finish_from_start_of_slot_with.
              rewrite addnA mulnBl mul1n.
              set cost_sub_end:=job_cost j - (time_slot - from_start_of_slot (job_arrival j)).
              rewrite addnBA; try apply hcm.
              rewrite addnC;rewrite addnBA.
              -- rewrite addnA.
                 assert (h1:cost_sub_end + to_next_slot (job_arrival j) = job_cost j + (tdma_cycle - time_slot)).
                 ++ rewrite /cost_sub_end /to_next_slot addnC subnBA.
                    ** rewrite addnBA.
                       --- rewrite addnC -addnA subnKC; try auto.
                           rewrite addnBA //.
                           by apply TDMA_cycle_ge_each_time_slot with (task:=tsk).
                       --- apply negbT in test_cost. rewrite -ltnNge in test_cost.
                           rewrite addnC -leq_subLR. auto.
                     ** destruct (TDMA_policy_case_RT_le_Period (job_arrival j)) as [hj |hj]. apply pendingArrival.
                          unfold in_time_slot_at in hj; auto. unfold in_time_slot_at in hj; auto.
                 ++ rewrite h1 -addnBA ; try apply hcm.
                    rewrite -addnA subnKC; try apply hcm.
                    rewrite addnC gtn_eqF //.
                    apply leq_add.
                    ** rewrite leq_mul2r. apply /orP. right. apply leq_divceil2r; auto.
                       apply leq_trans with (n:=job_cost j); try apply leq_subr.
                       rewrite /WCET -H_job_task //.
                    ** rewrite /WCET -H_job_task //.
             -- rewrite <-add0n. apply leq_add; auto.
        - unfold duration_to_finish_from_start_of_slot_with.
          rewrite addnA gtn_eqF //.
          apply leq_add; try (rewrite /WCET -H_job_task //).
          rewrite mulnBl mul1n addnBA.
          + rewrite leq_subLR. apply leq_add.
            * unfold to_next_slot. apply leq_sub2l. move/negP in test_in_slot.
              apply /leP. apply not_gt. apply /ltP. by apply/negP.
            * rewrite leq_mul2r. apply /orP. right. apply leq_divceil2r; try done.
          + apply leq_pmull, ceil_neq0.
            * apply H_valid_job.
            * apply H_valid_time_slot.
      Qed.

      (* We show that this analysis is exact: job j's response time is equal to WCRT when
         (1) the job cost is equal to WCER; and
         (2) the job arrives right at the end of its time slot. *)
      Lemma exists_WCRT:
        job_cost j = WCET /\ from_start_of_slot (job_arrival j)=time_slot ->
        job_response_time_tdma_in_at_most_one_job_is_pending = WCRT.
      Proof.
        intros [COST_WCET EXISTS].
        rewrite /job_response_time_tdma_in_at_most_one_job_is_pending /WCRT /formula_rt.
        unfold Task_in_time_slot in in_time_slot_at.
        have cost_pos: job_cost j>0 by apply H_valid_job.
        fold tdma_cycle in in_time_slot_at. fold time_slot in in_time_slot_at.
        fold slot_offset in in_time_slot_at. fold from_start_of_slot in in_time_slot_at.
        assert (gt_ref: reflect (time_slot> from_start_of_slot (job_arrival j))%coq_nat
        (time_slot >from_start_of_slot (job_arrival j))) by apply ltP.
        case hgt:(time_slot > from_start_of_slot (job_arrival j)).
        - apply decPcases in gt_ref. rewrite EXISTS ltnn in hgt. done.
        - apply decPcases in gt_ref.
          destruct (TDMA_policy_case_RT_le_Period (job_arrival j)) as [hj |hj]. apply pendingArrival.
          unfold in_time_slot_at in hj.
          + rewrite /from_start_of_slot in gt_ref. rewrite /from_start_of_slot in EXISTS. case (_ < _) in gt_ref;try ssromega.
          + have F:in_time_slot_at (job_arrival j) = false by auto. rewrite F.
            rewrite /to_next_slot EXISTS /duration_to_finish_from_start_of_slot_with.
            rewrite mulnBl mul1n addnA  {1}gtn_eqF // -COST_WCET.
            apply /eqP. rewrite eqn_add2r addnC subh1.
            * by rewrite addnK.
            * by apply leq_pmull, ceil_neq0.
      Qed.

      (** Main Theorem *)
      (* We prove that any job j of task tsk will be completed by the computed value WCRT,
         assuming that all its previous jobs have been completed by its arrival time. *)
      Theorem job_completed_by_WCRT:
        completed_by job_cost sched j (job_arrival j + WCRT).
      Proof.
        apply completion_monotonic with (t:= job_arrival j + job_response_time_tdma_in_at_most_one_job_is_pending);auto.
        rewrite leq_add2l.
        apply response_time_le_WCRT.
        apply completed_by_end_time with (job_arrival0:=job_arrival);auto.
        apply completes_at_end_time.
      Qed.

    End ValidWCRT.

  End WCRT_analysis.

End WCRT_OneJobTDMA.

author: pointoflight

repo: prosa

save_path: github-repos/coq/pointoflight-prosa