module RuntimeVerificationSpecP1
  use int.Int
  use seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use mach.java.util.Set
  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 tx_boursiers_ok (s : seq_voeu) (tx_b : int)  =
    tx_b * (length s) <= 100 * (nb_boursiers s)

  predicate candidats_is_s (s : seq_voeu) (candidats : set integer) =
     (length s = Set.size candidats) /\ (
     (forall c : integer. Set.contains candidats c ->
        exists k:integer. (0 <= k < length s && c = get_g_cn_cod s[k])) /\
     (forall k:integer. 0 <= k < length s -> Set.contains candidats (get_g_cn_cod s[k])))

  predicate p1_loc (s : seq_voeu) (tx_b : int) (i : int) =
     forall k. 0 <= k < i ->
      (tx_boursiers_ok s[..k] tx_b \/ non_boursiers_seulement s[k..])

  predicate spec (grp : GroupeClassementValide.t) =
    let s = get_ordre_appel_list grp in
    let tx_b = get_taux_min_boursiers_pourcents grp in
      p1_loc s tx_b (length s)
end

module RuntimeVerificationSpecP1_Lemmas
  use int.Int
  use seq.Seq
  use mach.java.util.Set
  use mach.java.lang.Integer
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use proofs.ordre_appel.properties.q1.Q1
  use proofs.ordre_appel.specs.GroupeClassementValideProperties
  use fr.parcoursup.whyml.ordreappel.algo.voeu_classe.VoeuClasse
  use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide
  use export RuntimeVerificationSpecP1

  let lemma candidats_is_s_snoc (s : seq_voeu) (ocandidats candidats: set integer) (v : VoeuClasse.t)
    requires { Set.size ocandidats < max_integer }
    requires { 0 <= length (snoc s v) <= max_integer }
    requires { candidats_is_s s ocandidats }
    requires { Set.is_add ocandidats candidats (get_g_cn_cod v) }
    ensures { candidats_is_s (snoc s v) candidats }
  = let sp = snoc s v in
    let cv = get_g_cn_cod v in
    assert { forall c : integer. Set.contains candidats c -> c <> cv -> exists k:integer. (0 <= k < length sp && c = get_g_cn_cod sp[k]) };
    assert { exists k:integer. (0 <= k < length sp && cv = get_g_cn_cod sp[k]) }

  let lemma candidats_is_s_l1 (s : seq_voeu) (candidats: set integer) (v : VoeuClasse.t)
    requires { candidats_is_s s candidats }
    requires { forall k : integer. 0 <= k < length s -> get_g_cn_cod s[k] <> get_g_cn_cod v }
    ensures { not Set.contains candidats (get_g_cn_cod v) }
  =
    ()

  let lemma candidats_is_s_l2 (s : seq_voeu) (ocandidats candidats: set integer) (i : int)
    requires { Set.size ocandidats < max_integer }
    requires { 0 <= i < length s }
    requires { candidats_is_s s[..i] ocandidats }
    requires { Set.is_add ocandidats candidats (get_g_cn_cod s[i]) }
    ensures { candidats_is_s s[.. i+1] candidats }
  =
    candidats_is_s_snoc s[..i] ocandidats candidats s[i]

  let lemma nb_boursiers_snoc (s : seq_voeu) (oboursiers boursiers : set integer) (i : int)
    requires { 0 <= i < length s }
    requires { Set.size oboursiers < max_integer }
    requires { nb_boursiers s[..i] = Set.size oboursiers }
    requires { Set.is_add oboursiers boursiers (get_g_cn_cod s[i]) }
    requires { est_boursier s[i] }
    ensures { nb_boursiers s[..i+1] = Set.size boursiers }
  =
    ()

  let lemma tx_boursiers_ok_snoc (s : seq_voeu) (tx_b : integer)  (i : int)
    requires { 0 <= i < length s }
    requires { 0 <= tx_b <= 100 }
    requires { tx_boursiers_ok s[..i] tx_b }
    requires { est_boursier s[i] }
    ensures { tx_boursiers_ok s[..i+1] tx_b }
  =
    assert { s[..i+1] = snoc s[..i] s[i] }

  let lemma tx_boursiers_ok_equiv_seq_respecte_taux_b (s : seq_voeu) (tx_b : Taux.t)
    ensures { tx_boursiers_ok s tx_b <-> seq_respecte_taux_b tx_b s }
  = ()

  let lemma spec_imply_rv_p1 (grp : GroupeClassementValide.t)
    requires { ordre_appel_properties grp }
    ensures { spec grp }
  =
    let s = get_ordre_appel_list grp in
    let tx_b = get_taux_min_boursiers grp in
      assert { q1 tx_b s }
end

(* generated on Thu Nov 21 02:04:27 UTC 2024 from rev:  *)