feat: add initial proof logging infrastructure

[Dekker1]

An attempted update of #216, with support for outputting proofs in DRCP format.

[codecov]

Codecov Report

❌ Patch coverage is 80.62016% with 150 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/huub-cli/src/proof.rs	76.88%	48 Missing and 59 partials ⚠️
crates/huub/src/solver/engine.rs	77.50%	18 Missing ⚠️
crates/huub-cli/src/cli.rs	94.50%	2 Missing and 3 partials ⚠️
crates/huub-cli/src/lib.rs	68.75%	3 Missing and 2 partials ⚠️
crates/huub/src/solver/solving_context.rs	75.00%	4 Missing and 1 partial ⚠️
crates/huub/src/solver.rs	85.71%	4 Missing ⚠️
crates/huub/src/lower.rs	86.95%	3 Missing ⚠️
crates/huub/src/solver/proof.rs	77.77%	2 Missing ⚠️
crates/huub/src/model/deserialize/flatzinc.rs	94.73%	1 Missing ⚠️

Files with missing lines	Coverage Δ
crates/huub-cli/src/trace.rs	63.89% <100.00%> (+37.05%)	⬆️
crates/huub/src/model.rs	82.83% <100.00%> (+0.33%)	⬆️
crates/huub/src/model/deserialize/flatzinc.rs	60.70% <94.73%> (+3.27%)	⬆️
crates/huub/src/solver/proof.rs	77.77% <77.77%> (ø)
crates/huub/src/lower.rs	73.84% <86.95%> (+1.04%)	⬆️
crates/huub/src/solver.rs	74.89% <85.71%> (+2.14%)	⬆️
crates/huub-cli/src/cli.rs	88.25% <94.50%> (+2.20%)	⬆️
crates/huub-cli/src/lib.rs	62.77% <68.75%> (+0.64%)	⬆️
crates/huub/src/solver/solving_context.rs	83.37% <75.00%> (+0.09%)	⬆️
crates/huub/src/solver/engine.rs	86.95% <77.50%> (-1.11%)	⬇️
... and 1 more

... and 1 file with indirect coverage changes

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[codspeed-hq]

Merging this PR will not alter performance

✅ 21 untouched benchmarks

---

_{Comparing Dekker1:feat/proof_logging (481580d) with develop (5d29843)}

[mmcilree]

This is looking great! I don't know exactly what the status of the DRCP checker is, but from the VeriPB side, the proofs can now be checked with the latest version from https://gitlab.com/MIAOresearch/software/VeriPB.

• At the moment, as a quirk of the way we've set this up, it requires an empty .opb file. Either we can just advise creating this manually, or huub can create one when the VeriPB format is used. Or I could propose a change to VeriPB to allow an empty formula to be implicit when only one file is given.

I have tested this locally and almost all of the proofs produced from crates/huub-cli/corpus pass the checker already. There's only a couple of further fixes needed, which I made a quick PR for Dekker1#5 .

1. For add_assumption_clause, CaDiCaL returns a clause representing the negation of the assumption literals it used. Therefore, I think we should add a conjunction in the proof for this. We might need to think some more going forward about how assumptions should be hinted (it looks like the flatzinc uses a special huub_assumption constraint?) In any case, we shouldn't output a pol derivation with empty antecedent chain, as this is not valid syntax.
2. If the solver terminates because it found the FlatZinc was UNSAT after reformulation, it should conclude the proof at that point too.

With these two fixes, all but two of the corpus proofs pass. The two that fail are due to the proofs being essentially empty, because Huub was able to detect contradiction without any search at all. This is related to the problem we discussed last year of needing to log root-level propagations in addition to the clauses traced by the SAT engine.

I think it's in a state where it could be merged (with some disclaimers in the docs) and then it can be built on top of. There are various suggestions I would have for later versions that wouldn't necessary need to be included in an "initial proof logging infrastructure". I'll note these shortly.

[mmcilree]

In terms of questions you asked:

all literals are just named according to their internal numbering, should these not be mapped back to the FlatZinc names somehow?

Yes, but this isn't strictly necessary for a bare assertion proof to pass. For the (in progress) justifier tool, I do need some kind of literal -> atomic constraint mapping. The .lits file produced for DRCP would work, or I think I had a lits.json being produced before? Alternatively, for the Glasgow solver we have standardised a VeriPB-CP-literal naming convention, which we could use instead directly in the proof. This would eliminate the need for literal mapping names entirely as the justifier could parse the meanings directly from the names.

In that sense, I would appreciate it if you could explain a workflow (or command) I could use to check the proofs, we now generate.

For now, from the latest VeriPB version, (after cargo install veripb)

touch empty.opb
veripb empty.opb huub_proof.pbp

should work (with an s UNDER ASSERTIONS). I'll keep you posted on the progress of the justifier
I'm afraid I'm not as familiar with the DRCP checker usage, but I can look into this as well. I might also try supporting a DRCP frontend for my tool.

Can you confirm that our plan was to add the constraint reference of the constraint that allowed the unification to each constraint that uses either of the unified decisions?

This was the plan. I think I have two alternative way to deal with unification however. Might need to progress further with the Justifier implementation before I can say what I'd recommend. But potentially we do either/both of:

• Model-level views (including unifications) are written into the literal mapping file as auxiliary information for the justifier
• We have a special trace event create_view that writes a VeriPB meta rule command into the proof and the justifier can expand this.

Both of these have the advantage of supporting derivable views as well as unifications, and avoids adding antecedent dependencies to every constrant that contains unified variables.

[Dekker1]

Thanks for the fixes. I've included them in the branch.

At the moment, as a quirk of the way we've set this up, it requires an empty .opb file. Either we can just advise creating this manually, or huub can create one when the VeriPB format is used. Or I could propose a change to VeriPB to allow an empty formula to be implicit when only one file is given.

Okay, I think that is okay for now. In my understanding, the justifier would in the end be a surrounding (leading) executable would make this unnecessary.

Yes, but this isn't strictly necessary for a bare assertion proof to pass. For the (in progress) justifier tool, I do need some kind of literal -> atomic constraint mapping. The .lits file produced for DRCP would work, or I think I had a lits.json being produced before? Alternatively, for the Glasgow solver we have standardised a VeriPB-CP-literal naming convention, which we could use instead directly in the proof. This would eliminate the need for literal mapping names entirely as the justifier could parse the meanings directly from the names.

This seems like it would be nice to resolve before we merge the branch. Writing out a literal mapping seems very straightforward, so we could do that, but if the "VeriPB-CP-literal naming convention" would make things work better, then I would be happy to implement that. (You just have to let me know where I can find the specification).

I've been thinking about changing the DRCP proofs to do the inline atomic constraints as well. It seems it would make things much more readable, but currently there is still a slight issue with the order in which some information gets to the tracer.

This is related to the problem we discussed last year of needing to log root-level propagations in addition to the clauses traced by the SAT engine.

Yes, this would certainly be something to tackle. I think the code infrastructure is now much better able to potentially handle this, but I think it might be wise to leave this for a next stage.

Both of these have the advantage of supporting derivable views as well as unifications, and avoids adding antecedent dependencies to every constrant that contains unified variables.

I think the alternatives sound much closer to what I was hoping for when we initially talked about this issue. They certainly seem to take some burden away from the logger. For now, I might just leave this in your (more capable) hands for now, and we can ship a solution in a next version.

[mmcilree]

In terms of naming conventions, we have gone for the following in the Glasgow Solver:

CP Literal/Atomic Constraint	Corresponding PB Literal
<name> >= <val>	i[<name>][geq<val>]
<name> < <val>	~i[<name>][geq<val>]
<name> == <val>	i[<name>][eq<val>]
<name> != <val>	~i[<name>][eq<val>]

The "i" is for "integer variable". The square bracketed names maybe seem a bit verbose, but we found it was what worked best for validating/parsing names in the formally verified PB encoding.
Potentially, if Huub can support both rich names and an external .lits file for both DRCP and VeriPB, then a --proof-name-mapping option or something similar to toggle this might make sense?

On the subject of args: these are more just taste things so feel free to ignore, but may as well note:

• --prove is what the Glasgow CP and Subgraph solvers have as the "enable proof logging" option. I think I mildly prefer this for a no-arg flag as it's a verb and doesn't imply that a proof somehow needs to be provided.
• For --proof-output, for me, the more intuitive default would be for the proof to appear in the current working directory (with name derived from the input file) rather than the same location as the input file. Since e.g. if I run --proof with no further arguments on something in huub-cli/crates/corpus it seems a bit unintuitive for the proof to appear in that directory.
• Additionally, it might be handy to detect if --proof-output is passed a directory, and if so, create the proof file with the default name in that directory, rather than erroring.
• Finally, I would argue --proof-type should be --proof-format. DRCP and VeriPB-with-hinted-assertions effectively only differ in syntax: the semantic content is the same proof. We might want to reserve --proof-type for some more drastic differences we could have in future e.g. whether nogoods are derived via resolution or RUP/RCP; or whether inferences are logged lazily or not.

[Dekker1]

I've also updated the design to output an .lits.json with the VeriPB proof. It currently has the following format:

{
  "x1": { "name": "X_INTRODUCED_4_" },
  "x2": { "name": "X_INTRODUCED_0_", "cmp": "<=", "val": 3 },
  "x3": { "name": "X_INTRODUCED_5_" },
  ...
}

If there was something more specific that you were thinking, then let me know. I couldn't find the previous JSON literal output that you mentioned.

For the flags, I did find that there was a big problem with the output path when using the default path, at least when using Huub through MiniZinc. Normally, MiniZinc will place the FlatZinc file in some temporary directory, which then also hides the proof created. I didn't really like placing it in the current directory automatically, so I went towards the design I think Glasgow CP uses, where you have to provide the path.

Now --proof takes the path as an argument (--proof-output no longer exists). I considered --prove, but somehow feel like it doesn't fit as well. Maybe exactly because of the reason that you mention that it is a verb and that doesn't match any of the other flags.

You are now allowed to give just a directory as the --proof argument, at which point it will create the proof files in that directory with the base name of the input FlatZinc file.

As suggested, I changed --proof-type to --proof-format.

---

From my side, the only remaining things on my list are seeing whether we can have an option to use the inline literal names/definitions, and if the DRCP team gets back to me to do some testing using their toolchain.