Parcoursup / Calcul de l'ordre d'appel des candidats index


module RuntimeVerificationSpecP3
   use seq.Seq
   use int.Int

   use fr.parcoursup.whyml.ordreappel.algo.taux.Taux
   use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
   use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide

   predicate p3a_aux (s : seq VoeuClasse.t) (i k : int) =
     est_boursier s[k] || get_rang s[k] <= get_rang s[i] ||
     get_rang_appel s[k] >= get_rang_appel s[i]

   predicate p3a_loc (s : seq VoeuClasse.t) (tx_r : Taux.t) (i : int) =
      (not (est_boursier s[i]) && (est_du_secteur s[i] || tx_r = 0))
      -> (forall k. 0 <= k < length s -> p3a_aux s i k)

   predicate rang_appel_correct_p (q_b rang rang_appel : int) =
       ((100 - q_b) * rang_appel <= (100 - q_b) + 100 * rang)

   predicate p3b_loc (s : seq VoeuClasse.t) (tx_b tx_r : Taux.t) (i : int) =
      not (est_boursier s[i]) && (est_du_secteur s[i] || tx_r = 0)
      -> rang_appel_correct_p tx_b (get_rang s[i]) (get_rang_appel s[i])

   predicate spec (grp : GroupeClassementValide.t) =
     let s = get_ordre_appel_list grp in
     let tx_b = get_taux_min_boursiers grp in
     tx_b < 100 ->
     let tx_r = get_taux_min_du_secteur grp in
       forall i. 0 <= i < length s -> (p3a_loc s tx_r i && p3b_loc s tx_b tx_r i)
end

module RuntimeVerificationSpecP3_LocalLemmas
  use mach.java.lang.Integer
  use int.Int
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.invariants.iq4_1.IQ4_1
  use proofs.ordre_appel.invariants.iq4_2.IQ4_2
  use proofs.ordre_appel.invariants.iq4_3.IQ4_3
  use proofs.ordre_appel.properties.q4_1.Q4_1
  use proofs.ordre_appel.properties.q5.Q5
  use fr.parcoursup.whyml.ordreappel.algo.taux.Taux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide
  use proofs.ordre_appel.specs.GroupeClassementValideProperties
  use RuntimeVerificationSpecP3

  let lemma l1a (grp : GroupeClassementValide.t) (s : seq_voeu) (i : int)
    requires { ordre_appel_properties grp }
    requires { s == get_ordre_appel_list grp }
    requires { 0 <= i < length s }
    requires { est_non_boursier_du_secteur s[i] }
    ensures { p3a_loc s (get_taux_min_du_secteur grp) i }
  =
    begin
      assert { q4_1a s };
      assert { q4_1a_loc s i };

      for k = 0 to length s - 1 do
        invariant { forall j. 0 <= j < k -> p3a_aux s i j }
        if est_boursier s[k] then continue;
        if est_du_secteur s[k] then
        begin
          assert { est_non_boursier_du_secteur s[k] };
          assert { p3a_aux s i k };
        end;
        assert { p3a_aux s i k };
      done
    end

  let lemma l1b (grp : GroupeClassementValide.t) (s : seq_voeu) (tx_b : Taux.t) (i : int)
    requires { ordre_appel_properties grp }
    requires { ordre_appel_contiguous grp }
    requires { s == get_ordre_appel_list grp }
    requires { 0 <= i < length s }
    requires { est_non_boursier_du_secteur s[i] }
    requires { tx_b = get_taux_min_boursiers grp }
    ensures { p3b_loc s tx_b (get_taux_min_du_secteur grp) i }
  =
    begin
      assert { q4_1 (nb_boursiers s) tx_b s };
      assert { q4_1b_loc tx_b s i };
      assert { rang_appel_correct_p tx_b (get_rang s[i]) (get_rang_appel s[i]) }
    end

  let lemma l2a (grp : GroupeClassementValide.t) (s : seq_voeu) (tx_b tx_ds : Taux.t) (i : int)
    requires { ordre_appel_properties grp }
    requires { s == get_ordre_appel_list grp }
    requires { 0 <= i < length s }
    requires { est_non_boursier_hors_secteur s[i] }
    requires { tx_b = get_taux_min_boursiers grp }
    requires { tx_ds = get_taux_min_du_secteur grp = 0 }
    ensures { p3a_loc s tx_ds i }
  =
    let nb_b = nb_boursiers s in
    let nb_ds = nb_du_secteur s in

    assert { q5 nb_b nb_ds tx_b tx_ds s };
    assert { q5a_aux_loc nb_b nb_ds tx_b tx_ds s i  };
    assert { forall k. 0 <= k < length s -> not in_Zr nb_ds tx_ds s k };
    for k = 0 to length s - 1 do
      invariant { forall j. 0 <= j < k -> p3a_aux s i j }
      if est_boursier s[k] || i <= k then
        continue;
      if get_rang s[k] > get_rang s[i] then
      begin
        assert { in_Zb nb_b tx_b s k };
        absurd;
      end
    done

  let lemma l2b (grp : GroupeClassementValide.t) (s : seq_voeu) (tx_b tx_ds : Taux.t) (i : int)
    requires { ordre_appel_properties grp }
    requires { ordre_appel_contiguous grp }

    requires { s == get_ordre_appel_list grp }
    requires { 0 <= i < length s }
    requires { est_non_boursier_hors_secteur s[i] }
    requires { tx_b = get_taux_min_boursiers grp < 100 }
    requires { tx_ds = get_taux_min_du_secteur grp = 0 }
    ensures { p3b_loc s tx_b tx_ds i }
  =
    let nb_b = nb_boursiers s in
    let nb_ds = nb_du_secteur s in
    assert { nb_contraintes_taux_ds nb_ds tx_ds s[..i] = 0 };
    assert { q5 nb_b nb_ds tx_b tx_ds s };
    assert { q5b_loc tx_b tx_ds s i };
    assert { q5b_aux_loc nb_b nb_ds tx_b tx_ds s i };
    assert { iq4_2a nb_b tx_b s };
    assert { iq4_2a_loc nb_b tx_b s i };
    ()
end

module RuntimeVerificationSpecP3_Lemmas
  use mach.java.lang.Integer
  use int.Int
  use mach.java.util.UnmodifiableList as UL
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use fr.parcoursup.whyml.ordreappel.algo.taux.Taux
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props
  use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide
  use proofs.ordre_appel.specs.GroupeClassementValideProperties
  use RuntimeVerificationSpecP3_LocalLemmas
  use export RuntimeVerificationSpecP3

  let lemma spec_imply_rv_p3 (grp : GroupeClassementValide.t)
    requires { ordre_appel_properties grp }
    requires { ordre_appel_contiguous grp }
    ensures { spec grp }
  =
    let tx_b = get_taux_min_boursiers grp in
    if Integer.to_int (Taux.tx tx_b) >= 100 then
      return;
    let tx_ds = get_taux_min_du_secteur grp in
    let s = UL.content (get_ordre_appel_list grp) in

    for i = 0 to Seq.length s - 1 do
      invariant { forall j. 0 <= j < i -> p3a_loc s tx_ds j }
      invariant { forall j. 0 <= j < i -> p3b_loc s tx_b tx_ds j }

      if est_boursier s[i] then continue;
      if est_du_secteur s[i] then
      begin
        assert { est_non_boursier_du_secteur s[i] };
        assert { p3a_loc s tx_ds i };
        assert { p3b_loc s tx_b tx_ds i };
      end
      else if Integer.to_int (Taux.tx tx_ds) = 0 then
      begin
        assert { est_non_boursier_hors_secteur s[i] };
        assert { p3a_loc s tx_ds i };
        assert { p3b_loc s tx_b tx_ds i };
      end
    done

end

(* generated on Thu Jan 30 02:06:23 UTC 2025 from rev:  *)

Generated by why3doc 1.7.2+git