change correct definition for correct user defs

src/syntax/FlightPlanSized.v

@@ -32,6 +32,9 @@ Set Implicit Arguments.
 Definition correct_block_id (fp: flight_plan) (id: block_id): Prop :=
   (id < get_nb_block fp).
 
+Definition is_user_id (fp: flight_plan) (id: block_id): Prop :=
+  (id < get_nb_block fp - 1).
+
 Lemma normalise_block_id_is_correct : 
   forall (fp: flight_plan) (id: block_id),
   correct_block_id fp (normalise_block_id fp id).
@@ -42,15 +45,28 @@ Proof.
   - apply leb_complete_conv in E. apply E.
 Qed.
 
+Lemma user_id_is_correct :
+  forall (fp: flight_plan) (id: block_id),
+  is_user_id fp id ->
+    correct_block_id fp id.
+Proof.
+  intros fp id Huser. unfold correct_block_id.
+  unfold is_user_id in Huser.
+  lia.
+Qed. 
+
 (** ** Properties about exceptions *)
 Definition correct_excpt (ex: fp_exception): Prop :=
   is_nat8 (get_expt_block_id ex).
 
+Definition correct_user_excpt (fp: flight_plan) (ex: fp_exception): Prop :=
+  correct_excpt ex /\ is_user_id fp (get_expt_block_id ex).
+
 (** ** Properties about forbidden deroutes *)
 Record correct_fbd_deroute (fp: flight_plan) (fbd: fp_forbidden_deroute) :=
   create_correct_fbd_deroute {
-    get_correct_from: correct_block_id fp (get_fbd_from fbd);
-    get_correct_to: correct_block_id fp (get_fbd_to fbd);
+    get_correct_from: is_user_id fp (get_fbd_from fbd);
+    get_correct_to: is_user_id fp (get_fbd_to fbd);
   }.
 
 (** ** Properties about deroute *)
@@ -60,6 +76,12 @@ Definition correct_deroutes (block: fp_block): Prop :=
       = DEROUTE ids' params
     -> is_nat8 (get_deroute_block_id params).
 
+Definition correct_user_deroutes (fp: flight_plan) (block: fp_block): Prop :=
+  forall ids ids' idd params,
+    List.nth ids (get_block_stages block) (DEFAULT idd) 
+      = DEROUTE ids' params
+    -> is_user_id fp (get_deroute_block_id params).
+
 (** * Property that blocks are well numbered *)
 Definition well_numbered_blocks (fp: flight_plan): Prop :=
   forall i, i < get_nb_block fp
@@ -75,6 +97,14 @@ Record well_sized_block (block: fp_block) :=
         get_correct_deroute: correct_deroutes block;
     }.
 
+Record well_sized_user_block (fp: flight_plan) (block: fp_block) :=
+  create_well_sized_user_block {
+      get_well_sized_block: well_sized_block block;
+      get_correct_user_lexcpts:
+      Forall (correct_user_excpt fp) (get_block_exceptions block);
+      get_correct_user_deroute: correct_user_deroutes fp block;
+  }.
+
 (** * Properties about the flight plan *)
 
 (** ** Property about that there is less than 256 blocks*)
@@ -89,8 +119,8 @@ Definition nb_block_lt_256 (fp: flight_plan): Prop :=
 Record verified_fp_e (fp: flight_plan) := create_verified_fp_e {
     get_nb_block8: nb_block_lt_256 fp;
     get_well_numbered_blocks: well_numbered_blocks fp;
-    get_well_sized_blocks: forall i, well_sized_block (get_block fp i);
-    get_correct_gexcpts: Forall correct_excpt (get_fp_exceptions fp);
+    get_well_sized_user_blocks: forall i, well_sized_user_block fp (get_block fp i);
+    get_correct_user_gexcpts: Forall (correct_user_excpt fp) (get_fp_exceptions fp);
     get_correct_fbd: Forall (correct_fbd_deroute fp)
                             (get_fp_forbidden_deroutes fp)
   }.