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


module Properties
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.properties.q1.Q1
  use proofs.ordre_appel.properties.q2.Q2
  use proofs.ordre_appel.properties.q3.Q3
  use proofs.ordre_appel.invariants.iq4_2.IQ4_2
  use proofs.ordre_appel.properties.q4_1.Q4_1
  use proofs.ordre_appel.properties.q4_2.Q4_2
  use proofs.ordre_appel.properties.q5.Q5
  use proofs.ordre_appel.properties.q6.Q6
  use proofs.ordre_appel.properties.p4.P4
  use proofs.ordre_appel.properties.p5.P5
  use fr.parcoursup.whyml.ordreappel.algo.taux.Taux
  use fr.parcoursup.whyml.ordreappel.algo.ordre_appel.OrdreAppel

  predicate ordre_appel_properties (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (op oa : seq_voeu) =
       q1 tx_b oa
    /\ q2 tx_b tx_ds oa
    /\ q3 oa
    /\ iq4_2a nb_b tx_b oa
    /\ q4_1 nb_b tx_b oa
    /\ q4_2 nb_ds tx_ds oa
    /\ q5 nb_b nb_ds tx_b tx_ds oa
    /\ q6 tx_b tx_ds op oa
    /\ p4 tx_b tx_ds oa
    /\ p5 tx_b tx_ds oa
end

module Properties_Snoc
  use Properties
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.invariants.iq0.IQ0
  use export proofs.ordre_appel.properties.q1.Q1_Snoc
  use export proofs.ordre_appel.properties.q2.Q2_Snoc
  use export proofs.ordre_appel.properties.q3.Q3_Snoc
  use export proofs.ordre_appel.invariants.iq4_2.IQ4_2_Snoc
  use export proofs.ordre_appel.properties.q4_1.Q4_1_Snoc
  use export proofs.ordre_appel.properties.q4_2.Q4_2_Snoc
  use export proofs.ordre_appel.properties.q5.Q5_Snoc
  use export proofs.ordre_appel.properties.q6.Q6_Snoc
  use export proofs.ordre_appel.properties.p4.P4_Snoc
  use export proofs.ordre_appel.properties.p5.P5_Snoc

  let lemma properties_empty (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (op oa : seq_voeu) (m : EnumMap.t)
    requires { oa = Seq.empty}
    requires { iq0 op oa m }
    requires { nb_b = nb_boursiers op }
    requires { nb_ds = nb_du_secteur op }
    ensures { ordre_appel_properties nb_b nb_ds tx_b tx_ds op oa }
  =
    assert { q6 tx_b tx_ds op oa };
    iq4_2_empty nb_b tx_b op oa m
end

module Properties_UpToRangAppel
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts
  use proofs.ordre_appel.seq_voeux.SeqVoeuxEqUpToRangAppel
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse_Props

  use proofs.ordre_appel.properties.q1.Q1_UpToRangAppel
  use proofs.ordre_appel.properties.q2.Q2_UpToRangAppel
  use proofs.ordre_appel.properties.q3.Q3_UpToRangAppel
  use proofs.ordre_appel.invariants.iq4_2.IQ4_2_UpToRangAppel
  use proofs.ordre_appel.properties.q4_1.Q4_1_UpToRangAppel
  use proofs.ordre_appel.properties.q4_2.Q4_2_UpToRangAppel
  use proofs.ordre_appel.properties.q5.Q5_UpToRangAppel
  use proofs.ordre_appel.properties.q6.Q6_UpToRangAppel
  use proofs.ordre_appel.properties.p4.P4_UpToRangAppel
  use proofs.ordre_appel.properties.p5.P5_UpToRangAppel
  use Properties

  let lemma properties_up_to_rang_appel_oa (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (op oa1 oa2 : seq_voeu)
    requires { [@expl:alld(oa1)] all_distincts oa1 }
    requires { ordre_appel_properties nb_b nb_ds tx_b tx_ds op oa1 }
    requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 }
    ensures { ordre_appel_properties nb_b nb_ds tx_b tx_ds op oa2 }
  =
    q1_up_to_rang_appel_oa tx_b oa1 oa2;
    q2_up_to_rang_appel_oa tx_b tx_ds oa1 oa2;
    q3_up_to_rang_appel_oa oa1 oa2;
    iq4_2a_up_to_rang_appel_oa nb_b tx_b oa1 oa2;
    q4_1_up_to_rang_appel_oa nb_b tx_b oa1 oa2;
    q4_2_up_to_rang_appel_oa nb_ds tx_ds oa1 oa2;
    q5_up_to_rang_appel_oa nb_b nb_ds tx_b tx_ds oa1 oa2;
    q6_up_to_rang_appel_oa tx_b tx_ds op oa1 oa2;
    p4_up_to_rang_appel_oa tx_b tx_ds oa1 oa2;
    p5_up_to_rang_appel_oa tx_b tx_ds oa1 oa2

  let lemma properties_up_to_rang_appel_op (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (op1 op2 oa : seq_voeu)
    requires { ordre_appel_properties nb_b nb_ds tx_b tx_ds op1 oa }
    requires { seq_voeu_eq_up_to_rang_appel op1 op2 }
    ensures { ordre_appel_properties nb_b nb_ds tx_b tx_ds op2 oa }
  =
    q6_up_to_rang_appel_op tx_b tx_ds op1 op2 oa

end

module Invariants
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap

  use proofs.ordre_appel.invariants.iqx.IQX
  use proofs.ordre_appel.invariants.iq0.IQ0
  use proofs.ordre_appel.invariants.iq1.IQ1
  use proofs.ordre_appel.invariants.iq2.IQ2
  use proofs.ordre_appel.invariants.iq3_0.IQ3_0
  use proofs.ordre_appel.invariants.iq3_1.IQ3_1
  use proofs.ordre_appel.invariants.iq3_2.IQ3_2
  use proofs.ordre_appel.invariants.iq3_3.IQ3_3
  use proofs.ordre_appel.invariants.iq3_4.IQ3_4
  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.invariants.iq6.IQ6

  use Properties

  predicate invariants_algo (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (op oa :seq_voeu) (filesAttente : EnumMap.t) =
    let nb_v = Seq.length op in
    nb_b = nb_boursiers op &&
    nb_ds = nb_du_secteur op &&
    iq0 op oa filesAttente &&
    iqx_0 nb_v nb_b nb_ds oa filesAttente &&
    iqx_2 nb_b tx_b oa &&
    iqx_3 nb_b nb_ds oa &&
    iqx_4 oa filesAttente &&
    iqx_5 oa filesAttente &&
    iq1 nb_b tx_b oa &&
    iq2 nb_b nb_ds tx_b tx_ds oa &&
    iq3_0 oa filesAttente &&
    iq3_1 oa filesAttente &&
    iq3_2 oa filesAttente &&
    iq3_3 oa filesAttente &&
    iq3_4 oa filesAttente &&

    iq4_1 nb_ds tx_ds oa filesAttente &&
    iq4_2 nb_b tx_b oa filesAttente &&
    iq4_3 nb_b nb_ds tx_b tx_ds oa filesAttente &&

    iq6 tx_b tx_ds oa filesAttente &&

    ordre_appel_properties nb_b nb_ds tx_b tx_ds op oa
end

module Invariants_Snoc
  use int.Int
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use proofs.ordre_appel.eligibles.ValidEligibles
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap
  use fr.parcoursup.whyml.ordreappel.algo.enum_map.EnumMap_Lemmas
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.PQueueVoeuxClasses as PQueue

  use proofs.ordre_appel.invariants.iqx.IQX_Snoc
  use proofs.ordre_appel.invariants.iq0.IQ0_Snoc
  use proofs.ordre_appel.invariants.iq1.IQ1_Snoc
  use proofs.ordre_appel.invariants.iq2.IQ2_Snoc
  use proofs.ordre_appel.invariants.iq3_0.IQ3_0_Snoc
  use proofs.ordre_appel.invariants.iq3_1.IQ3_1_Snoc
  use proofs.ordre_appel.invariants.iq3_2.IQ3_2_Snoc
  use proofs.ordre_appel.invariants.iq3_3.IQ3_3_Snoc
  use proofs.ordre_appel.invariants.iq3_4.IQ3_4_Snoc
  use proofs.ordre_appel.invariants.iq4_1.IQ4_1_Snoc
  use proofs.ordre_appel.invariants.iq4_2.IQ4_2_Snoc
  use proofs.ordre_appel.invariants.iq4_3.IQ4_3_Snoc
  use proofs.ordre_appel.invariants.iq6.IQ6_Snoc
  use Properties_Snoc

  use export Invariants

  (* unfold invariants_algo *)
  (* unfold ordre_appel_properties_for_oa *)
  (* unfold ordre_appel_seq_properties *)
  (* split_all_full *)
  let lemma invariants_algo_snoc (cB cR : bool)
                                 (nb_b nb_ds  : int) (tx_b tx_ds : Taux.t)
                                 (op oa : seq_voeu)
                                 (om m : EnumMap.t)
                                 (eligibles: PQueue.t)
                                 (v : VoeuClasse.t)
    requires { [@expl:pre/g ok] seq_groupe_ok op }
    requires { [@expl:pre/g sorted] seq_rangs_sorted op }
    (*requires { [@expl:pre/rangs >= 1] 1 <= v.rang && forall i. 0 <= i < length oa -> 1 <= oa[i].rang  }*)
    requires { [@expl:pre/valid eligibles] meilleur_eligible cB cR om eligibles v }
    requires { [@expl:pre/alld m] enummap_all_distincts om }
    requires { [@expl:pre/x selected] enummap_pop_v om m v }
    requires { [@expl:pre/cB equiv tx_b contraignant] cB = taux_b_contraignant tx_b oa nb_b }
    requires { [@expl:pre/cR equiv tx_ds contraignant] cR = taux_ds_contraignant tx_ds oa nb_ds }
    requires { [@expl:pre/inv algo om] invariants_algo nb_b nb_ds tx_b tx_ds op oa om }
    ensures { invariants_algo nb_b nb_ds tx_b tx_ds op (snoc oa v) m }
  =
    let nb_v = Seq.length op in
    let s = snoc oa v in
    iq0_snoc op oa om m v;
    iqx_0_snoc nb_v nb_b nb_ds oa om m v;
    iqx_2_snoc cB cR nb_b tx_b oa om eligibles v;
    iqx_3_snoc nb_v nb_b nb_ds oa om m v;
    iqx_4_snoc oa om m v;
    iqx_5_snoc oa om m v;
    iq1_snoc nb_b tx_b oa v;
    q1_snoc nb_b tx_b oa v;

    iq2_snoc cB cR nb_b nb_ds tx_b tx_ds oa om m eligibles v;
    q2_snoc nb_b nb_ds tx_b tx_ds oa v;

    iq3_0_snoc cB cR eligibles oa om m v;
    iq3_1_snoc cB cR eligibles oa om m v;
    q3_snoc oa m v;

    iq3_2_snoc cB cR eligibles oa om m v;
    iq3_3_snoc cB cR eligibles oa om m v;
    iq3_4_snoc cB cR eligibles oa om m v;

    iq4_1_snoc cB cR nb_ds tx_ds oa om m eligibles v;
    iq4_2_snoc cB cR nb_b tx_b oa om m eligibles v;
    iq4_3_snoc cB cR nb_b nb_ds tx_b tx_ds oa om m eligibles v;
    iq6_snoc cB cR nb_b nb_ds tx_b tx_ds oa om m v;

    q4_1_snoc nb_b tx_b oa m v;
    q4_2_snoc nb_ds tx_ds oa m v;
    q5_snoc nb_b nb_ds tx_b tx_ds  oa m v;
    q6_snoc nb_b nb_ds tx_b tx_ds op oa m v;
    p4_snoc nb_b nb_ds tx_b tx_ds oa s m v;
    p5_snoc nb_b nb_ds tx_b tx_ds oa s m v;
    ()

  let lemma invariants_algo_init (nb_b nb_ds  : int) (tx_b tx_ds : Taux.t) (op oa : seq_voeu) (m : EnumMap.t)
    requires { length op = EnumMap.get_nb_voeux_classes m }
    requires { nb_b = nb_boursiers op = EnumMap.get_nb_boursiers m }
    requires { nb_ds = nb_du_secteur op = EnumMap.get_nb_du_secteur m }
    requires { seq_groupe_ok op }
    requires { seq_rangs_sorted op }
    requires { oa = Seq.empty }
    requires { enummap_eq_grp m op }
    ensures { invariants_algo nb_b nb_ds tx_b tx_ds op oa m }
  =

    iq0_empty op m;
    iqx_0_empty op oa m;
    iq4_1_empty nb_ds tx_ds op oa m;
    iq4_2_empty nb_b tx_b op oa m;
    iqx_4_empty op oa m;
  (*
    iqx_4_empty g oa m;
    iqx_5_empty g oa m;
    iq4_2_empty g oa m;
    iq4_3_empty g oa m;
    iq6_empty g oa m;
    properties_empty g oa m
    *)

 ()

end

module GroupeClassementValideProperties
  use int.Int
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe
  use proofs.ordre_appel.seq_voeux.SeqVoeuxDistincts
  use proofs.ordre_appel.seq_voeux.SeqVoeuxEqUpToRangAppel
  use Properties
  use Properties_UpToRangAppel
  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 ordre_appel_properties_oa (g : GroupeClassementValide.t) (oa : seq_voeu) =
    let nb_b, tx_b  = nb_boursiers g, get_taux_min_boursiers g in
    let nb_ds, tx_ds  = nb_du_secteur g, get_taux_min_du_secteur g in
    let op = get_ordre_pedagogique g in
    Properties.ordre_appel_properties nb_b nb_ds tx_b tx_ds op oa

  predicate ordre_appel_properties (g : GroupeClassementValide.t)  =
    let oa = get_ordre_appel_list g in
    ordre_appel_properties_oa g oa

  predicate ordre_appel_contiguous (g : GroupeClassementValide.t)  =
    let oa = get_ordre_appel_list g in
    seq_rangs_appel_contiguous oa

  let lemma oap_up_to_rang_appel (nb_b nb_ds : int) (tx_b tx_ds : Taux.t) (op1 oa1 op2 oa2 : seq_voeu)
    requires { all_distincts oa1 }
    requires { Properties.ordre_appel_properties nb_b nb_ds tx_b tx_ds op1 oa1 }
    requires { seq_voeu_eq_up_to_rang_appel op1 op2 }
    requires { seq_voeu_eq_up_to_rang_appel oa1 oa2 }
    ensures { Properties.ordre_appel_properties nb_b nb_ds tx_b tx_ds op2 oa2 }
  =
    properties_up_to_rang_appel_oa nb_b nb_ds tx_b tx_ds op1 oa1 oa2;
    assert { Properties.ordre_appel_properties nb_b nb_ds tx_b tx_ds op1 oa2 }

  let lemma oap_up_to_rang_appel_groupe (g1 : GroupeClassementValide.t) (oa : seq_voeu) (g2 : GroupeClassementValide.t)
    requires { [@expl:pre/alld(oa)] all_distincts oa }
    requires { [@expl:pre/#b g1 = #b g2] nb_boursiers g1 = nb_boursiers g2 }
    requires { [@expl:pre/#ds g1 = #ds g2] nb_du_secteur g1 = nb_du_secteur g2 }
    requires { [@expl:pre/%b g1 = %b g2] get_taux_min_boursiers g1 = get_taux_min_boursiers g2 }
    requires { [@expl:pre/%ds g1 = %ds g2] get_taux_min_du_secteur g1 = get_taux_min_du_secteur g2 }
    requires { [@expl:pre/specs g1 oa] ordre_appel_properties_oa g1 oa }
    requires { [@expl:pre/op g1 = op g2 (mod ra)] seq_voeu_eq_up_to_rang_appel (get_ordre_pedagogique g1) (get_ordre_pedagogique g2) }
    requires { [@expl:pre/oa g1 = oa g2 (mod ra)] seq_voeu_eq_up_to_rang_appel oa (get_ordre_appel_list g2) }
    ensures { [@expl:specs g2] ordre_appel_properties g2 }
  =
    ()

end

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

Generated by why3doc 1.7.2+git