Ary Borenszweig asterite

Review: noir-lang/noir#13787 — feat(fv): machine-checked proofs that Noir's integer circuits are not underconstrained

AztecBot · cb/acir-lean-gadget-proofs → master · head 7c47f02 · 62 files, +25379 −1 · OPEN, REVIEW_REQUIRED · CI 137 passing, 0 failing, 2 skipped · behind base by 31 commits · Linear: none Reviewed 2026-09-30.

At a glance

This PR adds no compiler behavior change — only a new, CI-gated Lean proof that specific ACIR circuits are sound, plus the Rust/script glue that pins Lean's model to the real compiler.

	use aztec::macros::aztec;

	pub contract EcdsaKAccount {
	use authwit::{
	account::AccountActions,
	auth_witness::get_auth_witness,
	entrypoint::{app::AppPayload, fee::FeePayload},
	};
	use aztec::{
	context::private_context::PrivateContext,

	use rand::{Rng, SeedableRng};
	use rand_xorshift::XorShiftRng;

	pub struct Config<T, const N: usize> {
	pub options_with_weights: [(T, usize); N],
	pub total_weight: usize,
	}

	impl<T: Copy, const N: usize> Config<T, N> {
	pub const fn new(options_with_weights: [(T, usize); N]) -> Self {

	def affected_files(file, dependencies)
	tracked_files = Set(String).new
	track(file, dependencies, tracked_files)
	tracked_files
	end

	def track(file, dependencies, tracked_files)
	return unless tracked_files.add?(file)

	dependencies[file].each do \|to\|

	# Make sure to configure this script!
	# 1. Change `TEAM_LINEAR` properties below to match your Linear team
	# 2. Optionally add more teams
	# 3. Change the value of `DEPLOYED_TO_STAGING_GIT_TAG` to the tag/branch you use for deploys to staging
	# 4. Change the value of `DEPLOYED_TO_PRODUCTION_GIT_TAG` to the tag/branch you use for deploys to production
	#
	# Usage:
	# LINEAR_API_KEY=... GITHUB_API_KEY=... ruby move_deployed_linear_issues.rb
	#
	# Adding new teams (change "LinearTeam" to your team name):

	require "benchmark"

	module Parser(T)
	def self.char(a : Char)
	CharParser.new(a)
	end

	def self.int
	IntParser.new
	end

	time = Time.monotonic
	gcfile = File.new("chry_multiplied.fa")

	at = 0
	gc = 0

	while true
	# Peek the IO's buffer
	peek = gcfile.peek

	require "benchmark"

	RANGE = 3..7

	a = 1
	v = ARGV[0].to_i

	Benchmark.ips do \|x\|
	x.report("constant") do
	case v

	# This Crystal source file is a multiple threaded implementation to perform an
	# extremely fast Segmented Sieve of Zakiya (SSoZ) to find Twin Primes <= N.

	# Inputs are single values N, or ranges N1 and N2, of 64-bits, 0 -- 2^64 - 1.
	# Output is the number of twin primes <= N, or in range N1 to N2; the last
	# twin prime value for the range; and the total time of execution.

	# This code was developed on a System76 laptop with an Intel I7 6700HQ cpu,
	# 2.6-3.5 GHz clock, with 8 threads, and 16GB of memory. Parameter tuning
	# probably needed to optimize for other hardware systems (ARM, PowerPC, etc).

	require "colorize"

	enum Color
	Red
	Green
	Blue
	Yellow
	Pink
	Gray