[CakeML-Dev] translator + CF breaks ioProgLib
magnus.myreen at gmail.com
Thu Nov 3 06:50:27 UTC 2016
You could try adding ' * frame' to the problematic assumption. Here frame
is a variable. -- Magnus
On Thu, 3 Nov 2016 at 07:45, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> 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...
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Developers