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

  use int.Int
  use seq.Seq
  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_p3.RuntimeVerificationSpecP3 as P3
  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 : Taux.t) (rang rang_appel : integer) : bool
    requires { 0 <= q < 100 }
    requires { 0 <= rang && 0 <= rang_appel }
    ensures { result = P3.rang_appel_correct_p q rang rang_appel }
  =
    let q_b = Taux.tx q in
     let q_bp = 100 - (Long.of_integer q_b) in
     let r_appel = Long.of_integer rang_appel in
     let r = Long.of_integer rang in
     let result = (q_bp * r_appel <= q_bp + 100 * r) in
       assert { result = ((100 - q_b) * rang_appel <= (100 - q_b) + 100 * rang) };
       assert { result = P3.rang_appel_correct_p q_b r r_appel };
       result

  (*
  Verif de P3: Un candidat du secteur
  et non boursier qui a le rang r dans le classement pédagogique
  ne peut-être doublé que par des boursiers et aura un rang dans
  l’ordre d’appel inférieur ou égal à 1 + r * ( 1 + qB∕(100 - qB) )
  si qB < 100.

  https://framagit.org/parcoursup/algorithmes-de-parcoursup/-/blob/master/src/main/java/fr/parcoursup/algos/verification/VerificationsResultatsAlgoOrdreAppel.java
  *)
  let verifier (grp : GroupeClassementValide.t) : unit
    requires { groupe_ok grp }
    ensures { P3.spec grp }
    raises { VerificationException.E _ -> not (P3.spec grp) }
  =
    let q_b = get_taux_min_boursiers grp in
    if Taux.tx q_b >= 100 then
      return;

    let q_s = get_taux_min_du_secteur grp in
    let nb_voeux = get_nb_voeux_classes grp in
    let oa = get_ordre_appel_list grp in
    try begin
      for iv1 = 0 to nb_voeux - 1 do
        invariant { forall k. 0 <= k < iv1 -> P3.p3a_loc oa q_s k }
        invariant { forall k. 0 <= k < iv1 -> P3.p3b_loc oa q_b q_s k }

        let v1 = UL.get oa iv1 in
        if not (est_boursier v1) && (est_du_secteur v1 || (Taux.tx q_s) = 0) then
        begin
          if not (rang_appel_correct q_b (get_rang v1) (get_rang_appel v1) ) then
          begin
            assert { not (P3.p3b_loc oa q_b q_s iv1) };
            raise VerificationException.E (crtX2 VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_NON_BOURSIER_DU_SECTEUR_DIMINUE_TROP (get_g_cn_cod v1) (get_c_gp_cod grp));
          end;

          for iv2 = 0 to iv1 - 1 do
            invariant { forall k. 0 <= k < iv2 -> P3.p3a_aux oa iv1 k }
            let v2 = UL.get oa iv2 in
            if (not est_boursier v2) && get_rang v2 > get_rang v1 && get_rang_appel v2 < get_rang_appel v1 then
            begin
              assert { not (P3.p3a_aux oa iv1 iv2) };
              assert { not (P3.p3a_loc oa q_s iv1) };
              raise VerificationException.E (crtX2 VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_NON_BOURSIER_DEPASSE_CANDIDAT_DU_SECTEUR (get_g_cn_cod v2) (get_c_gp_cod grp));
            end;
            assert { P3.p3a_aux oa iv1 iv2 };
          done
        end
      done
    end with
    | InvalidArgumentException.E _ -> absurd
    | IndexOutOfBoundsException.E _ -> absurd
    end
end

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