Re: [fstar-club] Trying to use List.Tot.map with Kremlin
Correct. There is really no string library except for the few helpers that you
have found. Creating a set of helpers that implement the most needed functions
would be of course extremely useful.
The char type is difficult to deal with, because it is the only C type that is
neither signed or unsigned. Furthermore, we really don't have a powerful model
for C.char in F*. If you want to create a library for dealing with C-style,
zero-terminated strings, I would suggest making this a buffer of uint8 that is
zero-terminated (or that contains at least one zero) -- that way, you get the
benefits of uint8, a type for which we have a model and a variety of functions.
You could then implement C helpers that cast to (char *) at the boundary.
For instance:
* module C.StringBuffer
* type t = b:Buffer.buffer UInt8.t { zero_terminated b }
* val blit_c_string: C.String.t -> t -> n:UInt32.t -> Stack unit (requires
...)
* assume val print: t -> unit
You could then implement C.StringBuffer as follows:
#include "C_StringBuffer.h" // include the auto-generated header
void print (uint8_t *str) {
printf("%s\n", (char *) str); // this is a legal cast in C
}
Hope this helps!
~ jonathan
From: Pierre Beaucamp <m...@pierrebeaucamp.com>
Sent: Wednesday, May 9, 2018 7:32 PM
To: Jonathan Protzenko; Pierre Beaucamp via fstar-club
Subject: Re: [fstar-club] Trying to use List.Tot.map with Kremlin
Hi Jonathan,
thank you again for the tutorial - it is a very valuable resource and filled a
lot of knowledge gaps. I have one more question regarding strings: Is it
correct that there is currently no way to print a buffer of chars? The `server`
example calls printf directly from C, and looking through the libraries, I
couldn't find any fwrite or printf functions to use from Low* itself. (I'm
aware of print_bytes, but that's not really useful for printing chars).
I'd be happy to take a stab at implementing fwrite if that would be useful for
the project.
Best regards,
--
Pierre Beaucamp
On Wed, May 2, 2018, at 11:08 AM, Jonathan Protzenko 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<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%7C37856445ea3248a0ba3108d5b61e54e5%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C636615163759437386=A6pw%2FiNTF%2FUdNQ%2FZ94rxeL720sQiLXZsPyMfXW5lSyc%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 <m...@pierrebeaucamp.com>
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 th
Re: [fstar-club] Trying to use List.Tot.map with Kremlin
Hi Jonathan, thank you again for the tutorial - it is a very valuable resource and filled a lot of knowledge gaps. I have one more question regarding strings: Is it correct that there is currently no way to print a buffer of chars? The `server` example calls printf directly from C, and looking through the libraries, I couldn't find any fwrite or printf functions to use from Low* itself. (I'm aware of print_bytes, but that's not really useful for printing chars). I'd be happy to take a stab at implementing fwrite if that would be useful for the project. Best regards, -- Pierre Beaucamp On Wed, May 2, 2018, at 11:08 AM, Jonathan Protzenko 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 <m...@pierrebeaucamp.com> *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 &l
Re: [fstar-club] Trying to use List.Tot.map with Kremlin
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
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 <cpitclau...@gmail.com> 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 <fstar-club-boun...@lists.gforge.inria.fr> on behalf of > Clément Pit-Claudel via fstar-club <fstar-club@lists.gforge.inria.fr> > *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%7C72f988bf86f141af91ab2d7cd01
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 <fstar-club-boun...@lists.gforge.inria.fr> on behalf of > Clément Pit-Claudel via fstar-club <fstar-club@lists.gforge.inria.fr> > *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 <m...@pierrebeaucamp.com> >> *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 () = >>
Re: [fstar-club] Trying to use List.Tot.map with Kremlin
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 <fstar-club-boun...@lists.gforge.inria.fr> on behalf of Clément Pit-Claudel via fstar-club <fstar-club@lists.gforge.inria.fr> 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 <m...@pierrebeaucamp.com> > *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 u
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://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 <m...@pierrebeaucamp.com> > *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
Re: [fstar-club] Trying to use List.Tot.map with Kremlin
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 <m...@pierrebeaucamp.com>
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 <fstar-club-boun...@lists.gforge.inria.fr> on behalf of
> Pierre Beaucamp via fstar-club <fstar-club@lists.gforge.inria.fr>
> 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
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://fstarlang.github.io/lowstar/
> -- 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 <fstar-club-boun...@lists.gforge.inria.fr> on behalf of
> Pierre Beaucamp via fstar-club <fstar-club@lists.gforge.inria.fr>
> 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
> ___
> fstar-club mailing list
> fstar-club@lists.gforge.inria.fr
> https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.gforge.inria.fr%2Fmailman%2Flistinfo%2Ffstar-club=02%7C01%7Cprotz%40microsoft.com%7C445acbbb8a104079b70808d5af83d2b8%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636607903120375441=WkxhslLqaMBwupJazX4IDfRaWwsqX6IIiuWZT8YrwFc%3D=0
___
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
