[DRAFT] Non-Boolean conditional pass

.gitignore

@@ -1,3 +1,4 @@
 .vscode
 /target
 /examples
+.*.sw*

CHANGELOG.md

@@ -1,47 +1,57 @@
 # Release Notes
 
+## v0.8.0 (2023-01-10)
+
+### Features
+
+-   Added initial support for Circom 2.1.2, which includes tags, tuples, and
+    anonymous components.
+-   Added templates to the `bn128-specific-circuits` analysis pass.
+
+### Bug fixes
+
+-   Rewrote the `unconstrained-less-than` analysis pass to better capture the
+    underlying issue.
+-   Fixed an issue where the cyclomatic complexity calculation could underflow
+    in some cases in the `overly-complex-function-or-template` analysis pass.
 
 ## v0.7.2 (2022-12-01)
 
 ### Features
 
-  - Added a URL to the issue description for each output.
-
+-   Added a URL to the issue description for each output.
 
 ### Bug Fixes
 
-  - Rewrote description of the unconstrained less-than analysis pass, as the
+-   Rewrote description of the unconstrained less-than analysis pass, as the
     previous description was too broad.
-  - Fixed grammar in the under-constrained signal warning message.
-
+-   Fixed grammar in the under-constrained signal warning message.
 
 ## v0.7.0 (2022-11-29)
 
-
 ### Features
 
-  - New analysis pass (`unconstrained-less-than`) that detects uses of the
+-   New analysis pass (`unconstrained-less-than`) that detects uses of the
     Circomlib `LessThan` template where the input signals are not constrained
     to be less than the bit size passed to `LessThan`.
-  - New analysis pass (`unconstrained-division`) that detects signal assignments
+-   New analysis pass (`unconstrained-division`) that detects signal assignments
     containing division, where the divisor is not constrained to be non-zero.
-  - New analysis pass (`bn128-specific-circuits`) that detects uses of Circomlib
+-   New analysis pass (`bn128-specific-circuits`) that detects uses of Circomlib
     templates with hard-coded BN128-specific constants together with a custom curve like BLS12-381 or Goldilocks.
-  - New analysis pass (`under-constrained-signal`) that detects intermediate
+-   New analysis pass (`under-constrained-signal`) that detects intermediate
     signals which do not occur in at least two separate constraints.
-  - Rule name is now included in Sarif output. (The rule name is now also
+-   Rule name is now included in Sarif output. (The rule name is now also
     displayed by the VSCode Sarif extension.)
-  - Improved parsing error messages.
-
+-   Improved parsing error messages.
 
 ### Bug Fixes
 
-  - Fixed an issue during value propagation where values would be propagated to
+-   Fixed an issue during value propagation where values would be propagated to
     arrays by mistake.
-  - Fixed an issue in the `nonstrict-binary-conversion` analysis pass where
+-   Fixed an issue in the `nonstrict-binary-conversion` analysis pass where
     some instantiations of `Num2Bits` and `Bits2Num` would not be detected.
-  - Fixed an issue where the maximum degree of switch expressions were evaluated
+-   Fixed an issue where the maximum degree of switch expressions were evaluated
     incorrectly.
-  - Previous versions could take a very long time to complete value and degree
+-   Previous versions could take a very long time to complete value and degree
     propagation. These analyses are now time boxed and will exit if the analysis
     takes more than 10 seconds to complete.

Cargo.toml

@@ -4,5 +4,5 @@ members = [
   "parser",
   "program_analysis",
   "program_structure",
-  "program_structure_tests"
+  "program_structure_tests",
 ]

circom_algebra/Cargo.toml

@@ -1,7 +1,8 @@
 [package]
 name = "circomspect-circom-algebra"
-version = "2.0.1"
-edition = "2018"
+version = "2.0.2"
+edition = "2021"
+rust-version = "1.65"
 license = "LGPL-3.0-only"
 authors = ["hermeGarcia <hermegarcianavarro@gmail.com>"]
 description = "Support crate for the Circomspect static analyzer"

cli/Cargo.toml

@@ -1,23 +1,24 @@
 [package]
 name = "circomspect"
-version = "0.7.2"
+version = "0.8.0"
 edition = "2021"
+rust-version = "1.65"
 license = "LGPL-3.0-only"
 authors = ["Trail of Bits"]
 readme = "../README.md"
 description = "A static analyzer and linter for the Circom zero-knowledge DSL"
-repository = "https://github.com/trailofbits/circomspect"
 keywords = ["cryptography", "static-analysis", "zero-knowledge", "circom"]
+repository = "https://github.com/trailofbits/circomspect"
 
 [dependencies]
 anyhow = "1.0"
 atty = "0.2"
 # Stay on Clap version 3 until version 4 supports coloured help output.
 clap = { version = "3.2", features = ["derive"] }
 log = "0.4"
-parser = { package = "circomspect-parser", version = "2.0.11", path = "../parser" }
+parser = { package = "circomspect-parser", version = "2.1.2", path = "../parser" }
 pretty_env_logger = "0.4"
-program_analysis = { package = "circomspect-program-analysis", version = "0.7.1", path = "../program_analysis" }
-program_structure = { package = "circomspect-program-structure", version = "2.0.11", path = "../program_structure" }
+program_analysis = { package = "circomspect-program-analysis", version = "0.8.0", path = "../program_analysis" }
+program_structure = { package = "circomspect-program-structure", version = "2.1.2", path = "../program_structure" }
 serde_json = "1.0"
 termcolor = "1.1"

cli/src/main.rs

@@ -1,11 +1,9 @@
-mod config;
-mod analysis_runner;
-
 use std::path::PathBuf;
 use std::process::ExitCode;
-use clap::{CommandFactory, Parser};
+use clap::{ArgAction, CommandFactory, Parser};
 
-use analysis_runner::AnalysisRunner;
+use program_analysis::config;
+use program_analysis::analysis_runner::AnalysisRunner;
 
 use program_structure::constants::Curve;
 use program_structure::report::Report;
@@ -19,6 +17,10 @@ struct Cli {
     #[clap(name = "INPUT")]
     input_files: Vec<PathBuf>,
 
+    /// Analyze included files recursively
+    #[clap(short = 'i', long = "follow-includes", action = ArgAction::SetTrue)]
+    follow_includes: bool,
+
     /// Output level (INFO, WARNING, or ERROR)
     #[clap(short = 'l', long = "level", name = "LEVEL", default_value = config::DEFAULT_LEVEL)]
     output_level: MessageCategory,
@@ -67,8 +69,11 @@ fn main() -> ExitCode {
     let mut stdout_writer = CachedStdoutWriter::new(options.verbose)
         .add_filter(move |report: &Report| filter_by_id(report, &allow_list))
         .add_filter(move |report: &Report| filter_by_level(report, &options.output_level));
-    let mut runner = AnalysisRunner::new(&options.curve);
-    runner.with_files(&options.input_files, &mut stdout_writer);
+    let mut runner = AnalysisRunner::new(options.curve).with_files(
+        &options.input_files,
+        options.follow_includes,
+        &mut stdout_writer,
+    );
 
     runner.analyze_functions(&mut stdout_writer);
     runner.analyze_templates(&mut stdout_writer);

doc/analysis_passes.md

@@ -36,7 +36,6 @@ An assigned value which does not contribute either directly or indirectly to a c
 
 Here, `lout` no longer influences the generated circuit, which is detected by Circomspect.
 
-
 ### Shadowing variable
 
 A shadowing variable declaration is a declaration of a variable with the same name as a previously declared variable. This does not have to be a problem, but if a variable declared in an outer scope is shadowed by mistake, this could change the semantics of the program which would be an issue.
@@ -57,7 +56,6 @@ For example, consider this function which is supposed to compute the number of b
 
 Since a new variable `r` is declared in the while-statement body, the outer variable is never updated and the return value is always 0.
 
-
 ### Signal assignment
 
 Signals should typically be assigned using the constraint assignment operator `<==`. This ensures that the circuit and witness generation stay in sync. If `<--` is used it is up to the developer to ensure that the signal is properly constrained. Circomspect will try to detect if the right-hand side of the assignment is a quadratic expression. If it is, the signal assignment can be rewritten using the constraint assignment operator `<==`.
@@ -66,17 +64,14 @@ However, sometimes it is not possible to express the assignment using a quadrati
 
 The Tornado Cash codebase was originally affected by an issue of this type. For details see the Tornado Cash disclosure [here](https://tornado-cash.medium.com/tornado-cash-got-hacked-by-us-b1e012a3c9a8).
 
-
 ### Under-constrained signal
 
 Under-constrained signals are one of the most common issues in zero-knowledge circuits. Circomspect will flag intermediate signals that only occur in a single constraint. Since intermediate signals are not available outside the template, this typically indicates an issue with the implementation.
 
-
 ### Constant branching condition
 
 If a branching statement condition always evaluates to either `true` or `false`, this means that the branch is either always taken, or never taken. This typically indicates a mistake in the code which should be fixed.
 
-
 ### Non-strict binary conversion
 
 Using `Num2Bits` and `Bits2Num` from
@@ -88,44 +83,34 @@ uniquely determined by the input.
 
 For example, suppose that we create a component `n2b` given by `Num2Bits(254)` and set the input to `1`. Now, both the binary representation of `1` _and_ the representation of `p + 1` (where `p` is the order of the underlying finite field) will satisfy the circuit over BN128, since both are 254-bit numbers. If you cannot restrict the input size below the prime size you should use the strict versions `Num2Bits_strict` and `Bits2Num_strict` to convert to and from binary representation. Circomspect will generate a warning if it cannot prove (using constant propagation) that the input size passed to `Num2Bits` or `Bits2Num` is less than the size of the prime in bits.
 
-
 ### Unconstrained less-than
 
-The Circomlib `LessThan` template takes an input size as argument. If the individual input signals are not constrained to the input size (for example using the Circomlib `Num2Bits` circuit), it is possible to find inputs `a` and `b` such that `a > b`, but `LessThan` still evaluates to true when given `a` and `b` as inputs.
+The Circomlib `LessThan` template takes an input size as argument. If the individual input signals are not constrained to be non-negative (for example using the Circomlib `Num2Bits` circuit), it is possible to find inputs `a` and `b` such that `a > b`, but `LessThan` still evaluates to true when given `a` and `b` as inputs.
 
 For example, consider the following template which takes a single input signal
 and attempts to constrain it to be less than two.
 
 ```cpp
   template LessThanTwo() {
     signal input in;
-    signal output out;
 
     component lt = LessThan(8);
     lt.in[0] <== in;
     lt.in[1] <== 2;
 
-    out <== lt.out;
+    lt.out === 1;
   }
 ```
 
-Suppose that we define the private input `in` as `p - 254`, where `p` is the prime order of the field. This would result in the constraints
-
-```cpp
-    lt.in[0] <== p - 254;
-    lt.in[1] <== 2;
-```
-
-Since `p` is at least 64 bits, `p - 254` is not less than two (at least not when viewed as an unsigned integer), so we would perhaps expect `LessThanTwo` to return zero here. However, looking at [the implementation](https://github.com/iden3/circomlib/blob/cff5ab6288b55ef23602221694a6a38a0239dcc0/circuits/comparators.circom#L89-L99) of `LessThan`, we see that `lt.out` is given by
+Suppose that we define the private input `in` as `p - 254`, where `p` is the prime order of the field. Clearly, `p - 254` is not less than two (at least not when viewed as an unsigned integer), so we would perhaps expect `LessThanTwo` to fail. However, looking at [the implementation](https://github.com/iden3/circomlib/blob/cff5ab6288b55ef23602221694a6a38a0239dcc0/circuits/comparators.circom#L89-L99) of `LessThan`, we see that `lt.out` is given by
 
 ```cpp
-    1 - n2b.out[8] = 1 - (bit 8 of (p - 254) + 256 - 2) = 1 - 0 = 1.
+    1 - n2b.out[8] = 1 - bit 8 of (p - 254 + (1 << 8) - 2) = 1 - 0 = 1.
 ```
 
-It follows that `p - 254` satisfies `LessThanTwo()`, which is perhaps not what we expected. Note that, `p - 254` is equal to -254 which _is_ less than two, so there is nothing wrong with the Circomlib `LessThan` circuit. This may just be unexpected behavior if we're thinking of field elements as unsigned integers.
-
-Circomspect will check if the inputs to `LessThan` are constrained to the input size using `Num2Bits`. If it cannot prove that both inputs are constrained in this way, a warning is generated.
+It follows that `p - 254` satisfies `LessThanTwo()`, which is probably not what we expected. Note that, `p - 254` is equal to -254 which _is_ less than two, so there is nothing wrong with the Circomlib `LessThan` circuit. This may just be unexpected behavior if we're thinking of field elements as unsigned integers.
 
+Circomspect will check if the inputs to `LessThan` are constrained to be strictly less than `log(p) - 1` bits using `Num2Bits`. This guarantees that both inputs are non-negative, which avoids this issue. If it cannot prove that both inputs are constrained in this way, a warning is generated.
 
 ### Unconstrained division
 
@@ -140,46 +125,55 @@ This forces `c` to be equal to `a / b` during witness generation, and checks tha
 
 Circomspect will identify signal assignments on the form `c <-- a / b` and ensure that the expression `b` is constrained to be non-zero using the Circomlib `IsZero` template. If no such constraint is found, a warning is emitted.
 
-
 ### BN128 specific circuit
 
 Circom defaults to using the BN128 scalar field (a 254-bit prime field),
 but it also supports BSL12-381 (which has a 255-bit scalar field) and
 Goldilocks (with a 64-bit scalar field). However, since there are no constants denoting either the prime or the prime size in bits available in the Circom language, some Circomlib templates like `Sign` (which returns the sign of the input signal), and `AliasCheck` (used by the strict versions of `Num2Bits` and `Bits2Num`), hardcode either the BN128 prime size or some other constant related to BN128. Using these circuits with a custom prime may thus lead to unexpected results and should be avoided.
 
-Circomlib templates that may be problematic when used together with curves other than BN128 include the following circuit definitions.
-
-  | Template                  | Circomlib Source File            |
-  | ------------------------- | -------------------------------- |
-  | `Sign`                    | circuits/sign.circom             |
-  | `AliasCheck`              | circuits/aliascheck.circom       |
-  | `CompConstant`            | circuits/compconstant.circom     |
-  | `Num2Bits_strict`         | circuits/bitify.circom           |
-  | `Bits2Num_strict`         | circuits/bitify.circom           |
-  | `Bits2Point_Strict`       | circuits/bitify.circom           |
-  | `Point2Bits_Strict`       | circuits/bitify.circom           |
-  | `SMTVerifier`             | circuits/smt/smtverifier.circom  |
-  | `SMTProcessor`            | circuits/smt/smtprocessor.circom |
-  | `EdDSAVerifier`           | circuits/eddsa.circom            |
-  | `EdDSAPoseidonVerifier`   | circuits/eddsaposeidon.circom    |
-  | `EdDSAMiMCSpongeVerifier` | circuits/eddsamimcsponge.circom  |
-
+Circomlib templates that may be problematic when used together with curves other than BN128 include the following circuit definitions. (An `x` means that the template should not be used together with the corresponding curve.)
+
+| Template                  | Goldilocks (64 bits) | BLS12-381 (255 bits) |
+| :------------------------ | :------------------: | :------------------: |
+| `AliasCheck`              |           x          |           x          |
+| `BabyPbk`                 |           x          |                      |
+| `Bits2Num_strict`         |           x          |           x          |
+| `Num2Bits_strict`         |           x          |           x          |
+| `CompConstant`            |           x          |           x          |
+| `EdDSAVerifier`           |           x          |           x          |
+| `EdDSAMiMCVerifier`       |           x          |           x          |
+| `EdDSAMiMCSpongeVerifier` |           x          |           x          |
+| `EdDSAPoseidonVerifier`   |           x          |           x          |
+| `EscalarMulAny`           |           x          |                      |
+| `MiMC7`                   |           x          |                      |
+| `MultiMiMC7`              |           x          |                      |
+| `MiMCFeistel`             |           x          |                      |
+| `MiMCSponge`              |           x          |                      |
+| `Pedersen`                |           x          |                      |
+| `Bits2Point_strict`       |           x          |           x          |
+| `Point2Bits_strict`       |           x          |           x          |
+| `PoseidonEx`              |           x          |                      |
+| `Poseidon`                |           x          |                      |
+| `Sign`                    |           x          |           x          |
+| `SMTHash1`                |           x          |                      |
+| `SMTHash2`                |           x          |                      |
+| `SMTProcessor`            |           x          |           x          |
+| `SMTProcessorLevel`       |           x          |                      |
+| `SMTVerifier`             |           x          |           x          |
+| `SMTVerifierLevel`        |           x          |                      |
 
 ### Overly complex function or template
 
 As functions and templates grow in complexity they become more difficult to review and maintain. This typically indicates that the code should be refactored into smaller, more easily understandable, components. Circomspect uses cyclomatic complexity to estimate the complexity of each function and template, and will generate a warning if the code is considered too complex. Circomspect will also generate a warning if a function or template takes too many arguments, as this also impacts the readability of the code.
 
-
 ### Bitwise complement
 
 Circom supports taking the 256-bit complement `~x` of a field element `x`. Since the result is reduced modulo `p`, it will typically not satisfy the expected relations `(~x)ᵢ == ~(xᵢ)` for each bit `i`, which could lead to surprising results.
 
-
 ### Field element arithmetic
 
 Circom supports a large number of arithmetic expressions. Since arithmetic expressions can overflow or underflow in Circom it is worth paying extra attention to field arithmetic to ensure that elements are constrained to the correct range.
 
-
 ### Field element comparison
 
 Field elements are normalized to the interval `(-p/2, p/2]` before they are compared, by first reducing them modulo `p` and then mapping them to the correct interval by subtracting `p` from the value `x`, if `x` is greater than `p/2`. In particular, this means that `p/2 + 1 < 0 < p/2 - 1`. This can be surprising if you are used to thinking of elements in `GF(p)` as unsigned integers.