A learned pass that drops a range check

A range check is the boring constraint. This field element is less than this bound. Without it, modular arithmetic will wrap, and a value that was supposed to be a balance or an index becomes whatever the field felt like.

People put range checks in by hand, then get tired of it, then ask a compiler to add them. Lately the compiler has a learned pass. Someone trained a model to rewrite circuits or to propose witness-generation shortcuts, because the hand-written pass was slow or missed cases.

The proof still verifies. That is the part that makes this easy to ship and hard to catch.

Verifying is not the property you wanted

A proof says: there exists a witness such that these constraints hold. If a pass deleted a constraint, the statement changed. The verifier is happy about a weaker claim. Your brief still talks about the stronger one.

The failure looks like this. The intended property was “amount fits in 64 bits.” The compiled artifact dropped that check on a path the cost function thought was redundant. The model had seen a lot of circuits where a later constraint implied the bound. In this circuit it did not. The implication was a statistical habit, not a proof.

You cannot see that from “the proof verifies.” You see it if you still have the intended properties written down, independent of the compiler. That is what the brief is for. If the only artifact you trust is the compiled circuit, you have no place to stand when a pass gets creative.

This is a join. The crypto side knows what a range check is for. The model side knows the pass can delete nodes that look unused. Neither fact is a finding by itself. The finding is that a learned rewrite is allowed to change the statement, and nothing after it diffs the statement against the brief.

What a learned pass actually optimizes

Cost. Time. Gate count. Witness size. Sometimes a score that means “looks like the training set.” None of those are “preserves the property the author wrote in a comment.”

A classical optimizer can drop a check too. We already review those, because the rewrite rules are code you can read. A model does not give you the rule. It gives you a new circuit and a shrug. Fine, if the next stage is an independent check that every property in the brief still has a constraint. Not fine if the next stage is “run the prover, green check, ship.”

I do not care whether the pass is advertised as an assistant or as the compiler. If it can delete a constraint, it is in the trusted computing base of the statement. Put it in the brief that way. Name the properties you still need after it runs. Say who diffs them. If nobody diffs them, write that down too. Then at least the report and the client are looking at the same gap.

Training-set leakage shows up here in a petty way. The model has seen a popular template. It “knows” that template always range-checks amount next to transfer. Your fork moved amount through an adapter. The pass deletes the check next to the adapter because the template did not have one there. Nobody is being clever. The model is completing a pattern.

What we ask for

The intended properties, in writing, before the compiler. The compiled constraints. A way to see a deleted range check without reading every gate by hand: a dump, a diff, an exported list of bounds. The model files and the pass that loads them, if that pass is how the circuit you will verify gets produced.

We will not grade the model on how often it is helpful. We will try to make it drop a check that the brief still claims exists. If we cannot, we say so, and we say what we tried. A clean note there is not a proof that the pass is safe. It is a record that this team, with this time, did not find a rewrite that silently weakened the statement.

If you change the pass after that, the record does not cover the new one. Continuous review is how we look at the next compiler drop. It is people who already know the properties, not a scanner login.

This sits on Joins and on Crypto. Our methodology. Request an audit.