Add assume/prove/try_prove operation

[meheff]

The operation might have the following semantics:

Asserts that a relation (e.g, unsigned less than) between the data operand and a literal value is true. Analogous to the assert operation, a run time error is raised if the assumption is false. The assume operation evaluates to a tuple which includes the data operand value itself on which the optimizer may assume the relation holds.

Mnemonic

result = assume_eq(tkn, operand, value=<literal>)
result = assume_ne(tkn, operand, value=<literal>)
result = assume_ult(tkn, operand, value=<literal>)
result = assume_ule(tkn, operand, value=<literal>)

The assume operation constrains the legal range of a value in the program. Most obviously, this would inform range analysis which computes the possible ranges of every value in the program. These ranges can be used in optimizations such as narrowing the bit-width of the value or statically evaluating conditional operations.

By design, the form of the assume operation simplifies the analysis required to take advantage of the assumed constraint. Conceivably, an assert operation might be constructed which equivalently expresses the constraint of the assume operation. However, the analysis is more complex and less robust in the face of optimizations.

[meheff]

Below is a related internal discussion about a "prove" op which behaves like an assume but requires that the compiler itself prove the condition. This can be used to verify the programmers assumption as well as provide a specific target for aggressive analysis such as using a sat solver.

Assuming I understand things correctly this might be implemented in the compiler as a new op called "prove". A "prove" op takes some condition and raises an error if that condition can't be proven to be true for some definition of "proven". One heavy-weight approach would be to use a sat solver to verify that the condition is true. Another is to check at the end of the pipeline whether the condition was replaced with a literal one as the optimizer will replace known values with literals. The sat-solver approach is a stronger check on whether your condition is actually true (and strongly verifies your assumption about your code behavior), but doesn't say much about what the compiler itself actually knows about your code. The second approach will do a better job of verifying the compiler;s knowledge but may be a bit flakier because the compiler analyses are generally not as a strong as a sat-solver. I suppose one combined approach is to use a sat-solver to prove the statement then (if proven) automatically add an "assume" statement so the optimization pipeline can take advantage of it. This does insert a sat-solver into the compilation pipeline (which can be slow) but does so in a limited way.

[cdleary]

One of the notable challenges with a try_prove annotation would be that there is some amount of "flakiness" that can result from proof attempts to bounded amounts of time on different machines; e.g. try_prove(p, timeout=10_000) kind of thing might mean we get 10 seconds of attempted proof time for a given predicate on whatever machine. Also you're sensitive to how many times these things get instantiated in various caller contexts if they're parametric. We probably need to noodle a bit how best to expose these in the build/test system, given that a search for counterexamples is not supposed to turn up results in the typical case and may need to time out in the general cases where the proof can't close. Feels more in the bucket similar to "continuous fuzzing" to run those, in a sense.

[taktoa]

@cdleary Z3 can be given a resource limit (roughly speaking # of memory allocations), rather than a time limit, which makes it deterministic, so that flakiness wouldn't exist, except insofar as compiler optimizations or different architectures change the validity of the resource limit. Alternatively, you can use a solver like CVC4, which I believe is deterministic (including resource bounds) by default.

[cdleary]

That is cool, hadn't realized that. Maybe a few different considerations we can peel apart here:

• If you build z3 at a different rev you might get different proof strategies (e.g. if you want to think about it as "consistency in proof capability across source updates" or other perhaps "seemingly innocuous" changes from a user perspective)
• If you have libraries that can cause proofs to be created on a per-instantiation basis, you can get an explosion in proof requests in your code base
• You may want to run the prover on different "seeds" / strategies just to see if it converges or finds a counterexample quickly in some mode -- from what I understand talking to some local experts it sounds like this is actually often how to find an effective strategy in practice for your problem, try a bunch and see what went better

To me that adds up to feeling like it's more akin to continuous fuzzing than a concrete unit test (i.e. something you could effectively rely on to not time out your build/test environment on e.g. a dependency upgrade).

Just wanted to jot that down I we could remember what we chatted about.

[cdleary]

We had some discussion about how best to support proofs in the build/test system. I think if the proofs are noted to be something like psan_prove!(predicate) in the DSLX code and we have a separate config (i.e. called PSAN) that enables targets that run extra long proofs that aren't as suitable for unit test time frames (e.g. inside Google we'd not expect them to run/complete on TAP as part of CI because we try to confine those to be ~5 mins) that'd be a reasonable way to go.

[proppy]

could this potentially also emit SystemVerilog formal verification primitives/constraints? https://www.systemverilog.io/verification/gentle-introduction-to-formal-verification/ https://www.chipverify.com/systemverilog/systemverilog-constraints