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

  use ref.Ref
  use int.Int
  use seq.Seq
  use proofs.lib.seq.Seq
  use mach.java.util.Set
  use mach.java.util.UnmodifiableList as UL
  use mach.java.lang.Long
  use mach.java.lang.Integer

  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_p1.RuntimeVerificationSpecP1_Lemmas as P1
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe
  use fr.parcoursup.whyml.exceptions.verification_exception.VerificationException
  use fr.parcoursup.whyml.exceptions.verification_exception_message.VerificationExceptionMessage

  (*
  Verif de P1. Pour tout k, au moins qB pourcents des k premiers
  candidats sont boursiers ; ou sinon, aucun candidat parmi
  Ck+1, ..., Cn n’est boursier.

  https://framagit.org/parcoursup/algorithmes-de-parcoursup/-/blob/master/src/main/java/fr/parcoursup/algos/verification/VerificationsResultatsAlgoOrdreAppel.java
  *)

  let seulement_des_non_boursiers [@java:visibility:private] (oa : UL.ulist VoeuClasse.t) (i : integer) : unit
    requires { 0 <= i < UL.size oa < Integer.max_integer }
    ensures { forall k : integer. i <= k < UL.size oa -> est_non_boursier (Seq.get oa k) }
    ensures { non_boursiers_seulement (UL.content oa)[i..] }
    raises { VerificationException.E _ -> not (non_boursiers_seulement (UL.content oa)[i..]) }
  =
    let ghost s = UL.content oa in
    try
      for k = i to UL.size oa - 1 do
        invariant { forall j : integer. i <= j < k -> est_non_boursier (Seq.get oa j) }
        invariant { non_boursiers_seulement s[i..k] }
        let v = UL.get oa k in
        if est_boursier v then begin
           assert { s[i..] == s[i..k] ++ s[k..]};
           raise VerificationException.E (crtX0 VerificationExceptionMessage.VERIFICATION_RESULTATS_ALGO_ORDRE_APPEL_VIOLATION_P1);
        end;
        assert { s[i..k+1] == (snoc s[i..k] v) }
      done
    with
      IndexOutOfBoundsException.E _ -> absurd
    end

  let verifier (grp : GroupeClassementValide.t) : unit
    requires { groupe_ok grp }
    requires { seq_rangs_appel_ge_1 grp }
    requires { seq_rangs_appel_uniques grp }
    ensures { P1.spec grp }
    raises { VerificationException.E _ -> not (P1.spec grp) }
  =
    let oa = get_ordre_appel_list grp in
    let ghost s = UL.content oa in
    let ghost tx_b = get_taux_min_boursiers_pourcents grp in
    let lg_tx_b = Long.of_integer (get_taux_min_boursiers_pourcents grp) in
    let candidats : set integer = Set.empty () in
    let boursiers : set integer = Set.empty () in
    let nb_voeux = get_nb_voeux_classes grp in

    assert { nb_voeux = length s = UL.size oa };
    assert { forall i j : integer. 0 <= i < j < nb_voeux ->
      get_rang_appel (Seq.get oa i) < get_rang_appel (Seq.get oa j) };

    try
      for i = 0 to nb_voeux - 1 do
        invariant { [@expl:|candidats|] Set.size candidats = i <= max_integer }
        invariant { [@expl:candidats is s] P1.candidats_is_s s[..i] candidats }
        invariant { [@expl:boursiers -> candidats] is_subset boursiers candidats }
        invariant { [@expl:|boursiers|] Set.size boursiers = nb_boursiers s[..i] }
        invariant { [@expl:tx pref ok]  forall k. 0 <= k <= i -> P1.tx_boursiers_ok s[..k] tx_b }

        let v = UL.get oa i in
        let g_cn_cod = get_g_cn_cod v in

        if Set.contains candidats g_cn_cod then
          absurd;
        assert { s[..i+1] == snoc s[..i] v };
        label H in
        let _ = Set.add candidats g_cn_cod in ();

        P1.candidats_is_s_l2 s (pure { candidats at H }) candidats (pure { i });

        if est_boursier v then
        begin
          assert { is_subset boursiers candidats };
          let _ = Set.add boursiers g_cn_cod in ();
          P1.nb_boursiers_snoc s (pure { boursiers at H}) boursiers (pure { i } );
          is_subset_add (pure { boursiers at H}) (pure { candidats at H}) g_cn_cod boursiers candidats;
        end;

        let lg_nb_b = Long.of_integer (Set.size boursiers) in
        let lg_nb_c = Long.of_integer (Set.size candidats) in
        if 100 * lg_nb_b < lg_tx_b * lg_nb_c then
        begin
          assert { not P1.tx_boursiers_ok s[.. i+1] tx_b };
          assert { est_non_boursier v };
          seulement_des_non_boursiers oa i;
          assert { forall k. i <=k < length s -> non_boursiers_seulement s[k..] };
          break;
        end;
      done
    with
      IndexOutOfBoundsException.E _ -> absurd
    end
end

(* generated on Mon Dec  2 02:04:28 UTC 2024 from rev:  *)