✨: Support correctness witness validation

[jossmoff]

Feature Type

• Adding generic functionality to polywit

• Adding language specific functionality to polywit

• Changing existing functionality in polywit

• Removing functionality from polywit

Problem Description

The polywit framework can be extended to support correctness witness validation. This can be implemented in two ways:

• For programs with concrete execution paths i.e no nondeterministic function calls we can use the similar execution based methods to the violation witness framework.
• For nondeterministic programs, we can use validation via verification similar to MetaVal [1].

Feature Description

We can add functionality to the witness processor to process the correctness witnesses format [2]. Instead of creating a test harness we can have a verification harness. We can share functionality between the two to extend a common base class ValidationHarness to share stuff such as the validation execution command.

Alternative Solutions

There are other methods for correctness validation such as automata based methods however polywit revolves around processing compilation units and a witness. Validation by verification lends better to this as it is similar to the execution based violation validation.

Additional Context

No response