diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-05 16:18:47 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-05 16:18:47 +0200 |
| commit | 804339839051759c5c77e63232d0aec25bb3846d (patch) | |
| tree | 24f38be76b659cd03849d1ef07f46f06daafd648 /scheduling/BTL_SEsimuref.v | |
| parent | ed7397533af0f850688256f07a2c5a22d6c58615 (diff) | |
| download | compcert-kvx-804339839051759c5c77e63232d0aec25bb3846d.tar.gz compcert-kvx-804339839051759c5c77e63232d0aec25bb3846d.zip | |
lemma on HC_set_reg
Diffstat (limited to 'scheduling/BTL_SEsimuref.v')
| -rw-r--r-- | scheduling/BTL_SEsimuref.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index 60c49e04..c812c607 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -44,6 +44,17 @@ Definition ris_sreg_set (ris: ristate) (sreg: PTree.t sval): ristate := ok_rsval := ok_rsval ris; ris_sreg := sreg |}. +Lemma ris_sreg_set_access (ris: ristate) (sreg: PTree.t sval) r smem rsval: + {| ris_smem := smem; + ris_input_init := ris_input_init ris; + ok_rsval := rsval; + ris_sreg := sreg |} r = + ris_sreg_set ris sreg r. +Proof. + unfold ris_sreg_set, ris_sreg_get; simpl. + reflexivity. +Qed. + 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 |