From 2b6149c0f3b712c6074764e36624e1f84948e2f5 Mon Sep 17 00:00:00 2001 From: Alban Gruin <alban.gruin@irit.fr> Date: Tue, 26 Jul 2022 16:16:28 +0200 Subject: [PATCH] definitions: fix state_leb, proofs related to that function This fix an issue in state_leb, in which an instruction in a later stage would be less advanced than an instruction in an earlier stage with a lower latency. This also adds two lemmas related to comparison to simplify more complex theorems. Signed-off-by: Alban Gruin <alban.gruin@irit.fr> --- src/definitions.v | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/src/definitions.v b/src/definitions.v index 1e934bc..788c278 100644 --- a/src/definitions.v +++ b/src/definitions.v @@ -2,7 +2,7 @@ various related proofs. *) (* They may or may not be useful… *) -Require Import Bool List Nat. +Require Import Bool List Nat PeanoNat. Import ListNotations. (* Basic definitions: opcodes, stages, store buffer state. *) @@ -119,9 +119,21 @@ Definition state := (stage * nat)%type. (* Comparison between two states. *) Definition state_leb st1 st2 := match st1, st2 with - | (s1, n1), (s2, n2) => leb s1 s2 && Nat.leb n2 n1 + | (s1, n1), (s2, n2) => + if stage_beq s1 s2 then + Nat.leb n2 n1 + else + leb s1 s2 end. +Lemma state_leb_eq_true : forall st, state_leb st st = true. +Proof. + intro st. + destruct st. + simpl. + now rewrite stage_beq_eq_true, Nat.leb_le. +Qed. + (* Type definitions etc. *) Definition instr_kind := (opcode * state)%type. Definition trace_kind := list instr_kind. @@ -135,6 +147,16 @@ Definition compare_two (e1 e2 : option instr_kind) := | Some (_, st1), Some (_, st2) => state_leb st1 st2 end. +Lemma compare_two_eq_true : forall e, e <> None -> compare_two e e = true. +Proof. + intros e Hn. + destruct e. + - destruct i. + simpl. + now rewrite state_leb_eq_true. + - contradiction. +Qed. + Definition get_opc (trace : trace_kind) := fst (List.split trace). -- GitLab