Tahina Ramananandro (professional account)
Tahina Ramananandro (professional account)
With my colleague @msprotz, we observed segfaults related to 128-bit integers in some Windows OCaml programs using ocaml-stdint. It turns out that even the test executable produced by `make test/stdint_test`...
The automatic introduction of `exists_` and `pure` mechanism in Steel relies on the Steel tactic identifying lemmas by their attributes: 1. It finds all lemmas tagged `solve_can_be_split_lookup`. 2. Among them,...
This PR implements a suggestion by @R1kM : provide a SteelGhost function, `sldump`, to print the current vprop at type-checking time. For instance, the code below (available in this PR...
Currently, when generating a dependency file with `--dep`, F* produces rules for `.krml` files for all modules in the dependency cone of the files provided on the command line argument,...
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 = ...`...
## 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 PR is a partial fix to #139 : with this PR, I can now build KReMLin with dune instead of ocamlbuild. I moved all *.ml* files into the `src/`...
This PR resolves #68 , by clarifying the behavior of EverParse for the following example (expected to fail): ``` $ cat test1.3d entrypoint typedef struct _point { UINT16 x; UINT16...
If I run `make -C src/3d/tests/extern -j 4` on Cygwin with the mingw64 C compiler, I get the following error message: ``` make[3]: *** No rule to make target 'obj/TestWrapper.h',...