Proof Logging

[mmcilree]

This is a rewrite of my previous branch that added proof logging to Huub. My hope is that (after review/revisions) this can merged and viewed as a complete feature, since even if all inference steps are not yet checkable, the hinted proof still constitutes a useful/trimmable log for analysis purposes, and a certificate of correctness for at least the SAT solver part of the LCG solving process.

I am still relatively new to Rust and feedback would be most appreciated.

Summary of Changes

• Adds a --prove option to the CLI to enable proof logging. --prove default uses the name of the fzn as the file name, otherwise a file must be provided.
• Implements the new ProofTracer trait for the Engine struct, allowing it to capture proof information from CaDiCaL
• Uses the trace! macro (with target: proof), to actually log the proof information, not specific to any proof format, and then uses a Targets filter in the trace module to ensure debug log information does not end up in the proof, and vice versa. Note this requires the current tracing_subscriber::Subscriber to be exchanged for a tracing_subscriber::Registry.
• Adds a VeriPBEventFormatter to format generic messages as syntactically correct VeriPB proof lines. Similar formatters for e.g. DRCP/DRAT should be straightforward to add later.
• Finally, adds a ProofHint struct that stores key information that needs to be remembered and logged with clauses in the proof.

Notes about Proof Hint Implementation:

What is a proof hint?

At the moment a "Proof Hint" is just:

1. the original user constraint ids ultimately responsible for this clause, and
2. a name explaining what algorithm/solver function created the clause (will be needed for proof checkers/justifiers).

But it might be that more propagator-specific information should be added here in future.

How am I using proof hints?

A next_proof_hint register is stored in State and set/queried using ProofActions (also implemented for Engine and Solver for convenience). Propagators, reasons, conflicts, and clauses all store an associated Option<ProofHint> within State/Engine. The way this is intended to work is

• Default proof hints are created during Model::to_solver, and are set as the next_proof_hint when each Constraint::to_solver is called.
• Any propagators installed at this point store the current next_proof_hint as their default hint/
• Then, later, each propagator's associated hint is set as the next_proof_hint as soon as the propagator is taken from the propagation queue so that any clauses/reasons created by this propagator can be assigned this hint
• Also, any clauses/reasons have their associated proof hint set as the next_proof_hint immediately before they are posted to the SAT solver.
• Finally in the ProofTracer implementation, the current next_proof_hint is always used for the actual logging message.

Limitations/Improvements

I have not yet benchmarked to see if any of these changes incur a performance cost.

I would try the following improvements to try to speed things up if so:

• At the moment, hints are stored and created regardless of whether logging is enabled (just not written to file): probably it would be better to add checks, and store None in all all the places where hints are used when logging is off.
• The Targets filter might be slightly slower than the original LevelFilter, I've not yet looked into the performance-optimal Layers and Filters.
• Vectors of ints (e.g. clauses, antecedents) cannot be included directly as fields in tracing::Events and must be serialized/deserialized as strings (using their Fmt::Debug representation). Tracing now has the option to support custom Valuable implementations for user types which might improve ergonomics and eliminate the cost of stringifying, although the feature is marked as unstable/experimental.

[codecov]

Codecov Report

❌ Patch coverage is 40.50633% with 188 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/huub-cli/src/trace.rs	13.46%	89 Missing and 1 partial ⚠️
crates/huub/src/reformulate.rs	18.42%	31 Missing ⚠️
crates/huub/src/solver/engine.rs	59.70%	26 Missing and 1 partial ⚠️
crates/huub/src/lib.rs	46.42%	11 Missing and 4 partials ⚠️
crates/huub-cli/src/lib.rs	54.16%	5 Missing and 6 partials ⚠️
crates/huub/src/solver.rs	61.90%	5 Missing and 3 partials ⚠️
crates/huub/src/flatzinc.rs	66.66%	1 Missing and 2 partials ⚠️
crates/huub/src/solver/solving_context.rs	86.95%	3 Missing ⚠️

Files with missing lines	Coverage Δ
crates/huub-cli/src/main.rs	0.00% <ø> (ø)
crates/huub/src/actions.rs	86.00% <ø> (ø)
crates/huub/src/constraints.rs	56.92% <100.00%> (ø)
crates/huub/src/flatzinc.rs	53.24% <66.66%> (+0.09%)	⬆️
crates/huub/src/solver/solving_context.rs	83.39% <86.95%> (+0.05%)	⬆️
crates/huub/src/solver.rs	65.37% <61.90%> (-0.06%)	⬇️
crates/huub-cli/src/lib.rs	59.06% <54.16%> (-0.34%)	⬇️
crates/huub/src/lib.rs	69.27% <46.42%> (-0.72%)	⬇️
crates/huub/src/solver/engine.rs	75.33% <59.70%> (-1.53%)	⬇️
crates/huub/src/reformulate.rs	74.18% <18.42%> (-6.43%)	⬇️
... 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]

CodSpeed Performance Report

Merging #216 will not alter performance

_{Comparing mmcilree:feat/proof_logging (e2c0457) with develop (5f97188)}

Summary

✅ 21 untouched benchmarks

[mmcilree]

I've attempted to turn off the connect_tracer and proof hint apparatus when --prove is not set. Hopefully this will eliminate any overhead when proof logging is disabled.

If there's still a cost to having proof logging, maybe I can look into setting it up as a build-time option so that there's definitely 0 overhead when proof logging is off.

[mmcilree]

@Dekker1 could you possibly approve another workflow run and I'll see if that's made a difference?

[mmcilree]

Thanks. Okay, looking at the codspeed profiling, it seems tracing is more of the issue. I'lll do some more thinking.

EDIT: turns out I was missing a tracing filter on the RegisterLazyLits layer. I've run codspeed on my fork and it looks like the overheads should be much better now 🤞

[Dekker1]

Yes, times look much better now! I think doing the filters correctly in the Registry subscriber seems the important part.

The PR looks pretty good to me now. I might change a few things (e.g. names) before I merge it, but we should be mostly there. Let's meet and discuss!

[mmcilree]

Hi @Dekker1 just looking back over my notes from our last meeting. In terms of what still needs done for this branch, I have:

• Refactor --prove option to be just a bool, and add a --proof-output option to change the output path
• Change proof hint to be an enum - either just an integer reference or an integer with extra hint string
• Use Option<Box<str>> where possible for proof hint strings
• Add means to register propagators with the proof formatted itself, to avoid passing vectors around in the proof hint.

Is that everything? Also do you need access to this branch if you want to make any changes?