Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
87 commits
Select commit Hold shift + click to select a range
6bf4df6
feat(annotations): initial parser crate
reo101 Jul 7, 2025
10a72df
feat(annotations): WIP function calls
reo101 Jul 7, 2025
c910d03
feat(annotations): WIP more function calls
reo101 Jul 7, 2025
5c52271
chore(monomorphizer): Private to pub
Aristotelis2002 Jul 8, 2025
1f8f5ea
feat(fv-bridge): First steps towards new architecture
Aristotelis2002 Jul 8, 2025
d589dc6
feat(fv-bridge): Attach VIR FV annotations to Mon. AST
Aristotelis2002 Jul 10, 2025
8175d96
feat(new-syntax): Add new-syntax support to `nargo fv`
Aristotelis2002 Jul 10, 2025
93bcb3b
chore(tests): Change the syntax of the tests
Aristotelis2002 Jul 11, 2025
37c389f
chore(new-syntax): parse, don't validate
reo101 Jul 11, 2025
b48ac8f
feat(annotations): fully integrate with the rest of the codebase
reo101 Jul 14, 2025
37e426d
feat(annotations)!: new AST and full type inference
reo101 Jul 14, 2025
a2f7e5b
chore(annotations): `<'a, 'b>` -> `<'a>`
reo101 Jul 22, 2025
30ccf2d
fix: stop mistakingly using nightly features
reo101 Jul 14, 2025
d366248
fix(annotations): predicate operations' return type
reo101 Jul 14, 2025
2f054ce
chore(fv_bridge): Use new `formal_verification` module interface
Aristotelis2002 Jul 24, 2025
78922bc
feat(annotations): quantifiers
reo101 Jul 14, 2025
81c4fe1
chore(rust): update to `1.88.0`
reo101 Jul 14, 2025
56ea2fc
feat(annotations): check if integer literals fit in their holes
reo101 Jul 14, 2025
3665291
feat(annotations): reorder all parsers to adhere to upstream Noir
reo101 Jul 14, 2025
fb2de5f
feat(annotations)!: add array and tuple indexing
reo101 Jul 14, 2025
ee70ca4
feat(annotations): assert precedence in `test_equality_precedence`
reo101 Jul 14, 2025
6723ab3
feat(annotations)!: multiple bindings in quantifiers, `id`s in varibles
reo101 Jul 14, 2025
805f673
fix(annotations): correct bit-shifting parsing
reo101 Jul 14, 2025
89ed5f4
fix(annotations): correctly propagate type through predicates
reo101 Jul 14, 2025
c3fce65
fix(annotations): fix parsing of spaces around parenthesis
reo101 Jul 14, 2025
d6c979a
feat(fv-bridge): Typed attributes to VIR
Aristotelis2002 Jul 29, 2025
34d1dbd
feat(annotations): More informative errors when parsing
reo101 Jul 14, 2025
87adca5
chore(annotations): remove old comments
reo101 Jul 14, 2025
927cee2
fix(annotations): Even stricter type inferrence
reo101 Jul 14, 2025
8d1a2c7
feat(annotations): add cast expressions
reo101 Jul 14, 2025
a934df1
feat(annotations): add `location` field to `TypeError`
reo101 Jul 14, 2025
fd78d6f
feat(errors): Error propagation in `fv_bridge`
Aristotelis2002 Jul 31, 2025
b100d4b
refactor(annotations): clean up
reo101 Jul 14, 2025
8677995
chore(typing): Fetch min available local id
Aristotelis2002 Aug 1, 2025
dc65a39
fix(annotations): parse `^` correctly (again)
reo101 Jul 14, 2025
4065cc6
fix(tag_attr): Keep whitespace tokens when parsing
Aristotelis2002 Aug 1, 2025
e440c21
feat(annotations): propagate `Location`s through parser errors
reo101 Jul 14, 2025
71cfa1e
chore(annotations): Reverse order of annotation parsing
Aristotelis2002 Aug 1, 2025
4f80d89
feat(annotations): add support for paths in variables
reo101 Jul 14, 2025
b2deb7e
refactor(annotations): Error type specification location for `fv_bridge`
reo101 Jul 14, 2025
a4ea598
chore(annotations): format
reo101 Jul 14, 2025
6c9d172
feat(annotations): parse and type-infer derefences
reo101 Jul 14, 2025
0f25a8f
chore(annotations): use field punning again after renames
reo101 Jul 14, 2025
19f5f80
feat(annotations): add tuple literals
reo101 Jul 14, 2025
2e89436
feat(annotations): add array literals
reo101 Jul 14, 2025
ab58a51
fix(annotations): parse whitespace around parenthesis (again)
reo101 Jul 14, 2025
0190b76
refactor(annotations): add `OptinalType` type
reo101 Jul 14, 2025
b1eedc8
refactor(annotations): type-inference algorithm for tuples and arrays
reo101 Jul 14, 2025
e68ba1d
fix(annotations): type-infer `IntegerLiteral`s through `UnaryOp`s
reo101 Jul 14, 2025
8e97ec9
chore(annotations): remove redundant `.clone()`
reo101 Jul 14, 2025
9656eda
chore(annotations): remove redundant comment
reo101 Jul 14, 2025
bee644f
refactor(annotations): in-place mutation when type-inferring
reo101 Jul 14, 2025
40047f1
fix(annotations): `empty_state` ids for testing
reo101 Jul 14, 2025
f2dd392
chore(annotations): remove old `eprintln!` call
reo101 Jul 14, 2025
505f4bc
chore(annotations): expand the catch-all case in a `match`
reo101 Jul 14, 2025
8cb5da4
chore(annotations): remove unused imports
reo101 Jul 14, 2025
635f617
refactor(annotations): deduplicate `tuple_elements_from_expr`
reo101 Jul 14, 2025
9df7b17
feat(monomorphizer): Make `queue_function` public
Aristotelis2002 Aug 4, 2025
d465ff1
feat(monomorph): Process monomorphization requests
Aristotelis2002 Aug 5, 2025
7ad2ee0
feat(annotations): assign `LocalId`s to quantified variables
reo101 Jul 14, 2025
d178eb2
feat(annotations): Type infer args in func calls
Aristotelis2002 Aug 18, 2025
abf3a33
fix(annotations): correct `Offset` calculation for `prefix` / `postfix`
reo101 Jul 14, 2025
daf8949
chore(annotations): emit an adequate type errors for array literals
reo101 Jul 14, 2025
191f4c6
chore(annotation): Correct Location before `parse_attribute`
Aristotelis2002 Aug 19, 2025
f35d7c2
feat(annotation-to-vir): Convert cast expressions
Aristotelis2002 Aug 19, 2025
ec5cdd9
feat(annotations-to-vir): Tuple and Array literals
Aristotelis2002 Aug 19, 2025
5476536
chore(tests): Move failing successful tests in fix dir
Aristotelis2002 Aug 21, 2025
3185413
chore(tests): Add some basic tests
Aristotelis2002 Aug 21, 2025
5bb32b4
chore(tests): Remove tmp file
Aristotelis2002 Aug 21, 2025
2d348a8
refactor(annotations): prefer `impl` over `dyn` `Fn` for `cata` `fn`s
reo101 Jul 14, 2025
3206263
chore(annotations): remove old comment linking to `nom` documentation
reo101 Jul 14, 2025
e474dc9
refactor(annotations): remove unneeded `alt` call
reo101 Jul 14, 2025
0e1e7a8
chore(annotations): remove outdated comment about `OptionalType`s
reo101 Jul 14, 2025
07ff027
chore(annotations): remove more outdated comments
reo101 Jul 14, 2025
88b37ed
chore(annotations): augment comment about dummy function definition
reo101 Jul 14, 2025
5491f9c
chore(annotations): remove old code for type-related tests in `parse.rs`
reo101 Jul 14, 2025
0d5016b
chore(annotations): clarify wanted behaviour of `nom`'s `ParserError`
reo101 Jul 14, 2025
92d43ad
chore(annotations): remove outdated comment about unit type
reo101 Jul 14, 2025
c151564
feat(fv_std): Support calling fv_std::old in annotations
Aristotelis2002 Aug 22, 2025
b39de5a
feat(fv_std): Support global consts
Aristotelis2002 Aug 22, 2025
4405e96
chore(errors): Exec function in Spec code error
Aristotelis2002 Aug 22, 2025
53ee451
chore(fv_std): Add TODO comment for paths
Aristotelis2002 Aug 22, 2025
2dc2db2
feat(annotations): Parser for structure access op
Aristotelis2002 Aug 25, 2025
5ac40d3
feat(annotations): Convert structure access to tuple access
Aristotelis2002 Aug 29, 2025
8aeb7dd
chore(fv): Expand unhandled case arms
Aristotelis2002 Sep 1, 2025
1c17fb3
feat(globals): Add support for pathed globals in annotations
Aristotelis2002 Sep 2, 2025
6f977a9
fix(globals): Allow access to fully imported globals
Aristotelis2002 Sep 10, 2025
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
77 changes: 77 additions & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

5 changes: 5 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,13 +1,16 @@
[workspace]

members = [
# FV crates
"compiler/fv_bridge",
# Compiler crates
"compiler/noirc_arena",
"compiler/noirc_evaluator",
"compiler/noirc_frontend",
"compiler/noirc_errors",
"compiler/noirc_driver",
"compiler/noirc_printable_type",
"compiler/formal_verification",
"compiler/fm",
"compiler/wasm",
# Crates related to tooling built on top of the Noir compiler
Expand Down Expand Up @@ -154,6 +157,8 @@ codespan-reporting = "0.11.1"

# Formal verification
vir = {git = "https://github.com/Aristotelis2002/verus-lib", branch = "synced_main"}
formal_verification = { path = "compiler/formal_verification"}
fv_bridge = { path = "compiler/fv_bridge" }

# Benchmarking
criterion = "^0.5.0"
Expand Down
37 changes: 37 additions & 0 deletions compiler/formal_verification/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
[package]
name = "formal_verification"
version.workspace = true
authors.workspace = true
edition.workspace = true
rust-version.workspace = true
license.workspace = true

[dependencies]
bn254_blackbox_solver.workspace = true
serde_json.workspace = true
serde.workspace = true
num-bigint.workspace = true
num-traits.workspace = true
noirc_errors.workspace = true
noirc_evaluator.workspace = true
noirc_frontend.workspace = true
vir.workspace = true
cfg-if.workspace = true
tracing.workspace = true
strum.workspace = true
strum_macros.workspace = true
nom = "8.0"
derive_more = { version = "2.0.1", features = ["deref", "from", "into", "debug"] }

[dev-dependencies]
base64.workspace = true
function_name = "0.3.0"
proptest.workspace = true
proptest-derive.workspace = true
insta.workspace = true

[features]
bn254 = []
bls12_381 = []
test_utils = []
nextest = []
Loading