[CakeML-Dev] translator + CF breaks ioProgLib

[Ramana Kumar]

Hi Magnus,

The proof in ioProgLib does not work on the translator-cf-basic branch, so
I don't want to merge it into master yet. I tried fixing it, but it's not a
trivial fix, and you might like to comment on the strategy. The problem
stems from the "junk" references that the translator now must assume that
any constant declaration might produce.

In ioProgLib, you prove lemmas (like raw_evaluate_prog) of the form:
(CHAR_IO * one FFI_split * STDIN input * STDOUT [])
     (st2heap p (auto_state_2 ffi)) ⇒ ...
The heap predicate there is simply taken from the specification of the main
program. The problem is that this assumption is no longer true. The heap of
auto_state_2 also includes the junk references. So this lemma becomes
useless.

What we do have is a lemma of the form:
|- ∀h_i h_k st.
     SPLIT (st2heap p st) (h_i,h_k) ⇒
     (CHAR_IO * one FFI_split * STDIN input * STDOUT []) h_i ⇒ ...

Previously, you would instantiate h_i with the whole auto_state_2 and h_k
with the empty heap. Now we need to figure out how to extract the junk
references to put them into h_k. Do you have any ideas? I guess I could
start with st2heap p (auto_state_2 ffi) and the delete the junk...

For more clarification of what auto_state_2 contains, here is what I get
from EVAL:
store2heap (auto_state_2 (io_ffi input)).refs =
   Mem 0 (W8array [0w]) INSERT
   store2heap_aux 1
     (... ++ ... ++ stack_remove_max_stack_alloc_refs ++
      stack_remove_stack_err_lab_refs ++ stack_names_x64_names_refs ++
      stack_names_arm_names_refs ++ lab_to_target_ffi_offset_refs ++
      basisprog_basis_refs ++ x64_dec_fail_refs ++ x64_config_refs ++
      init_env_refs ++ prim_config_refs ++ x64_compiler_config_refs)

This problem blocks the translator-cf-basic merge. I don't know if you
envisioned generalising more of the contents of ioProgLib, or whether it's
already considered in a good state... I would think ideally the main
theorem would follow more directly from what comes out of CF...

Cheers,
Ramana
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20161103/f59bc27e/attachment.html>