Re: [fstar-club] Trying to use List.Tot.map with Kremlin

[Clément Pit-Claudel via fstar-club]

On 2018-05-02 12:08, Jonathan Protzenko wrote:
> I generally use meta-programming to refer to any partial program
> evaluation that is performed by F* at type-checking time instead of
> being performed at run-time, but perhaps that's an incorrect term...
> any suggestions for a better term? 

I usually just call it partial evaluation, as you did above :)
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club

Re: [fstar-club] Trying to use List.Tot.map with Kremlin

[Jonathan Protzenko via fstar-club]

So contrary to what I said, this works, and String.concat is correctly reduced:

module Test

open FStar.HyperStack.ST

 let main (): St C.exit_code =
   C.String.(print !$(normalize_term (String.concat ", " ["hello"; 
"world"])));
   C.EXIT_SUCCESS

compile it with krml -no-prefix Test -add-include '"kremstr.h"'

I generally use meta-programming to refer to any partial program evaluation 
that is performed by F* at type-checking time instead of being performed at 
run-time, but perhaps that's an incorrect term... any suggestions for a better 
term? 


~ jonathan


From: Clément Pit-Claudel 
Sent: Wednesday, May 2, 2018 9:02 AM
To: Jonathan Protzenko; Clément Pit-Claudel via fstar-club
Subject: Re: [fstar-club] Trying to use List.Tot.map with Kremlin

Hmm, I don't think this involves meta-programming; normalize_term is a pure 
function with special support in the compiler.

The meta-programming version would look like this, rather:

open FStar.Tactics

let main () : int =
  C.print_string (C.string_of_literal (synth_by_tactic (fun () ->
  let body = `(String.concat ", " ["hello"; "world"]) in
  exact (norm_term [primops; delta; iota; zeta] body;
  C.exit_success

Clément.


On 2018-05-02 11:47, Jonathan Protzenko wrote:
> Yes -- you can always meta-program as much as you want, although:
>
>   * meta-programming support is limited for string functions -- I think only 
> String.length can be meta-evaluated
>   * the chapter on meta-programming Low* hasn't been written yet in the 
> tutorial .
>
>
> ~ jonathan
>
> --
> *From:* fstar-club  on behalf of 
> Clément Pit-Claudel via fstar-club 
> *Sent:* Wednesday, May 2, 2018 8:44 AM
> *To:* fstar-club@lists.gforge.inria.fr
> *Subject:* Re: [fstar-club] Trying to use List.Tot.map with Kremlin
>
> I'd expect the following to work, though. Does it?
>
>  let main () =
>C.print_string (C.string_of_literal (normalize_term (String.concat ", 
> " ["hello"; "world"])));
>C.exit_success
>
> … though maybe we don't apply `normalize_term` early enough.
>
> Clément.
>
> On 2018-05-02 11:08, Jonathan Protzenko via fstar-club wrote:
>> Yes, this is something that has poor usability. Prims.string and 
>> FStar.String.concat are supported as transition mechanisms to help porting 
>> F* programs to Low* but I agree that it's confusing for beginners to have 
>> them work "by default".
>>
>> https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Ffstarlang.github.io%2Flowstar%2Fhtml%2FLowStar.html%23c-string-literals=02%7C01%7Cprotz%40microsoft.com%7C6270df4eb0a244eaac3908d5b043b2d5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636608727210614165=ffbZwtJJ2ud7JXMhD56SL3Kyv15X%2BEYQT87%2Bc%2BlLFgY%3D=0
>>  has a note that explains it, my plan is to make it a warning that's fatal 
>> by default, and that can be disabled if you need these mechanisms
>>
>> ~ jonathan
>>
>> 

Re: [fstar-club] Trying to use List.Tot.map with Kremlin

[Clément Pit-Claudel via fstar-club]

Hmm, I don't think this involves meta-programming; normalize_term is a pure 
function with special support in the compiler.

The meta-programming version would look like this, rather:

open FStar.Tactics

let main () : int =
  C.print_string (C.string_of_literal (synth_by_tactic (fun () ->
  let body = `(String.concat ", " ["hello"; "world"]) in
  exact (norm_term [primops; delta; iota; zeta] body;
  C.exit_success

Clément.


On 2018-05-02 11:47, Jonathan Protzenko wrote:
> Yes -- you can always meta-program as much as you want, although:
> 
>   * meta-programming support is limited for string functions -- I think only 
> String.length can be meta-evaluated
>   * the chapter on meta-programming Low* hasn't been written yet in the 
> tutorial .
> 
> 
> ~ jonathan
> 
> --
> *From:* fstar-club  on behalf of 
> Clément Pit-Claudel via fstar-club 
> *Sent:* Wednesday, May 2, 2018 8:44 AM
> *To:* fstar-club@lists.gforge.inria.fr
> *Subject:* Re: [fstar-club] Trying to use List.Tot.map with Kremlin
>  
> I'd expect the following to work, though. Does it?
> 
>  let main () =
>    C.print_string (C.string_of_literal (normalize_term (String.concat ", 
> " ["hello"; "world"])));
>    C.exit_success
> 
> … though maybe we don't apply `normalize_term` early enough.
> 
> Clément.
> 
> On 2018-05-02 11:08, Jonathan Protzenko via fstar-club wrote:
>> Yes, this is something that has poor usability. Prims.string and 
>> FStar.String.concat are supported as transition mechanisms to help porting 
>> F* programs to Low* but I agree that it's confusing for beginners to have 
>> them work "by default".
>> 
>> https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Ffstarlang.github.io%2Flowstar%2Fhtml%2FLowStar.html%23c-string-literals=02%7C01%7Cprotz%40microsoft.com%7C6270df4eb0a244eaac3908d5b043b2d5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636608727210614165=ffbZwtJJ2ud7JXMhD56SL3Kyv15X%2BEYQT87%2Bc%2BlLFgY%3D=0
>>  has a note that explains it, my plan is to make it a warning that's fatal 
>> by default, and that can be disabled if you need these mechanisms
>> 
>> ~ jonathan
>> 
>> --
>> *From:* Pierre Beaucamp 
>> *Sent:* Tuesday, May 1, 2018 4:38 PM
>> *To:* Jonathan Protzenko; Pierre Beaucamp via fstar-club
>> *Subject:* Re: [fstar-club] Trying to use List.Tot.map with Kremlin
>>  
>> Thanks for the quick answer Jonathan.
>> 
>> I already assumed that this is caused by limited inter-polarity between F* 
>> strings and their representation in Low*. What threw me off is that this 
>> code works:
>> 
>>     let main () =
>>   C.print_string (C.string_of_literal (String.concat ", " ["hello"; 
>> "world"]));
>>   C.exit_success
>> 
>> Either way, I'm excited for the Low* tutorial - thank you for writing it. 
>> This is a very interesting language with unfortunately very little 
>> documentation for new-comers (I'm pretty much trying to learn F* 

Re: [fstar-club] Trying to use List.Tot.map with Kremlin

[Jonathan Protzenko via fstar-club]

Yes -- you can always meta-program as much as you want, although:

  *   meta-programming support is limited for string functions -- I think only 
String.length can be meta-evaluated
  *   the chapter on meta-programming Low* hasn't been written yet in the 
tutorial .


~ jonathan


From: fstar-club  on behalf of 
Clément Pit-Claudel via fstar-club 
Sent: Wednesday, May 2, 2018 8:44 AM
To: fstar-club@lists.gforge.inria.fr
Subject: Re: [fstar-club] Trying to use List.Tot.map with Kremlin

I'd expect the following to work, though. Does it?

 let main () =
   C.print_string (C.string_of_literal (normalize_term (String.concat ", " 
["hello"; "world"])));
   C.exit_success

… though maybe we don't apply `normalize_term` early enough.

Clément.

On 2018-05-02 11:08, Jonathan Protzenko via fstar-club wrote:
> Yes, this is something that has poor usability. Prims.string and 
> FStar.String.concat are supported as transition mechanisms to help porting F* 
> programs to Low* but I agree that it's confusing for beginners to have them 
> work "by default".
>
> https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Ffstarlang.github.io%2Flowstar%2Fhtml%2FLowStar.html%23c-string-literals=02%7C01%7Cprotz%40microsoft.com%7C6270df4eb0a244eaac3908d5b043b2d5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636608727210614165=ffbZwtJJ2ud7JXMhD56SL3Kyv15X%2BEYQT87%2Bc%2BlLFgY%3D=0
>  has a note that explains it, my plan is to make it a warning that's fatal by 
> default, and that can be disabled if you need these mechanisms
>
> ~ jonathan
>
> --
> *From:* Pierre Beaucamp 
> *Sent:* Tuesday, May 1, 2018 4:38 PM
> *To:* Jonathan Protzenko; Pierre Beaucamp via fstar-club
> *Subject:* Re: [fstar-club] Trying to use List.Tot.map with Kremlin
>
> Thanks for the quick answer Jonathan.
>
> I already assumed that this is caused by limited inter-polarity between F* 
> strings and their representation in Low*. What threw me off is that this code 
> works:
>
> let main () =
>   C.print_string (C.string_of_literal (String.concat ", " ["hello"; 
> "world"]));
>   C.exit_success
>
> Either way, I'm excited for the Low* tutorial - thank you for writing it. 
> This is a very interesting language with unfortunately very little 
> documentation for new-comers (I'm pretty much trying to learn F* and Low* at 
> the same time, and I guess this is where a lot of the confusion is coming 
> from).
>
> Thank you and best regards,
>
> --
> Pierre Beaucamp
>
> On Tue, May 1, 2018, at 7:09 PM, Jonathan Protzenko wrote:
>> Hello Pierre,
>>
>> These are all excellent questions -- I am currently writing a tutorial
>> for Low* are these served as good inspiration for the introduction. If
>> CI goes through, a work-in-progress version of the tutorial should be
>> uploaded in the next few hours at 
>> https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Ffstarlang.github.io%2Flowstar%2F=02%7C01%7Cprotz%40microsoft.com%7Cdb40113318a44ce8c0be08d5afbc9c55%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636608146970557404=aLvfTn4cd9Wrvck8prnVvnQfEA9I3BPpp1%2BE0PkjGpw%3D=0
>> -- please read it and let me know whether after browsing it, your
>> questions have been answered.
>>
>> In case the CI doesn't perform the upload, or the tutorial is unclear,
>> the essence of your issue is that your code is not Low*.
>>
>>   *   the F* string and list types are F* values, i.e. concat has type
>> string -> string -> string; the only way to give you these semantics
>> without requiring the user to track allocations and lifetimes is to use
>> a garbage-collector, which C does not have
>>   *   the same goes for lists: compiling them to C with the current F*
>> value semantics would lead to a zillion uncollected list cell
>> allocations.
>>
>> What the C.String module provides is a bare-bones model of C string
>> literals, i.e. `const char *s 

Re: [fstar-club] Trying to use List.Tot.map with Kremlin

[Clément Pit-Claudel via fstar-club]

I'd expect the following to work, though. Does it?

 let main () =
   C.print_string (C.string_of_literal (normalize_term (String.concat ", " 
["hello"; "world"])));
   C.exit_success

… though maybe we don't apply `normalize_term` early enough.

Clément.

On 2018-05-02 11:08, Jonathan Protzenko via fstar-club wrote:
> Yes, this is something that has poor usability. Prims.string and 
> FStar.String.concat are supported as transition mechanisms to help porting F* 
> programs to Low* but I agree that it's confusing for beginners to have them 
> work "by default".
> 
> https://fstarlang.github.io/lowstar/html/LowStar.html#c-string-literals has a 
> note that explains it, my plan is to make it a warning that's fatal by 
> default, and that can be disabled if you need these mechanisms
> 
> ~ jonathan
> 
> --
> *From:* Pierre Beaucamp 
> *Sent:* Tuesday, May 1, 2018 4:38 PM
> *To:* Jonathan Protzenko; Pierre Beaucamp via fstar-club
> *Subject:* Re: [fstar-club] Trying to use List.Tot.map with Kremlin
>  
> Thanks for the quick answer Jonathan.
> 
> I already assumed that this is caused by limited inter-polarity between F* 
> strings and their representation in Low*. What threw me off is that this code 
> works:
> 
>     let main () =
>   C.print_string (C.string_of_literal (String.concat ", " ["hello"; 
> "world"]));
>   C.exit_success
> 
> Either way, I'm excited for the Low* tutorial - thank you for writing it. 
> This is a very interesting language with unfortunately very little 
> documentation for new-comers (I'm pretty much trying to learn F* and Low* at 
> the same time, and I guess this is where a lot of the confusion is coming 
> from).
> 
> Thank you and best regards,
> 
> -- 
> Pierre Beaucamp
> 
> On Tue, May 1, 2018, at 7:09 PM, Jonathan Protzenko wrote:
>> Hello Pierre,
>> 
>> These are all excellent questions -- I am currently writing a tutorial 
>> for Low* are these served as good inspiration for the introduction. If 
>> CI goes through, a work-in-progress version of the tutorial should be 
>> uploaded in the next few hours at 
>> https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Ffstarlang.github.io%2Flowstar%2F=02%7C01%7Cprotz%40microsoft.com%7Cdb40113318a44ce8c0be08d5afbc9c55%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636608146970557404=aLvfTn4cd9Wrvck8prnVvnQfEA9I3BPpp1%2BE0PkjGpw%3D=0
>> -- please read it and let me know whether after browsing it, your 
>> questions have been answered.
>> 
>> In case the CI doesn't perform the upload, or the tutorial is unclear, 
>> the essence of your issue is that your code is not Low*.
>> 
>>   *   the F* string and list types are F* values, i.e. concat has type 
>> string -> string -> string; the only way to give you these semantics 
>> without requiring the user to track allocations and lifetimes is to use 
>> a garbage-collector, which C does not have
>>   *   the same goes for lists: compiling them to C with the current F* 
>> value semantics would lead to a zillion uncollected list cell 
>> allocations.
>> 
>> What the C.String module provides is a bare-bones model of C string 
>> literals, i.e. `const char *s = "my string literal";`, meaning that you 
>> should provide an actual literal, e.g. `C.String.( print !$"hello, world
>> \n" );`. This is very limited, and does not allow you to do arbitrary 
>> string manipulation.
>> 
>> A proof-of-concept example exists that does that, in the test/ 
>> subdirectory of KreMLin, and is called Server.fst. It models blitting 
>> C.String.t's into a mutable buffer of C chars, tracking how much space 
>> remains in your buffer, whether the buffer is live, etc. and rules out 
>> buffer overflows.
>> 
>> Naturally, it's a little involved for a hello world, but I guess that's 
>> the reality of tracking temporal (liveness) and spatial safety (bounds) 
>> in C.
>> 
>> Let me know if that helps.
>> 
>> Cheers,
>> 
>> Jonathan
>> 
>> 
>> ~ jonathan
>> 
>> 

Re: [fstar-club] Trying to use List.Tot.map with Kremlin

[Jonathan Protzenko via fstar-club]

Yes, this is something that has poor usability. Prims.string and 
FStar.String.concat are supported as transition mechanisms to help porting F* 
programs to Low* but I agree that it's confusing for beginners to have them 
work "by default".

https://fstarlang.github.io/lowstar/html/LowStar.html#c-string-literals has a 
note that explains it, my plan is to make it a warning that's fatal by default, 
and that can be disabled if you need these mechanisms


~ jonathan


From: Pierre Beaucamp 
Sent: Tuesday, May 1, 2018 4:38 PM
To: Jonathan Protzenko; Pierre Beaucamp via fstar-club
Subject: Re: [fstar-club] Trying to use List.Tot.map with Kremlin

Thanks for the quick answer Jonathan.

I already assumed that this is caused by limited inter-polarity between F* 
strings and their representation in Low*. What threw me off is that this code 
works:

let main () =
  C.print_string (C.string_of_literal (String.concat ", " ["hello"; 
"world"]));
  C.exit_success

Either way, I'm excited for the Low* tutorial - thank you for writing it. This 
is a very interesting language with unfortunately very little documentation for 
new-comers (I'm pretty much trying to learn F* and Low* at the same time, and I 
guess this is where a lot of the confusion is coming from).

Thank you and best regards,

--
Pierre Beaucamp

On Tue, May 1, 2018, at 7:09 PM, Jonathan Protzenko wrote:
> Hello Pierre,
>
> These are all excellent questions -- I am currently writing a tutorial
> for Low* are these served as good inspiration for the introduction. If
> CI goes through, a work-in-progress version of the tutorial should be
> uploaded in the next few hours at 
> https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Ffstarlang.github.io%2Flowstar%2F=02%7C01%7Cprotz%40microsoft.com%7Cdb40113318a44ce8c0be08d5afbc9c55%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636608146970557404=aLvfTn4cd9Wrvck8prnVvnQfEA9I3BPpp1%2BE0PkjGpw%3D=0
> -- please read it and let me know whether after browsing it, your
> questions have been answered.
>
> In case the CI doesn't perform the upload, or the tutorial is unclear,
> the essence of your issue is that your code is not Low*.
>
>   *   the F* string and list types are F* values, i.e. concat has type
> string -> string -> string; the only way to give you these semantics
> without requiring the user to track allocations and lifetimes is to use
> a garbage-collector, which C does not have
>   *   the same goes for lists: compiling them to C with the current F*
> value semantics would lead to a zillion uncollected list cell
> allocations.
>
> What the C.String module provides is a bare-bones model of C string
> literals, i.e. `const char *s = "my string literal";`, meaning that you
> should provide an actual literal, e.g. `C.String.( print !$"hello, world
> \n" );`. This is very limited, and does not allow you to do arbitrary
> string manipulation.
>
> A proof-of-concept example exists that does that, in the test/
> subdirectory of KreMLin, and is called Server.fst. It models blitting
> C.String.t's into a mutable buffer of C chars, tracking how much space
> remains in your buffer, whether the buffer is live, etc. and rules out
> buffer overflows.
>
> Naturally, it's a little involved for a hello world, but I guess that's
> the reality of tracking temporal (liveness) and spatial safety (bounds)
> in C.
>
> Let me know if that helps.
>
> Cheers,
>
> Jonathan
>
>
> ~ jonathan
>
> 
> From: fstar-club  on behalf of
> Pierre Beaucamp via fstar-club 
> Sent: Tuesday, May 1, 2018 9:48 AM
> To: fstar-club@lists.gforge.inria.fr
> Subject: [fstar-club] Trying to use List.Tot.map with Kremlin
>
> Hi everyone,
>
> I'm just playing a bit around with F-Star and Kremlin and I seem to be
> stuck at a simple problem. I don't know if I'm missing something obvious
> or if this might be a bug. My code looks like this:
>
> let main () =
>   C.print_string (C.string_of_literal (String.concat ",
> " (List.Tot.map string_of_int [1; 2; 3])));
>   C.exit_success
>
> I expect this code to print `1, 2, 3` but instead I get the following
> runtime error:
>
> KreMLin abort at ./Main.c:9
> This function was not extracted:
> Failure("Cannot extract string_of_literal applied to a non-literal")
>
> I tried some variations of the above program to see if I can reverse-
> engineer what is going on, but as soon as I introduce `List.Tot.map`,
> the code breaks. I know that there is also `C.Loops.map`, but I don't
> know if I really need to use buffers to make it work.
>
> Also, I'm generally interested in learning more about Kremlin / Low* /
> F*. If there are any recommended resources or other helpful links, feel
> free to share them with me.
>
> Thank you and best regards,
>
> --
> Pierre Beaucamp
>