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

  use int.Int
  use mach.java.lang.Integer
  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_p2.RuntimeVerificationSpecP2 as P2
  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

   (*
    Verif de P2: Un candidat à la fois boursier et du secteur
    (ou dans un groupe sans taux de candidats du secteur)
    qui a le rang r dans le classement pédagogique 
    n’est jamais doublé par personne et aura donc un rang inférieur 
    ou égal à r dans l’ordre d’appel. 

    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 { P2.spec grp }
    raises { VerificationException.E _ -> not (P2.spec grp) }
  =
    let oa = get_ordre_appel_list grp in
    let nb_voeux = get_nb_voeux_classes grp in
    let tx_sect = get_taux_min_du_secteur_pourcents grp in
    try begin
      for iv1 = 0 to nb_voeux - 1 do
        invariant { [@expl:inv P2a] forall k. 0 <= k < iv1 -> P2.p2a_loc oa tx_sect k }
        invariant { [@expl:inv P2b] forall k. 0 <= k < iv1 -> P2.p2b_loc oa tx_sect k }

        let v1 = UL.get oa iv1 in
        if est_boursier v1 && (tx_sect = 0 || est_du_secteur v1) then
        begin
          if get_rang_appel v1 > get_rang v1 then
          begin
            assert {[@expl:P2a nok] not (P2.p2a_loc oa tx_sect iv1) };
            raise VerificationException.E (crtX2
              VerificationExceptionMessage.VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_BOURSIER_DU_SECTEUR_DECROIT
                (get_g_cn_cod v1) (get_c_gp_cod grp));
          end;

          for iv2 = 0 to iv1 - 1 do
            invariant { forall k. 0 <= k < iv2 -> P2.p2b_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 { [@expl:P2b nok] not (P2.p2b_aux oa iv1 iv2) };
              assert { [@expl:P2b nok] not (P2.p2b_loc oa tx_sect iv1) };
              raise VerificationException.E (crtX3 VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_BOURSIER_DU_SECTEUR_DEPASSE
                (get_g_cn_cod v1) (get_g_cn_cod v2) (get_c_gp_cod grp));
            end;
          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:  *)