<div dir="ltr"><div>I think you might be right. Doing it with ` * frame ` is better. I think that works.<br><br></div>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.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 3 November 2016 at 18:20, Magnus Myreen <span dir="ltr"><<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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<div class="HOEnZb"><div class="h5"><br><div class="gmail_quote"><div dir="ltr">On Thu, 3 Nov 2016 at 07:57, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr" class="m_-3215181839604206033gmail_msg">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.<br class="m_-3215181839604206033gmail_msg"></div><div class="gmail_extra m_-3215181839604206033gmail_msg"><br class="m_-3215181839604206033gmail_msg"><div class="gmail_quote m_-3215181839604206033gmail_msg">On 3 November 2016 at 17:50, Magnus Myreen <span dir="ltr" class="m_-3215181839604206033gmail_msg"><<a href="mailto:magnus.myreen@gmail.com" class="m_-3215181839604206033gmail_msg" target="_blank">magnus.myreen@gmail.com</a>></span> wrote:<br class="m_-3215181839604206033gmail_msg"><blockquote class="gmail_quote m_-3215181839604206033gmail_msg" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">You could try adding ' * frame' to the problematic assumption. Here frame is a variable. -- Magnus<div class="m_-3215181839604206033m_-3229708715087100730HOEnZb m_-3215181839604206033gmail_msg"><div class="m_-3215181839604206033m_-3229708715087100730h5 m_-3215181839604206033gmail_msg"><br class="m_-3215181839604206033gmail_msg"><div class="gmail_quote m_-3215181839604206033gmail_msg"><div dir="ltr" class="m_-3215181839604206033gmail_msg">On Thu, 3 Nov 2016 at 07:45, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" class="m_-3215181839604206033gmail_msg" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>> wrote:<br class="m_-3215181839604206033gmail_msg"></div><blockquote class="gmail_quote m_-3215181839604206033gmail_msg" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr" class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"><div class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"><div class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"><div class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"><div class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">Hi Magnus,<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"><br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"></div>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.<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"><br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"></div>In ioProgLib, you prove lemmas (like raw_evaluate_prog) of the form:<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">(CHAR_IO * one FFI_split * STDIN input * STDOUT [])<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">     (st2heap p (auto_state_2 ffi)) ⇒ ...<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"></div>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.<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"><br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"></div>What we do have is a lemma of the form:<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"><div class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">|- ∀h_i h_k st.<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">     SPLIT (st2heap p st) (h_i,h_k) ⇒<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">     (CHAR_IO * one FFI_split * STDIN input * STDOUT []) h_i ⇒ ...<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"><br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"></div><div class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">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...<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"><br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"></div><div class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">For more clarification of what auto_state_2 contains, here is what I get from EVAL:<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">store2heap (auto_state_2 (io_ffi input)).refs =<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">   Mem 0 (W8array [0w]) INSERT<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">   store2heap_aux 1<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">     (... ++ ... ++ stack_remove_max_stack_alloc_<wbr>refs ++<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">      stack_remove_stack_err_lab_<wbr>refs ++ stack_names_x64_names_refs ++<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">      stack_names_arm_names_refs ++ lab_to_target_ffi_offset_refs ++<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">      basisprog_basis_refs ++ x64_dec_fail_refs ++ x64_config_refs ++<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">      init_env_refs ++ prim_config_refs ++ x64_compiler_config_refs)<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"><br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"></div><div class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">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...<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"><br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"></div><div class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">Cheers,<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"></div><div class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg">Ramana<br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"></div><div class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"><br class="m_-3215181839604206033m_-3229708715087100730m_-3218333519014044309gmail_msg m_-3215181839604206033gmail_msg"></div></div>
</blockquote></div>
</div></div></blockquote></div><br class="m_-3215181839604206033gmail_msg"></div>
</blockquote></div>
</div></div></blockquote></div><br></div>