update mmio_info in pan_to_targetProof

CakeML · Mar 6, 2024 · 5847f49 · 5847f49
1 parent 7569986
commit 5847f49
Showing 1 changed file with 4 additions and 5 deletions.
diff --git a/pancake/proofs/pan_to_targetProofScript.sml b/pancake/proofs/pan_to_targetProofScript.sml
@@ -302,11 +302,10 @@ val pan_installed_def = Define`
          MAP (\rec. rec.entry_pc + mc_conf.target.get_pc ms) shmem_extra =
          DROP i mc_conf.ffi_entry_pcs ∧
          mc_conf.mmio_info =
-         (λindex. EL (index − i)
-                     (MAP
-                      (\rec. (rec.nbytes, rec.access_addr, rec.reg,
-        rec.exit_pc + mc_conf.target.get_pc ms))
-      shmem_extra)) /\
+         ZIP (GENLIST (λindex. index + i) (LENGTH shmem_extra),
+             (MAP (λrec. (rec.nbytes, rec.access_addr, rec.reg,
+                        rec.exit_pc + mc_conf.target.get_pc ms))
+                                                           shmem_extra)) ∧
     cbspace + LENGTH bytes + ffi_offset * (i + 3) < dimword (:'a))`;
 
 Theorem pan_installed_imp_installed: