<div dir="ltr"><div><div><div>Another (minor?) problem: the top-level vml/Makefile starts with<br><br>all:<br> cd repl/proof; Holmake<br><br></div>but the directory should be<br><br></div> repl/proofs<br><br></div>Konrad.<br>
</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Jan 14, 2014 at 4:20 PM, Magnus Myreen <span dir="ltr"><<a href="mailto:magnus.myreen@cl.cam.ac.uk" target="_blank">magnus.myreen@cl.cam.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I guess it is possible to compose: the translator's certificate<br>
theorem, Ramana's compiler correctness theorem and my verified<br>
bytecode-to-machine-code mapping. The result is a theorem that relates<br>
the original function (fact) with the generated machine code w.r.t.<br>
the ISA. However, the theorem would come with a rather complicated<br>
precondition saying that the compiler's invariant must be met, and<br>
that the initial state of the machine code must be set up to have an<br>
ML heap correctly represented in memory+registers and have the<br>
runtimes helper routines (including the GC) hanging around in the<br>
machine state.<br>
<br>
Cheers,<br>
Magnus<br>
<div class="HOEnZb"><div class="h5"><br>
On 15 January 2014 08:55, Konrad Slind <<a href="mailto:konrad.slind@gmail.com">konrad.slind@gmail.com</a>> wrote:<br>
> Specific application: one example would be a guard (a HOL function)<br>
> generated from a Guardol program. The input and output for the guard<br>
> are supplied by other code or hardware. My specification wouldn't<br>
> mention I/O at all. All I would want is some kind of link between the<br>
> execution<br>
> of the ISA code and the original function.<br>
><br>
> Konrad.<br>
><br>
><br>
><br>
> On Tue, Jan 14, 2014 at 3:24 PM, Magnus Myreen <<a href="mailto:magnus.myreen@cl.cam.ac.uk">magnus.myreen@cl.cam.ac.uk</a>><br>
> wrote:<br>
>><br>
>> On 15 January 2014 08:09, Konrad Slind <<a href="mailto:konrad.slind@gmail.com">konrad.slind@gmail.com</a>> wrote:<br>
>> > Thanks Magnus. I will do as you suggest.<br>
>> ><br>
>> > I haven't absorbed your last point yet, so this is half-baked,<br>
>> > but I can imagine using the compiler to generate executables<br>
>> > that get linked in with I/O components coming from (say) a pre-existing<br>
>> > C library, so that the repl is not involved at all. Is that a possbile<br>
>> > scenario for cakeML?<br>
>><br>
>> Not currently, no. We aren't able to produce stand-alone executables.<br>
>> The invariants haven't been set up for the compiler to be used as a<br>
>> stand-alone thing. Hmmm... Do you have some specific application in<br>
>> mind? I'm guessing you'd like a foreign function interface.<br>
>><br>
>> Regarding pre-existing C libraries: the current implementation of<br>
>> CakeML uses C's getc and putc for I/O, but these are code pointers<br>
>> that are passed into the verified blob of machine code and the proofs<br>
>> make assumptions about these code pointers (e.g. a call to putc puts<br>
>> the input char onto some output stream and then returns control<br>
>> according to the C calling convention). The C code that wraps the<br>
>> verified code (asm_code.s) is here, in case you want to see it:<br>
>><br>
>> <a href="https://github.com/xrchz/vml/blob/master/x86-64/wrapper/wrapper.c" target="_blank">https://github.com/xrchz/vml/blob/master/x86-64/wrapper/wrapper.c</a><br>
>><br>
>> Cheers,<br>
>> Magnus<br>
>><br>
>> > Cheers,<br>
>> > Konrad.<br>
>> ><br>
>> ><br>
>> ><br>
>> > On Tue, Jan 14, 2014 at 2:51 PM, Magnus Myreen<br>
>> > <<a href="mailto:magnus.myreen@cl.cam.ac.uk">magnus.myreen@cl.cam.ac.uk</a>><br>
>> > wrote:<br>
>> >><br>
>> >> Hi Konrad,<br>
>> >><br>
>> >> > I've downloaded cakeML from git and have been building it. I was<br>
>> >> > warned<br>
>> >> > that I needed 16 GB to do everything, so I expected failure. But I<br>
>> >> > wanted<br>
>> >> > to see how far it got before crashing. Here's the error message:<br>
>> >><br>
>> >> As far as I know, the full bootstrap has only been successfully run on<br>
>> >> a 64 GB machine, but maybe Ramana had some data suggesting 16 GB would<br>
>> >> is enough.<br>
>> >><br>
>> >> > 294 declarations still to go<br>
>> >> > 0: (val opn_to_prim2)0 (val div_exc_cn)1 (val cdiv_exc)2 (val<br>
>> >> > eq_exc_cn)3<br>
>> >> > (val ceq_exc)4 (fun pat_to_cpat*)5 (fun exp_to_cexp*)6 (datatype<br>
>> >> > call_context)7 (fun lunion)8 (val lshift)9 (fun free_vars*)10 (val<br>
>> >> > bind_fv)11 (fun label_closures*)12 (val get_label)13 (val pushret)14<br>
>> >> > (fun<br>
>> >> > compile_envref)15 (val compile_varref)16 (val el_check)17 (val<br>
>> >> > bool_to_tag)18 (val unit_tag)19 runtime: 21m34s, gctime: 21m07s,<br>
>> >> > systime: 2m40s.<br>
>> >> > 1: (val block_tag)0 (fun num_fold)1 (val push_lab)2 (val emit_ceref)3<br>
>> >> > (val<br>
>> >> > emit_ceenv)4 (val closure_tag)5 (val cons_closure)6 (val<br>
>> >> > update_refptr)7<br>
>> >> > (val compile_closures)8 (val prim1_to_bc)9 (val prim2_to_bc)10 (fun<br>
>> >> > compile*)Warning - Unable to increase stack - interrupting thread<br>
>> >> > runtime: 17m06s, gctime: 16m47s, systime: 3m42s.<br>
>> >> > Exception- Interrupt raised<br>
>> >> > Holmake: Failed script build for compileReplDecsScript - exited with<br>
>> >> > code 1<br>
>> >> > make: *** [all] Error 1<br>
>> >> ><br>
>> >> ><br>
>> >> > Questions:<br>
>> >> ><br>
>> >> > 1. Is this the expected place of failure? (This is on an 8 GB box<br>
>> >> > running<br>
>> >> > PolyML 5.5).<br>
>> >><br>
>> >> That looks like the expected choke point.<br>
>> >><br>
>> >> > 2. I just invoked "make" in the top level. What is the invocation if<br>
>> >> > I<br>
>> >> > wanted to avoid<br>
>> >> > the memory-expensive bootstrap?<br>
>> >><br>
>> >> You'll need to replace<br>
>> >><br>
>> >> vml/bootstrap/compileReplDecsScript.sml<br>
>> >><br>
>> >> with<br>
>> >><br>
>> >> vml/bootstrap/compileReplDecsCheatScript.sml<br>
>> >><br>
>> >> and also delete "Cheat" in the second line in the file, i.e. the<br>
>> >> new_theory command.<br>
>> >><br>
>> >> > 2a. The build needs lem. This should be mentioned.<br>
>> >><br>
>> >> Yes, lem is required for silly Holmake reasons.<br>
>> >><br>
>> >> > 2b. In lem, the hol-lib directory has a spurious file called<br>
>> >> > stringScript.sml that<br>
>> >> > derails the build. I've talked to Scott about this already.<br>
>> >> ><br>
>> >> > 3. I would like to explore the verification aspects of the system. In<br>
>> >> > particular, suppose<br>
>> >> > I want to define (executable) functions in HOL and prove<br>
>> >> > properties,<br>
>> >> > then somehow<br>
>> >> > map the functions to cakeML and get some sort of<br>
>> >> > "correctness-of-compilation"<br>
>> >> > theorem out that I can use to make a formal connection between<br>
>> >> > the<br>
>> >> > properties, the<br>
>> >> > function, and the executable code.<br>
>> >> ><br>
>> >> > For example, I define factorial and prove that it is always<br>
>> >> > positive:<br>
>> >> ><br>
>> >> > val fact_def = Define `fact n = if n <= 0 then 1 else n * fact<br>
>> >> > (n-1)`;<br>
>> >> > (* The fact function could be over integers, if need be. *)<br>
>> >> ><br>
>> >> > val fact_pos = prove(``!n. 0 < fact n``, ....);<br>
>> >> ><br>
>> >> > ... and now what steps do I take? I have read the relevant<br>
>> >> > papers<br>
>> >> > by<br>
>> >> > Magnus and<br>
>> >> > others, but now I am seeking more concrete hints.<br>
>> >><br>
>> >> To turn your fact function into CakeML, you'll need to run it through<br>
>> >> the translator, i.e. write a file like<br>
>> >><br>
>> >> vml/translator/ml_translator_demoScript.sml<br>
>> >><br>
>> >> for your fact function, which can use num. The translator turns HOL<br>
>> >> ``:num`` into CakeML ints and maintains an invariant that the CakeML<br>
>> >> ints are not negative.<br>
>> >><br>
>> >> To reason about the machine code or bytecode that executes this CakeML<br>
>> >> is a bit more tricky. The top-level theorem makes a statement about<br>
>> >> the whole system in terms of an input stream of characters and an<br>
>> >> output stream of characters. I guess we'd need a verified pretty<br>
>> >> printer to turn CakeML AST into a string that is guaranteed to parse<br>
>> >> back as that CakeML AST. Alternatively, one can try to evaluate (in<br>
>> >> the logic) a the application of the parser to a string representing<br>
>> >> that AST and check that the parser maps that string into the desired<br>
>> >> AST. Then you'll need to somehow talk about your fact function in the<br>
>> >> context of all the other code that gets input during execution of the<br>
>> >> read-eval-print loop. The final theorem would be about the output<br>
>> >> string and terminate/diverge behaviour of the entire system with the<br>
>> >> fact function fed in on the input stream.<br>
>> >><br>
>> >> I'm rather vague about the last parts because we haven't yet worked<br>
>> >> through all the details. But we aim to do so in conjunction with the<br>
>> >> verified HOL light case study.<br>
>> >><br>
>> >> Cheers,<br>
>> >> Magnus<br>
>> >><br>
>> >> > Thanks,<br>
>> >> > Konrad.<br>
>> >> ><br>
>> >> ><br>
>> >> > _______________________________________________<br>
>> >> > Users mailing list<br>
>> >> > <a href="mailto:Users@cakeml.org">Users@cakeml.org</a><br>
>> >> > <a href="https://lists.cakeml.org/listinfo/users" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
>> >> ><br>
>> ><br>
>> ><br>
><br>
><br>
</div></div></blockquote></div><br></div>