karamel
karamel copied to clipboard
FStarLang
KaRaMeL is a tool for extracting low-level F* programs to readable C code
Access to a F* (or Steel) reference `r` is currently extracted to C as `r[0]`, both for reading and writing. Currently, the only way to produce `*r` instead has been...
This is a follow-up issue to FStarLang/FStar#2664 . @msprotz proposed an optimized implementation of `Steel.ST.Reference.with_local` without the need for anything like `EPushFrame`/`EPopFrame`, hoping to avoid unnecessary `let res = ...`...
krml performs a def-use analysis to detect unused variables; if they are trivially readonly, these are just skipped from the code-gen; if they are not obviously readonly (e.g. function call),...
Needs https://github.com/FStarLang/FStar/pull/2658 before we can get a green
## What works In general, Karamel is pretty good at erasing non-informative types away from tuple types. Consider for instance the following Low* code: ```fstar module TH module B =...
This reverts commit bb5a50cf71e622f7a75a049683ab25c17dd0eded. Placeholder until I figure out why this broke HACL*.
Following our discussion, here's a proposed fix for the type names. Please let me know if this works as intended. Thanks!
I don't mind which version to use but the warnings about this are annoying, let's decide on a casing.
Hi, with this patch, I was able to compile Kremlin on a POSIX-friendly environment, which means: 1. replace `which` by the POSIX `command -v` 2. replace `bash` by POSIX `sh`...
