Denis Merigoux

AES256-CBC

1

Specifications for AES256 with sboxes (not constant time), and AES256-CBC. Both specs are tested.

In `hir_to_rustspec.rs`, we populate the typechecking context with function signatures coming from all the dependent crates. Then, for each function or method call that we find in the source code,...

To match Rust compiler's behavior.

Similar to conditional statements, hacspec should get conditional matches where each branch return `unit`.

Like #172 shows, some bugs of the typechecker are related to the code in `hir_to_rustspec.rs`, and the logic of how it imports symbols from external crates that the current crate...

Related messages : https://hacspec.zulipchat.com/#narrow/stream/271594-FStar/topic/extraction.20error.200xunknown/near/253561784

* [ ] Chacha20 * [ ] Poly1305 * [ ] Chacha20Poly1305

From the Rust guide: ``` struct Struct; impl Struct { const ID: u32 = 0; } fn main() { println!("the ID of Struct is: {}", Struct::ID); } ```

Name resolution : precedence of local variables or scope variables ?

3

## The problem Consider the following program: ``` declaration scope X: ... declaration scope Foo: x scope X internal y content integer scope Foo: definition y equals let x equals...