goal_eval messes up variable names

[msaaltink]

The goal_eval and goal_eval_unint commands have the unfortunate effect of renaming the variables used in a goal, so that counterexamples are not easily related to the original formula. For example, without these commands, we get something like

sawscript> prove z3 {{ \y z -> y != (z:[2][8]) }}
[03:35:36.588] prove: 1 unsolved subgoal(s)
[03:35:36.588] Invalid: [y = [0, 0], z = [0, 0]]

while if we include one of these commands

sawscript> prove do { goal_eval; z3; } {{ \y z -> y != (z:[2][8]) }}
[03:36:33.494] prove: 1 unsolved subgoal(s)
[03:36:33.494] Invalid: [x0 = 0, x2 = 0, x1 = 0, x3 = 0]

Obviously in this example we can guess that each of y and z has been replaced by two variables, and can reconstruct the counterexamples in y and z. In larger examples it is not so simple.

The simple answer is to avoid using goal_eval, but there is no other easy way to expand comprehensions, maps, or folds appearing in a formula.

[brianhuffman]

For goals involving free variables (such as proof obligations arising from llvm_verify, or user-created goals using variables made with fresh_symbolic) goal_eval preserves the original variable names. The problem only arises when we have Pi-bound quantified variables in the goal, such as you get when you use prove with a lambda term.

Looking at the implementation of goal_eval, the reason for this is evident on line 541:

saw-script/src/SAWScript/Builtins.hs

Lines 533 to 544 in 6789b1a

	goal_eval :: [String] -> ProofScript ()
	goal_eval unints =
	withFirstGoal $ \goal ->
	do sc <- getSharedContext
	unintSet <- resolveNames unints
	t0 <- liftIO $ propToPredicate sc (goalProp goal)
	let gen = globalNonceGenerator
	sym <- liftIO $ Crucible.newSAWCoreBackend FloatRealRepr sc gen
	(_names, (_mlabels, p)) <- liftIO $ W4Sim.w4Eval sym sc Map.empty unintSet t0
	t1 <- liftIO $ Crucible.toSC sym p
	t2 <- liftIO $ scEqTrue sc t1
	return ((), mempty, Just (goal { goalProp = Prop t2 }))

Function w4Eval from the saw-core what4 backend returns not only the resulting boolean term (p), but also the names of all the pi-bound variables (_names) and information about how to put them back together (_mlabels). So all the information we need is right there, but we throw it away.

What we need to do is use the mlabels to build a substitution to replace the newly-invented free variables with de Bruijn variables (or tuple/record/vector projections of them) and then use names to put the lambda binders back on with the appropriate names.

[brianhuffman]

I just made a PR that fixes the problem. It turns out that it was easier to just avoid sending lambdas to the what4 backend in the first place, converting them to free variables first (because w4Eval already preserves free variables correctly).