[CakeML-Dev] translator + CF breaks ioProgLib

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Thu Nov 3 07:35:10 UTC 2016


I think you might be right. Doing it with ` * frame ` is better. I think
that works.

By the way, I noticed that proving the final theorem takes extremely long
because it must calculate no_dup_top_types and no_dup_mods for
entire_program by EVAL_TAC. Is that expected to take a really long time, or
is it a performance bug on this branch? (I guess it always took a long
time.) It would be nice to avoid having to prove that by EVAL_TAC.

On 3 November 2016 at 18:20, Magnus Myreen <magnus.myreen at gmail.com> wrote:

> OK, but the frame in app won't help with "you prove lemmas (like
> raw_evaluate_prog) of the for". Maybe I'm not getting the whole picture
> here. -- Magnus
>
> On Thu, 3 Nov 2016 at 07:57, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
> wrote:
>
>> OK I might try that, but first I'm going to try instantiating the h_i and
>> h_k better. I think there are some nice lemmas about SPLIT that could be
>> proven and used for this... Adding ' * frame' should not strictly be
>> necessary, because we already have the frame rule built into app.
>>
>> On 3 November 2016 at 17:50, Magnus Myreen <magnus.myreen at gmail.com>
>> wrote:
>>
>> 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...
>>
>> Cheers,
>> Ramana
>>
>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20161103/0ef45f42/attachment.html>


More information about the Developers mailing list