Aymeric Fromherz

I can't remember precisely how they were used, @Chris-Hawblitzel is the expert here. Quickcodes are the custom VC generation for Vale, where the parts of the VCs operating on registers...

> > from my understanding there is now work done inside the rust compiler that does export [lifetime] information, but not sure how easy to use > > If there...

Another observation was that if we manually add a trailing (), in theory mimicking the insertion of a return by the typechecker for the weakening, this also works fine.

This has been tracked by @nikswamy to an issue in the interactive mode, these files verify from the command line. We need to debug further and fix the issue. In...

Part of the issue seems to be related to an aggressive normalization of fst/snd in the Steel tactic. Using a custom fst/snd inside the tactic so that all fst/snd are...

Minimizing further, the following test4 fails: ``` let test4 (a:Type) (len:U32.t) (v0:contents a { length v0 == U32.v len }) (src:array a) (xx:t) : SteelT unit (is_array src v0 `star`...

We discussed this issue during today's Steel meeting. As mentioned by Aseem, the problem is that the tactic context does not contain the logical context. As such, when some SMT...

The first one is due to a limitation where there is no smt fallback in can_be_split_post. I'm currently not sure how we could add it, encoding an abstract smt fallback...

The second one is a bit more complex. The problem occurs when the smt fallback path operates on a term containing unresolved implicit(s). In your example, unification is attempted between...

Some progress on this, PR FStarLang/FStar#2227 addresses issue 3, fixing errors in the unifier. Still investigating the SMT failures.