chore(docs): Updated docs

formal_verification_docs/src/SUMMARY.md

@@ -1,16 +1,17 @@
 # Summary
 
 - [Blocksense Noir](./blocksense_noir.md)
-- [Noir Formal Verification](./noir_formal_verification/README.md)
-  - [Getting Started](./noir_formal_verification/getting_started.md)
-  - [Specifications](./noir_formal_verification/specifications/README.md)
-    - [Pre- and Postconditions](./noir_formal_verification/specifications/pre_and_postconditions.md)
-    - [Quantifiers](./noir_formal_verification/specifications/quantifiers.md)
-    - [Ghost Functions](./noir_formal_verification/specifications/ghost_functions.md)
-    - [Recursion and Loops](./noir_formal_verification/specifications/recursion_and_loops.md)
-  - [Additional Features](./noir_formal_verification/additional_features.md)
-  - [Specification Syntax](./noir_formal_verification/specification_syntax.md)
-  - [Limitations](./noir_formal_verification/limitations.md)
+- [Verno](./verno/README.md)
+  - [Getting Started](./verno/getting_started.md)
+  - [Specifications](./verno/specifications/README.md)
+    - [Pre- and Postconditions](./verno/specifications/pre_and_postconditions.md)
+    - [Quantifiers](./verno/specifications/quantifiers.md)
+    - [Ghost Functions](./verno/specifications/ghost_functions.md)
+    - [Recursion and Loops](./verno/specifications/recursion_and_loops.md)
+  - [Additional Features](./verno/additional_features.md)
+  - [Unconstrained Noir Support](./verno/unconstrained_support.md)
+  - [Specification Syntax](./verno/specification_syntax.md)
+  - [Limitations](./verno/limitations.md)
 - [Noir PLONKY2 Backend](./noir_plonky2_backend/README.md)
   - [Getting Started](./noir_plonky2_backend/getting_started.md)
 - [Noir Tracer](./noir_tracer/README.md)

formal_verification_docs/src/blocksense_noir.md

@@ -4,7 +4,7 @@ At Blocksense, we’ve enhanced the Noir programming language and compiler with
 
   1. [Noir time-travel debugging](./noir_tracer) in the [CodeTracer](https://github.com/metacraft-labs/codetracer) environment;
 
-  2. [formal verification](./noir_formal_verification) of Noir circuits, based on the Z3 SMT solver and the IR language of the [Verus project](https://github.com/verus-lang/verus); and
+  2. [Formal verification](./verno) of Noir circuits, based on the Z3 SMT solver and the IR language of the [Verus project](https://github.com/verus-lang/verus); and
 
   3. [Noir compilation support](./noir_plonky2_backend) for the PLONKY2 proof system.
 

formal_verification_docs/src/unconstrained_support.md

@@ -0,0 +1 @@
+# Unconstrained Noir Support

formal_verification_docs/src/noir_formal_verification/README.md → formal_verification_docs/src/verno/README.md

@@ -1,16 +1,15 @@
-# Noir FV overview
+# Verno Overview
 
-We at Blocksense have created a tool for verifying the correctness of code written in Noir. Building upon Microsoft's open-source verification framework Verus, we're able to prove functional correctness of constrained code, before it is ever ran! Noir FV introduces no run-time checks, but instead uses computer-aided theorem proving to statically verify that executable code will always satisfy some user-provided specifications for all possible inputs.  
-
-Constrained Noir is not [Turing-complete](https://en.wikipedia.org/wiki/Turing_completeness) which simplifies proof writing. Noir’s deterministic nature eliminates the need for complex clauses which appear in other formal verification systems (like [invariants](https://viperproject.github.io/prusti-dev/user-guide/tour/loop_invariants.html?#loop-invariants) and [decrease clauses](https://verus-lang.github.io/verus/guide/reference-decreases.html?#the-decreases-measure)). Alongside the absence of a heap, we see Noir as a strong candidate for formal verification.
+Verno is a tool for verifying the correctness of code written in Noir, built by Metacraft-labs. Building upon Microsoft's open-source verification framework Verus, we're able to prove functional correctness of constrained code, before it is ever run. Verno introduces no run-time checks, but instead uses computer-aided theorem proving to statically verify that executable code will always satisfy some user-provided specifications for all possible inputs.
 
+Constrained Noir is not [Turing-complete](https://en.wikipedia.org/wiki/Turing_completeness) which simplifies proof writing. Many loops verify automatically thanks to determinism and fixed bounds, yet Verno also supports richer constructs—such as [loop invariants](https://viperproject.github.io/prusti-dev/user-guide/tour/loop_invariants.html?#loop-invariants) and [decrease clauses](https://verus-lang.github.io/verus/guide/reference-decreases.html?#the-decreases-measure)—when the program logic requires them. Alongside the absence of a heap, we see Noir as a strong candidate for formal verification.
 
 # This guide
 
-Noir FV reuses Noir's syntax and type system to express specifications for executable code. Basic proficiency with the language is assumed by this guide. Noir's documentation can be found [here](https://noir-lang.org/docs).
+Verno reuses Noir's syntax and type system to express specifications for executable code. Basic proficiency with the language is assumed by this guide. Noir's documentation can be found [here](https://noir-lang.org/docs).
 
-Code specification needs to be written according to a number of predetermined rules, using clauses like `forall` and `requires`. Of course, you'll also need to grasp and conform to the required rigor for creating, what is effectively, a mathematical proof. It can be challenging to prove that a Noir function satisfies its postconditions (its ensures clauses) or that a call to a function satisfies the function’s preconditions (its requires clauses). 
+Code specification needs to be written according to a number of predetermined rules, using clauses like `forall` and `requires`. Of course, you'll also need to grasp and conform to the required rigor for creating, what is effectively, a mathematical proof. It can be challenging to prove that a Noir function satisfies its postconditions (its ensures clauses) or that a call to a function satisfies the function’s preconditions (its requires clauses).
 
 Therefore, this guide’s tutorial will walk you through the various concepts and techniques, starting with relatively simple concepts (e.g., basic properties about integers), progressing to moderately difficult challenges, and eventually covering advanced topics like proofs about arrays using `forall` and `exists`.
 
-All of these proofs are supported by an automated theorem prover (specifically, Z3, a satisfiability-modulo-theories solver, or “SMT solver” for short). The SMT solver will often be able to prove simple properties, such as basic properties about booleans or integer arithmetic, with no additional help from the programmer. However, more complex proofs often require effort from both the programmer and the SMT solver. Therefore, this guide will also help you understand the strengths and limitations of SMT solving, and give advice on how to fill in the parts of proofs that SMT solvers cannot handle automatically.
+All of these proofs are supported by an automated theorem prover (specifically, Z3, a satisfiability-modulo-theories solver, or “SMT solver” for short). The SMT solver will often be able to prove simple properties, such as basic properties about booleans or integer arithmetic, with no additional help from the programmer. However, more complex proofs often require effort from both the programmer and the SMT solver. Therefore, this guide will also help you understand the strengths and limitations of SMT solving, and give advice on how to fill in the parts of proofs that SMT solvers cannot handle automatically.