module VerificationResultatsAlgoOrdreAppelP4
  [@java:package:fr.parcoursup.whyml.verification]
  [@java:visibility:package]

  use int.Int
  use mach.java.lang.Integer
  use mach.java.lang.Long
  use mach.java.lang.IndexOutOfBoundsException
  use mach.java.util.UnmodifiableList
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide
  use proofs.ordre_appel.properties.rv_p4.RuntimeVerificationSpecP4_Lemmas as P4
  use fr.parcoursup.whyml.exceptions.invalid_argument_exception.InvalidArgumentException
  use fr.parcoursup.whyml.exceptions.verification_exception.VerificationException
  use fr.parcoursup.whyml.exceptions.verification_exception_message.VerificationExceptionMessage

  let rang_appel_correct (q_r rang rang_appel : integer) : bool
    requires { 0 < q_r <= 100 }
    requires { 0 <= rang && 0 <= rang_appel }

    ensures { result = P4.rang_appel_correct_p q_r rang rang_appel }
  =
    let q_rp = 100 - (Long.of_integer q_r) in
    let r_appel = Long.of_integer rang_appel in
    let r = Long.of_integer rang in
    let result = (q_rp * r_appel <= q_rp + 100 * r) in
      assert { result = P4.rang_appel_correct_p q_r r r_appel };
      result

   (*
    Verif de P4: Un candidat hors-secteur boursier qui a le rang r 
    dans le classement pédagogique ne peut être doublé que par des
    candidats du secteur, boursiers ou non, et aura donc un rang au
    plus 1 + (1 +  qR ∕ (100 - qR) ) * r dans l’ordre d’appel. 
   *)
  let verifier (grp : GroupeClassementValide.t) : unit
    requires { groupe_ok grp }
    ensures { P4.spec grp }
    raises { VerificationException.E _ -> not (P4.spec grp) }
  =
    let oa = get_ordre_appel_list grp in
    let q_r = get_taux_min_du_secteur_pourcents grp in
    if q_r = 0 then
      return;
    let nb_voeux = get_nb_voeux_classes grp in

    try begin
      for iv1 = 0 to nb_voeux - 1 do
        invariant { forall k. 0 <= k < iv1 -> P4.p4a_loc oa k }
        invariant { forall k. 0 <= k < iv1 -> P4.p4b_loc oa q_r k }

        let v1 = UL.get oa iv1 in
        if not (est_boursier v1 && not (est_du_secteur v1))then
          continue;

        if q_r < 100 then
        begin
          if not (rang_appel_correct q_r (get_rang v1) (get_rang_appel v1) ) then
          begin
            assert { not (P4.p4b_loc oa q_r iv1) };
            raise VerificationException.E (crtX4 VerificationExceptionMessage.VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_BOURSIER_HORS_SECTEUR_DIMINUE_TROP
             (get_g_cn_cod v1) (get_rang v1) (get_rang_appel v1) (get_c_gp_cod grp))
          end
        end;

        for iv2 = 0 to iv1 - 1 do
          invariant { forall k. 0 <= k < iv2 -> P4.p4a_aux oa iv1 k }
          let v2  = UL.get oa iv2 in
          if not (est_du_secteur v2) && get_rang v2 > get_rang v1 &&
            get_rang_appel v2 < get_rang_appel v1 then
          begin
            assert { not (P4.p4a_aux oa iv1 iv2) };
            assert { not (P4.p4a_loc oa iv1) };
            raise VerificationException.E (crtX3 VerificationExceptionMessage.VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_HORS_SECTEUR_DEPASSE_BOURSIER_HORS_SECTEUR
              (get_g_cn_cod v2) (get_g_cn_cod v1) (get_c_gp_cod grp));
          end
        done
      done
    end with
    | InvalidArgumentException.E _ -> absurd
    | IndexOutOfBoundsException.E _ -> absurd
    end
end

(* generated on Thu Nov 21 02:04:27 UTC 2024 from rev:  *)