Rule System: Trace and verifier

[chriseth]

We can turn the rule system into a verified rule system with the following steps:

1. Translate each rule into an equivalent in e.g. lean and prove the correctness of the rule.
2. When executing the rule system, export a trace similar to a SAT proof that logs which fact was derived using which rule (preliminary pr at Add trace logging. crepe#2 )
3. Implement a verifier (e.g. in lean) that takes two constraint systems A, B and a log L and verifies that B is the result of applying L to A. Prove its correctness.