coq/correctness: Update CircuitCorrectness.v and Correctness.v (#7)

I forgot to update these files when I introduced the interp_cycle APIs. Reported-by: @mbty
mit-plv · Apr 13, 2021 · 69ca343 · 69ca343
1 parent 37a4d8b
commit 69ca343
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 5 deletions.
diff --git a/coq/CompilerCorrectness/CircuitCorrectness.v b/coq/CompilerCorrectness/CircuitCorrectness.v
@@ -1568,7 +1568,7 @@ Section CompilerCorrectness.
       circuit_env_equiv ->
       forall (idx: reg_t),
         interp_circuit (REnv.(getenv) (compile_scheduler' rc rules external s) idx) =
-        REnv.(getenv) (interp_cycle cr csigma rules s) idx.
+        REnv.(getenv) (interp_cycle csigma rules s cr) idx.
   Proof.
     intros; unfold compile_scheduler', interp_cycle, interp_scheduler, commit_update, commit_rwdata.
     rewrite !getenv_map, !getenv_create; cbn.

diff --git a/coq/CompilerCorrectness/Correctness.v b/coq/CompilerCorrectness/Correctness.v
@@ -42,10 +42,8 @@ Section Thm.
     Proof.
       cbv zeta; intros.
       setoid_rewrite compile_scheduler'_correct.
-      - rewrite scheduler_lowering_correct.
-        unfold lower_r, lower_log;
-          rewrite SemanticProperties.commit_update_log_map_values, getenv_map;
-          reflexivity.
+      - rewrite cycle_lowering_correct.
+        unfold lower_r, lower_log; rewrite getenv_map; reflexivity.
       - apply circuit_env_equiv_CReadRegister.
     Qed.
   End Standalone.