module RuntimeVerificationSpecP2
   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 p2a_loc (s : seq VoeuClasse.t) (tx_ds : int) (i : int) =
     (est_boursier s[i] /\ (tx_ds = 0 \/ est_du_secteur s[i]))
     -> get_rang_appel s[i] <= get_rang s[i]

   predicate p2b_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 p2b_loc (s : seq VoeuClasse.t) (tx_ds : int) (i : int) =
     (est_boursier s[i] /\ (tx_ds = 0 \/ est_du_secteur s[i]))
     -> (forall k. 0 <= k < length s -> p2b_aux s i k)

   predicate spec (grp : GroupeClassementValide.t) =
      let s = get_ordre_appel_list grp in
      let tx_ds = get_taux_min_du_secteur_pourcents grp in
         forall k. 0 <= k < length s -> (p2a_loc s tx_ds k && p2b_loc s tx_ds k)
end

module RuntimeVerificationSpecP2_LocalLemmas
  use int.Int
  use seq.Seq
  use mach.java.util.Set
  use mach.java.lang.Integer
  use proofs.lib.seq.Seq
  use proofs.ordre_appel.seq_voeux.SeqVoeux
  use proofs.ordre_appel.seq_voeux.SortedSeqVoeux
  use proofs.ordre_appel.seq_voeux.SeqVoeuxGroupe
  use proofs.ordre_appel.seq_voeux.SeqVoeuxTaux
  use proofs.ordre_appel.properties.q3.Q3
  use proofs.ordre_appel.properties.q4_2.Q4_2
  use proofs.ordre_appel.invariants.iq4_1.IQ4_1
  use proofs.ordre_appel.specs.GroupeClassementValideProperties
  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 RuntimeVerificationSpecP2
  use pigeon.Pigeonhole

  let lemma l1 (s : seq_voeu) (i : int)
    requires { 0 <= i < length s }
    requires { seq_rangs_ge_1 s }
    requires { seq_rangs_uniques s }
    requires { forall j. 0 <= j < i -> voeu_lt s[j] s[i] }
    ensures { i < get_rang s[i] }
  =
    let ghost function p (i : int) : int = Integer.to_int (get_rang s[i]) - 1 in
    if Integer.to_int (get_rang s[i]) <= i then
    begin
      assert { forall j. 0 <= j < i -> 0 <= get_rang s[j] - 1  < get_rang s[i] - 1 < i };
      assert { forall j. 0 <= j < i -> p j = get_rang s[j] - 1 };
      assert { forall j. 0 <= j < i -> 0 <= p j < i };
      pigeonhole i (i-1) p;
      let (i1,i2) = any (i1:int,i2:int) ensures { 0 <= i1 < i2 < i /\ p i1 = p i2 } in
      assert { get_rang s[i1] = get_rang s[i2] };
      absurd
    end

   let lemma l2 (grp : GroupeClassementValide.t) (s : seq_voeu)  (i : int)
     requires { ordre_appel_properties grp }
     requires { ordre_appel_contiguous grp }
     requires { s == get_ordre_appel_list grp}
     requires { 0 <= i < length s }
     ensures { p2a_loc s (get_taux_min_du_secteur grp) i }
   =
     assert { get_rang_appel s[i] = i + 1 };
     if not est_boursier s[i] then
       return;
     assert { q3 s };
     if est_du_secteur s[i] then
     begin
       assert { est_boursier_du_secteur s[i] };
       assert { 1 <= i + 1 <= get_rang s[i] };
       assert { get_rang_appel s[i] <= get_rang s[i] };
       return;
     end;
     let tx_ds = get_taux_min_du_secteur grp in
     if Taux.tx tx_ds > 0 then
       return;
     if i = 0 then begin
       assert { seq_rangs_ge_1 s };
       assert { 1 <= get_rang s[i]  };
       return;
     end;
     let nb_ds = nb_du_secteur s in
     assert { est_boursier_hors_secteur s[i] };
     assert { q4_2 nb_ds tx_ds s };
     if get_rang_appel s[i] > get_rang s[i] then
     begin
       assert { q4_2a_aux_loc nb_ds tx_ds s i };
       assert { forall j. 0 <= j < i -> get_rang s[i] < get_rang s[j] -> (est_du_secteur s[j] && in_Zr nb_ds tx_ds s j)} ;
       assert { forall j. 0 <= j < i -> not in_Zr nb_ds tx_ds s j } ;
       assert { forall j. 0 <= j < i -> get_rang s[j] < get_rang s[i] } ;
       l1 s i;
       assert { i < get_rang s[i] }
     end;
     assert { get_rang_appel s[i] <= get_rang s[i] };
     ()

 let lemma l3 (grp : GroupeClassementValide.t) (s : seq_voeu)  (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_boursier_du_secteur s[i] }
     ensures { p2b_loc s (get_taux_min_du_secteur grp) i }
   =
      assert { q3 s };
      assert { 1 <= i+1 <= get_rang s[i] };
      assert { q3a_loc s i };
      assert { forall k. 0 <= k < i -> get_rang s[k] < get_rang s[i] };
      ()

   let lemma l4 (grp : GroupeClassementValide.t) (s : seq_voeu)  (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_boursier_hors_secteur s[i] }
     requires { get_taux_min_du_secteur_pourcents grp = 0 }
     ensures { p2b_loc s (get_taux_min_du_secteur grp) i }
   =
      let tx_ds = get_taux_min_du_secteur grp in
      let nb_ds = nb_du_secteur s in
      assert { q4_2 nb_ds tx_ds s };
      assert { q4_2a_aux_loc nb_ds 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 -> p2b_aux s i j }
        if k < i then begin
          if get_rang s[i] < get_rang s[k] then
          begin
            assert {in_Zr nb_ds tx_ds s k };
            absurd;
          end;
          assert { get_rang s[k] <= get_rang s[i] };
          continue;
        end;
      done;

      assert { forall k. 0 <= k < length s -> p2b_aux s i k };
      ()

end

module RuntimeVerificationSpecP2_Lemmas
  use int.Int
  use seq.Seq
  use mach.java.util.Set
  use mach.java.lang.Integer
  use mach.java.lang.IndexOutOfBoundsException
  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.properties.q3.Q3
  use proofs.ordre_appel.properties.q4_2.Q4_2
  use proofs.ordre_appel.invariants.iq4_1.IQ4_1
  use proofs.ordre_appel.specs.GroupeClassementValideProperties
  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 RuntimeVerificationSpecP2_LocalLemmas
  use export RuntimeVerificationSpecP2

  let lemma spec_imply_rv_p2 (grp : GroupeClassementValide.t)
    requires { ordre_appel_properties grp }
    requires { ordre_appel_contiguous grp }
    ensures { spec grp }
  =
    let s = get_ordre_appel_list grp in
    let tx_ds = get_taux_min_du_secteur grp in
    let nb_voeux = UL.size s in
    try
      for i = 0 to nb_voeux - 1 do
        invariant { [@expl:inv p2a] forall k. 0 <= k < i -> p2a_loc s tx_ds k }
        invariant { [@expl:inv p2b] forall k. 0 <= k < i -> p2b_loc s tx_ds k }
        let si = UL.get s i in
        if not (est_boursier si) then
          continue;

        if est_du_secteur si  then
        begin
          l3 grp (UL.content s) (Integer.to_int i);
          assert { [@expl:p2b] p2b_loc s tx_ds i }
        end
        else if Taux.tx tx_ds = 0 then
        begin
          l4 grp (UL.content s) (Integer.to_int i);
          assert { est_boursier_hors_secteur s[i] };
          assert { [@expl:p2b] p2b_loc s tx_ds i };
        end;
      done
    with
      IndexOutOfBoundsException.E _ -> absurd
    end
end

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