Lucas Franceschino

Overloaded `&`: make non-dependent tuple whenever possible

2

Hi, Recently in a Slack conversation about deprecating the `*` operator for tuples in favor of the overloaded `&` operator, @TWal pointed out that the `&` operator sometimes makes dependent...

### Description ### Checklist - [ ] The description above is sufficient to understand the PR - [ ] The code compiles correctly - [ ] The code is tested...

### Type of Changes - [x] Bugfix - [ ] New Feature - [x] Breaking Change - [ ] Documentation Update - [ ] CI Update ### Description Hacspec used...

### Description This adds basic F*-related CI via a Github action [`.github/workflows/generate_examples_fstar.yml`](https://github.com/W95Psp/hacspec/blob/fstar_equivalence_proofs/.github/workflows/generate_examples_fstar.yml): - extraction of Chacha20 and Poly1305 to F*; - type-checking of those extractions and of their associated equivalence...

Allow unannonated `Some` and `None`

1

### Type of Changes - [x] Bugfix - [x] New Feature - [ ] Breaking Change - [ ] Documentation Update - [ ] CI Update ### Description I forgot...

### Type of Changes - [ ] Bugfix - [ ] New Feature - [ ] Breaking Change - [ ] Documentation Update - [ ] CI Update ### Description...

### Description This (very draft) PR experiments with using generic types in the Hacspec library, to get rid of macros that redefine newtypes and dedicated `impl`s for every use cases....

A Rust variant of arity `n` is extracted as an F* constructor of arity one whose payload is a tuple of size `n`. For instance, the Rust code bellow: ```rust...

Existential quantifications over multiple variables behaves oddly

1

Hi, I just ran into the following issue: discharging by Z3 a proposition consisting of one existential quantification over two variables fails while the same proposition spelled out using two...

Consider the following example: ```fstar class class_a (t: Type0): Type u#1 = { type_a: Type0; f_a: t -> type_a } class class_b (t: Type0): Type u#1 = { super_a: class_a...