Results 9 issues of Marco Stronati

Using the command ` cargo hax --cargo-args --tests \; into fstar` ``` error[HAX0001]: (AST import) something is not implemented yet. Pointer, with [cast] being (Types.ClosureFnPointer Types.Normal) --> tests/main.rs:22:1 | 21...

enhancement
engine

Temporary mitigation to https://github.com/0xMiden/miden-vm/issues/1873 and https://github.com/0xMiden/miden-base/issues/1441 and waiting for the better solution described in https://github.com/0xMiden/miden-vm/issues/1776. This PR introduces the function `clear_debug_info` that allows to strip a compiled program or library...

assembly
debugging

When testing a script with an advice map using the test-utils framework, even if the map is correctly loaded by the host, the event handler is unable to find the...

assembly
tests

This PR removes from the ast the typed push instructions Push{U8,U16,U32,Flet,Word} in favor of the generic `Push` instruction that takes an `IntValue`. This simplifies the ast and the parser, however...

assembly

https://github.com/0xMiden/miden-vm/pull/1855 introduced support for word constants, the documentation should explain the syntax to define them.

documentation
assembly

### What should be done? The vendoring PR #1643 should test that the adviceMap of a vendored library is copied to assembled library. It's not easy to create MAST Forest...

assembly
tests

In PR https://github.com/0xPolygonMiden/miden-vm/pull/1771/ 4 tests in `miden/tests/integration/cli/cli_test.rs` using `is_prime.masp` were removed because they relied on an assert syntax that was modified and no sources were easily available. The test should...

tests

When using reify with an effect with a simple option monad, there is a very weird behavior if there is a non-trivial wp. The option pattern matching returns an "incomplete...

When writing a function that takes a dependent tuple as argument, if the argument is decorated with a type annotation, it is ignored. ``` module Bug_dtuple type d = r:nat...