module RuntimeVerificationSpec
  use int.Int
  use seq.Seq
  use mach.java.lang.Integer
  use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe
  use proofs.ordre_appel.seq_voeux.SeqVoeuxEqUpToRangAppel

  use proofs.ordre_appel.properties.rv_p1.RuntimeVerificationSpecP1 as P1
  use proofs.ordre_appel.properties.rv_p2.RuntimeVerificationSpecP2 as P2
  use proofs.ordre_appel.properties.rv_p3.RuntimeVerificationSpecP3 as P3
  use proofs.ordre_appel.properties.rv_p4.RuntimeVerificationSpecP4 as P4
  use proofs.ordre_appel.properties.rv_p5.RuntimeVerificationSpecP5 as P5

  use fr.parcoursup.whyml.ordreappel.algo.algo_ordre_appel_sortie.AlgoOrdreAppelSortie as AOAS
  use fr.parcoursup.whyml.ordreappel.algo.algo_ordre_appel_entree.AlgoOrdreAppelEntree as AOAE
  use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide

  predicate grp_eq_up_to_rang_appel (grp1 : t) (grp2 : t) =
    get_c_gp_cod grp1 = get_c_gp_cod grp2 /\
    get_taux_min_boursiers_pourcents grp1 = get_taux_min_boursiers_pourcents grp2 /\
    get_taux_min_du_secteur_pourcents grp1 = get_taux_min_du_secteur_pourcents grp2 /\
    get_nb_voeux_classes grp1 = get_nb_voeux_classes grp2 /\
    seq_voeu_eq_up_to_rang_appel (get_ordre_pedagogique grp1) (get_ordre_pedagogique grp2)

  predicate donnees_entree_eq_sortie (entree : seq GroupeClassementValide.t) (sortie : seq GroupeClassementValide.t) =
    Seq.length entree = Seq.length sortie /\
    forall i. 0 <= i < Seq.length sortie -> exists j. 0 <= j < Seq.length entree &&
      grp_eq_up_to_rang_appel entree[j] sortie[i]

  predicate group_satisfies_specs (grp : GroupeClassementValide.t) =
    seq_rangs_appel_ge_1 grp /\
    seq_rangs_appel_uniques grp /\
    P1.spec grp /\
    P2.spec grp /\
    P3.spec grp /\
    P4.spec grp /\
    P5.spec grp

  predicate groups_satisfy_specs_loc (sortie : seq GroupeClassementValide.t) (i : int) =
    forall k. 0 <= k < i -> group_satisfies_specs sortie[k]

  predicate groups_satisfy_specs (sortie : seq GroupeClassementValide.t) =
    groups_satisfy_specs_loc sortie (Seq.length sortie)

end

module RuntimeVerificationSpec_Lemmas
  use proofs.ordre_appel.specs.GroupeClassementValideProperties
  use proofs.ordre_appel.properties.rv_p1.RuntimeVerificationSpecP1_Lemmas as P1
  use proofs.ordre_appel.properties.rv_p2.RuntimeVerificationSpecP2_Lemmas as P2
  use proofs.ordre_appel.properties.rv_p3.RuntimeVerificationSpecP3_Lemmas as P3
  use proofs.ordre_appel.properties.rv_p4.RuntimeVerificationSpecP4_Lemmas as P4
  use proofs.ordre_appel.properties.rv_p5.RuntimeVerificationSpecP5_Lemmas as P5

  use fr.parcoursup.whyml.ordreappel.algo.groupe_classement_valide.GroupeClassementValide
  use export RuntimeVerificationSpec

  let lemma spec_imply_rv  (grp : GroupeClassementValide.t)
    requires { ordre_appel_properties grp }
    requires { ordre_appel_contiguous grp }
    ensures { group_satisfies_specs grp }
  = ()
end

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