module RuntimeVerificationSpecP5
  use seq.Seq
  use int.Int

  use mach.java.lang.Integer
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide

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

  predicate p5a_loc (s : seq VoeuClasse.t) (i : int) =
    (not (est_boursier s[i]) && not (est_du_secteur s[i]))
    -> (forall k. 0 <= k < length s -> p5a_aux s i k)

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

  predicate p5b_loc (s : seq VoeuClasse.t) (tx_b tx_r : int) (i : int) =
    (not (est_boursier s[i]) && not (est_du_secteur s[i]))
    -> tx_b + tx_r < 100
    -> rang_appel_correct_p tx_b tx_r (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_pourcents grp in
    let tx_r = get_taux_min_du_secteur_pourcents grp in
    forall k. 0 <= k < length s ->  (p5a_loc s k && p5b_loc s tx_b tx_r k)
end

module RuntimeVerificationSpecP5_LocalLemmas
  use mach.java.lang.Integer
  use int.Int
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.properties.q3.Q3
  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 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 RuntimeVerificationSpecP5

  let lemma l1 (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 }
    requires { tx_ds = get_taux_min_du_secteur grp }
    ensures { p5a_loc s i }
  =
    assert { q3 s };
    assert { q4_1a s };
    assert { q4_2a s };
    assert { q5a s };

    for k = i+1 to length s - 1 do
      invariant { forall j. 0 <= j < k -> p5a_aux s i j }
      assert { get_rang_appel s[k] > get_rang_appel s[i] };
      if get_rang s[k] >= get_rang s[i] then
        continue;
      if est_boursier_du_secteur s[k] then
      begin
        assert { q3a_loc s k };
        absurd;
      end;

      if est_non_boursier_du_secteur s[k] then
      begin
        assert { q4_1a_loc s k };
        assert { est_boursier s[i] };
        absurd;
      end;

      if est_boursier_hors_secteur s[k] then
      begin
        assert { q4_2a_loc s k };
        assert { est_du_secteur s[i] };
        absurd;
      end;
      assert { est_non_boursier_hors_secteur s[k] };
      assert { q5a_loc s k };
      assert { est_boursier s[i] \/ est_du_secteur s[i] };
      absurd;
    done

    let lemma l2 (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 }
      requires { tx_ds = get_taux_min_du_secteur grp }
      requires { tx_b + tx_ds < 100 }
      ensures { p5b_loc s tx_b tx_ds  i }
    =
      assert { q5b tx_b tx_ds s };
      assert { q5b_loc tx_b tx_ds s i };
      assert { rang_appel_correct_p tx_b tx_ds (get_rang s[i]) (get_rang_appel s[i]) }
end

module RuntimeVerificationSpecP5_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 RuntimeVerificationSpecP5_LocalLemmas
  use export RuntimeVerificationSpecP5

  let lemma spec_imply_rv_p5 (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
    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 -> p5a_loc s j }
      invariant { forall j. 0 <= j < i -> p5b_loc s tx_b tx_ds j }

      if est_boursier s[i] then continue;
      if est_du_secteur s[i] then continue;
      assert { p5a_loc s i };

      if Taux.tx tx_ds + Taux.tx tx_b >= 100 then continue;
      assert { p5b_loc s tx_b tx_ds i };
    done
end

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