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

  use int.Int
  use mach.java.lang.Integer
  use mach.java.lang.IndexOutOfBoundsException
  use mach.java.lang.Long
  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.seq_voeux.SeqVoeuxGroupe
  use proofs.ordre_appel.properties.rv_p5.RuntimeVerificationSpecP5_Lemmas as P5
  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_b q_r rang rang_appel : integer) : bool
    requires { 0 <= q_b <= 100 }
    requires { 0 <= q_r <= 100 }
    requires { q_b + q_r < 100 }
    requires { 0 <= rang && 0 <= rang_appel }

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

   (*
    Un candidat non-résident non-boursier ne double jamais personne.
    Si son rang dans le classement pédagogique est r et
    si qB + qR < 100 alors son rang dans l'ordre d’appel
    sera inférieur ou égal à
    ⌈ (1 + (qB + qR) ⁄ (100 - (qB + qR)) × (r + 1) ⌉.

    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 { P5.spec grp }
    raises { VerificationException.E _ -> not (P5.spec grp) }
  =
    let oa = get_ordre_appel_list grp in
    let q_b = get_taux_min_boursiers_pourcents grp in
    let q_r = get_taux_min_du_secteur_pourcents grp in
    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 -> P5.p5a_loc oa k }
        invariant { forall k. 0 <= k < iv1 -> P5.p5b_loc oa q_b q_r k }

        let v1 = UL.get oa iv1 in

        if est_boursier v1 || est_du_secteur v1 then
          continue;

        if q_b + q_r < 100 then
        begin
          if not (rang_appel_correct q_b q_r (get_rang v1) (get_rang_appel v1)) then
          begin
            assert { not (P5.p5b_loc oa q_b q_r iv1) };
            raise VerificationException.E (crtX2 VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_NON_BOURSIER_HORS_SECTEUR_DIMINUE_TROP
              (get_g_cn_cod v1) (get_c_gp_cod grp));
          end;
        end;

        assert { seq_rangs_appel_sorted oa };
        assert { forall k. 0 <= k <= iv1 -> get_rang_appel (Seq.get oa k) <= get_rang_appel v1 };
        for iv2 = iv1+1 to nb_voeux - 1 do
          invariant { forall k. 0 <= k < iv2 -> P5.p5a_aux oa iv1 k }
          let v2 = UL.get oa iv2 in
          if get_rang v2 < get_rang v1 && get_rang_appel v2 > get_rang_appel v1 then
          begin
            assert { not (P5.p5a_aux oa iv1 iv2) };
            assert { not (P5.p5a_loc oa iv1) };
            raise VerificationException.E (crtX3 VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_NON_BOURSIER_HORS_SECTEUR_DEPASSE_CANDIDAT
              (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 Mon Dec  2 02:04:28 UTC 2024 from rev:  *)