Merge pull request #26 from weakmemory/dev-smal-rex-admits

Close some admits in the re-execution proof
weakmemory · Jan 17, 2025 · 4f4f1ea · 4f4f1ea
2 parents b2fe342 + 05491cd
commit 4f4f1ea
Show file tree

Hide file tree

Showing 8 changed files with 1,831 additions and 1,221 deletions.
diff --git a/src/lib/Rhb.v b/src/lib/Rhb.v
@@ -43,6 +43,15 @@ Proof using.
   basic_solver.
 Qed.
 
+Lemma wf_rpo_immE
+    (WF : Wf G) :
+  rpo_imm ≡ ⦗E⦘ ⨾ rpo_imm ⨾ ⦗E⦘.
+Proof using.
+  split; [| basic_solver].
+  unfold rpo_imm. rewrite wf_sbE; vauto.
+  basic_solver 21.
+Qed.
+
 Lemma no_rpo_imm_to_init :
   rpo_imm ≡ rpo_imm ⨾ ⦗fun e => ~is_init e⦘.
 Proof using.

diff --git a/src/reordering/ReordExecNaNb.v b/src/reordering/ReordExecNaNb.v