Haskell backend supports functional claims directly

[ehildenb]

Part of runtimeverification/k#2491

Should the backend be allowed to use these functional claims as lemmas directly? When discharging other proof goals, we could treat these functional claims as lemmas, to assist in those proofs.

[ana-pantilie]

Requires modifying kore-exec to detect "functional claims", which will be encoded as REQ -> (LHS #Equals (RHS #And ENS)) (in order to be very similar to actual simplification rules) inside spec modules. If the proof fails, return the claim as part of the stuck claims conjunction (as we do with the other type of claims).

See https://github.com/runtimeverification/haskell-backend/blob/master/kore/src/Kore/Reachability/Prove.hs

[ana-pantilie]

If implication simplification works as expected for this feature this should be small

[ana-pantilie]

@JKTKops We need to make sure that #3121 is supported in this feature. A similar test should be added when implementing this.

[ana-pantilie]

What would be the best way to represent EquationalClaims?

It's an implication, always of the form \\implies(requires, \\equals(leftTerm, \\and(rightTerm, ensures))).

simplify :: Pattern -> OrPattern

checkImplication :: claim -> LogicT m (CheckImplicationResult claim)

We want trans1 :: EquationalClaim -> Pattern and trans2 :: OrPattern -> EquationalClaim

For now let's go with EquationalClaim ~ OrPattern.

We will refactor class Claim later to make it more general.

[ana-pantilie]

haskell-backend/kore/test/Test/ConsistentKore.hs

Line 204 in b06757e

patternGen =

is our Pattern generator

@radumereuta let us know when you have a working branch with the frontend support so that we can start integration testing.

[radumereuta]

Front end changes: runtimeverification/k#2733

[JKTKops]

Status update posted on the PR.