feat(annotations): initial parser crate #266
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
reo101
force-pushed
the
feat/new-annotation-parser
branch
3 times, most recently
from
2c8ecbe to
d0661a6
Compare
reo101
force-pushed
the
feat/new-annotation-parser
branch
3 times, most recently
from
c9f421f to
20116d8
Compare
- `State` passing around parsers, carrying important type information - `pub`-licize some functions in the `noirc_evaluator` module
Start working towards using Noir as a library without modifying internal structures (like extending the AST). Defined a new module `fv-bridge` which contains the functions for compiling a program and converting it to a VIR Krate.
Attach the FV annotations to the monomorphized AST which was converted to VIR form. The functions were duplicated to allow verification of programs written using either the old or the new syntax. This feature will be available only temporary.
You can now run `nargo fv --new-syntax` to verify programs which use the new-syntax for the FV annotations. If the flag `--new-syntax` is not provided you will be able to verify programs which use the old syntax. The new syntax is the following one `#[requires(expr)]` -> `#['requires(expr)]` `#[ensures(expr)]` -> `#['ensures(expr)]` `#[ghost]` -> `#['ghost]`
Move to the new FV annotation syntax for the formal verification tests.
- First end to end working state - we have some basic tests working with the `--new-syntax` - Change `Input` type to `(&str, &State)`, since we need a lot of data for the type-checking done (for now, see below) - `impl` a plethora of `nom` traits, needed to have the new `Input` function as a `nom` `Parser` input type (mostly delegates to the `&str` methods) - Make more helpers for creating `vir` types (`Expr`, `Location`, etc.) - Parse all operators (hopefully) correctly (all binary and unary) - Parse actual attributes - Make work on using a better error type (see below) - Introduce `CompileOrResolverError` and friends to correctly propagate the annotation parsing errors upwards in the stack (solved a TODO) - Correctly add the `main` annotations to `new_ids_to_old_ids` - Add support for the `--new-syntax` flag in the `nargo_cli` `build.rs` TODO: - Make new (simpler) `AST` type, parse the attributes into that, and do the type-checking and infering at a later stage (since we cannot do it fully directly) - Parse quantifiers (won't work with current `&State` approach) - Parse array and tuple indexing - Correctly replace error with out own in all parsers, maybe ever `assert!` that `nom`'s `ParseError::from_error_kind` is never called
Make a minimal `AST` `ExprF` type, wrapping it with a `Cofree`-style
recursive *annotating* `struct`, which inserts arbitrary data (generic)
at each *recursion* level.
That is used to have a few different "versions" of the same `AST`,
depending on what phase we're in:
- pure parsing (`OffsetExpr`): just keeping context-free offset from the
start of the input `&str` (two numbers)
- span attachment (`SpannedExpr`): convert the offsets to real `Noir`
`Span`s, referring to the real place in code (both file and location
inside of it)
- type checking (`Spanned{Optionally,}TypedExpr`): type-infer and add
`Noir` `Type` information to all expressions (using an intermediary
`SpannedOptionallyTypedExpr` for when we're still not sure of integer
literals' types, as they have to come from above)
All of the conversions between the different stages are implemented as
variants of a [catamorphism](https://en.wikipedia.org/wiki/Catamorphism)
and its derivatives.
Also split all the code in separate modules (`ast`, `parse`, `typing`),
with some of the main driver logic in the top-level `lib.rs`
TODO:
- Connection with the rest of the codebase
- Quantifiers (parsing and type inference)
- Array and tuple indexing (parsing and type inference)
- Better errors (still...)
- More organization of the API itself (cleaner `lib.rs`, etc.)
- More tests
Remnants of the old `Input` type, which required two lifetimes
- Erroneously left out from some prior experiments - Also fix default `devShell` to not provide a nightly toolchain but a stable one
Also add a few more `TODO`s
We now call the `parse_attribute` function and the result we pass to the `type_infer` function. The typed attributes are then passed to the unimplemented function `convert_typed_attribute_to_vir_attribute`. The final results are then collected and given to the original pipeline for generating VIR.
- Parse quantifier expressions (with a test) - Implement `nom::error::ContextError` for our `Error` type (now has a field keeping track of all the reported contexts) - Add `context` calls throughout the parser (replaces the now-deleted debug `eprintln!` calls) - Try using `cut` more for better early-errors (for now just in `fn_call` and `quantifier` expressions) - Make a new `try_contextual_cata` for carrying extra context - Employ `try_contextual_cata` in `type_infer` (carry extra bound variables by quantifiers until now) - Type-infer quantifier expressions (their variables employ the same type-inference strategy as number literals) - Change model of `BinaryOp` (one big `enum` again) - Fix type inference for `BinaryOp` (`[&|^]` can act as both arithmetic and boolean operators) - Add test for type-inferring quantifiers (also uses `cata` for verifying the resulting types) TODO: - Parse and type-infer array and tuple indexing expressions - Parse equality operators with a higher precedence (not personal preference, it's just how it's done in `Noir` itself) - In the type-inference algorithm, use a custom type for propagating the "untyped" terms, instead of `Option<NoirType>`
- Create a `bi_can_fit_in` function that finds the smallest type, in which a `BigInteger` can fit and checks if that fits inside a predetermined type. - Use that to verify if all integer literals fit in their inferred types - Add a big test that tests all edge cases
- We now (should) parse much more closely to Noir Example is `a == b | c == d` being `((a == (b | c)) == d)` - Add comments for missing parsers in the correct places (in terms of parsing precedence)
- Correctly parse and type infer array and tuple indexes (array indexes get an index expression, tuple ones get a literal) - Add tests for parsing and type inferrence of array and tuple indexes - Add an array and a tuple to the `empty_state()` parameters (for tests) - Promote `propagate_concrete_type` to a global function (now also used in the `ExprF::Index` type inferrence) TODO: - Better look at the spans of `parse_portfix_expr` - Quantifier/Variable `id` field (needed for the later conversion to `vir`)
- Rename from `test_equality{,_precedence}`
- Change the type of `State`'s `min_local_id` to a `Rc` of a `RefCell`, since we want to modify it without having to mutate the parent `State` (can be done more cleanly with a `Counter` struct, which does the mutation inside and only exposes a `gen_id` function or similar) - Change `try_contextual_cata` to pass the updated context to the current expression (needed to generating the quantified variables' ids early enough) - Now the following tests also pass - `tests::formal_verify_success_exists_big_element_sum` - `tests::formal_verify_success_exists_zero_in_array` - `tests::formal_verify_success_forall_max_is_max` - `tests::formal_verify_success_forall_sum_of_evens`
We now unify the types of the args of each function call with the types of the function's signature.
- Refactor `concretize_type` to return an `Option` - Return a `TypeAnnotationNeededOnArrayLiteral`
Offset the location before calling the function `parse_attribute`. This resolves the TODO in the function `parse_attribute`.
Aristotelis2002
approved these changes
Aug 19, 2025
Aristotelis2002
left a comment
Aristotelis2002
left a comment
There was a problem hiding this comment.
LGTM.
All comments I have left are nits. It would be nice if you address them.
We now convert Tuple and Array literals expressions located in FV annotaitons to VIR.
Some tests are failing because we don't support paths and structures in annotations as of yet. We are moving those tests in a "to_be_fixed" directory for now.
Also we are now converting dereference expressions to VIR. Moved the test `fv_std_old` from `formal_verify_to_be_fixed` to `formal_verify_success`.
We now support global variables inside of annotations. We also now type infer variables with paths. We do that by ignoring the path, beacuse in the `state` parameter the paths are already omitted. This means that all tests which use `fv_std` now pass successfully.
We now have a new error type for the case when we have an exec function call inside of FV annotation. Added a test which produces this error.
Adds support for structures by converting all structure access operations to tuple indexing operations. All "to_be_fixed" tests have now been fixed.
We can now call any global variable from any dependency inside of FV annotations. However there is a limitation. The user must always use the full path for constants located in foreign dependencies. Multiple tests are added to show off the feature and its limitation.
Now the user doesn't have to write the full paths for imported global variables if the given variable was already imported via `use`. A test which was previously failing is now fixed.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.