definitions: add a function to compare the whole pipeline

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>

src/definitions.v

@@ -229,6 +229,15 @@ Proof.
     + contradiction.
 Qed.
 
+(* Pipeline comparison. *)
+Definition pipeline_leb p1 p2 :=
+  let comb := List.combine p1 p2 in
+  Nat.eqb (List.length p1) (List.length p2)
+  && List.forallb (fun instrs =>
+                     match instrs with
+                     | ((o1, st1), (o2, st2)) => opcode_beq o1 o2 && state_leb st1 st2
+                     end) comb.
+
 (* Pipeline validity. *)
 Definition single_in_stage trace st :=
   List.count_occ stage_eq_dec (get_stg trace) st <=? 1.