Aymeric Fromherz

Enable subtyping in ctrl_rewrite (and hence, l_to_r)

2

#2476 reported issues when using `l_to_r` to perform rewritings. `l_to_r` is based on the primitive `ctrl_rewrite`, which traverses all subterms `t` of a given term, creates a goal of the...

Steel effect: Assume requires clause when typechecking ensures

1

Consider the following toy example, as reported by @cmovcc: ```fstar let test (x: nat) : Steel nat emp (fun _ -> emp) (requires (fun _ -> x > 0)) (ensures...

Steel work items

1

Recapping here the list of Steel work items **Code Refactoring** - [x] Replace SteelAtomic unobservable and SteelAtomic observable by SteelGhost and SteelAtomic - [ ] Remove the quantification on invariant_names...

Executing the P256 spec in OCaml leads to a stack overflow

4

While testing the HPKE spec in OCaml, I reliably hit stack overflow errors when the ciphersuite involved P256. After debugging, it seems that the culprit is the redefinition of exponentiation...

Similar to what is done for other specs, which would also avoid the need for the specific ci target `test-hpke`. See #553 for a more detailed description of the issue

This PR adds a new variant of the Steel `for_loop` combinator called `for_loop_full`, which supports the additional use of a selector invariant on top of the current vprop invariant. Note,...

This PR adds a new function, called `malloca_of_list` to Steel. Similarly to what was done in Low*, this function takes a list literal, and allocates a new array statically initialized...

Bad interaction between unused variable elimination and "let x = if ... in" hoisting

1

This issue is based on the following comment in one of the HACL PRs: https://github.com/hacl-star/hacl-star/pull/611#discussion_r974402228 The problematic code has the shape `let c = BN.bn_add args in Ghost.hide c`, where...

F* over TRAMP crashes

17

I'm trying to run F* over TRAMP, and get the following error: F*: subprocess exited. error in process filter: fstar-subp--process-response: Invalid state: Received orphan response "Json parsing failed." to query...

Consider the following code: ```fstar module Test inline_for_extraction noextract val f (x:int) : unit noextract inline_for_extraction let f x = () ``` Attempting to typecheck currently raises the following error...