<div dir="ltr"><div><div><div><div>Hi Magnus,<br><br></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><br></div>In ioProgLib, you prove lemmas (like raw_evaluate_prog) of the form:<br>(CHAR_IO * one FFI_split * STDIN input * STDOUT [])<br>     (st2heap p (auto_state_2 ffi)) ⇒ ...<br></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><br></div>What we do have is a lemma of the form:<br><div>|- ∀h_i h_k st.<br>     SPLIT (st2heap p st) (h_i,h_k) ⇒<br>     (CHAR_IO * one FFI_split * STDIN input * STDOUT []) h_i ⇒ ...<br><br></div><div>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><br></div><div>For more clarification of what auto_state_2 contains, here is what I get from EVAL:<br>store2heap (auto_state_2 (io_ffi input)).refs =<br>   Mem 0 (W8array [0w]) INSERT<br>   store2heap_aux 1<br>     (... ++ ... ++ stack_remove_max_stack_alloc_refs ++<br>      stack_remove_stack_err_lab_refs ++ stack_names_x64_names_refs ++<br>      stack_names_arm_names_refs ++ lab_to_target_ffi_offset_refs ++<br>      basisprog_basis_refs ++ x64_dec_fail_refs ++ x64_config_refs ++<br>      init_env_refs ++ prim_config_refs ++ x64_compiler_config_refs)<br><br></div><div>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><br></div><div>Cheers,<br></div><div>Ramana<br></div><div><br></div></div>