From ed7397533af0f850688256f07a2c5a22d6c58615 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 1 Jul 2021 16:25:05 +0200 Subject: red_PTree lemmas --- scheduling/BTL_SEsimuref.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'scheduling/BTL_SEsimuref.v') diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 66abe6e1..60c49e04 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -38,6 +38,12 @@ Definition ris_sreg_get (ris: ristate) r: sval := end. Coercion ris_sreg_get: ristate >-> Funclass. +Definition ris_sreg_set (ris: ristate) (sreg: PTree.t sval): ristate := + {| ris_smem := ris_smem ris; + ris_input_init := ris_input_init ris; + ok_rsval := ok_rsval ris; + ris_sreg := sreg |}. + Record ris_ok ctx (ris: ristate) : Prop := { OK_RMEM: (eval_smem ctx (ris_smem ris)) <> None; OK_RREG: forall sv, List.In sv (ok_rsval ris) -> eval_sval ctx sv <> None -- cgit