Potential for dangling variables

[robdockins]

saw-script/src/SAWScript/Proof.hs

Line 191 in 7ee6c7d

ecs <- traverse (\(nm, ty) -> scFreshEC sc nm ty) args

Note this pattern, where we open a term by generating fresh variables for it's Pi-bound arguments and substitute them into the body. If there are dependencies among the types of the arguments, this will result in dangling variables and probably result in some very weird effects later.

[robdockins]

Note, it's pretty easy to trigger this bug when reasoning about quantified goals. Also the eval_goal and eval_goal_unint tactics suffer from basically the same issue.

Consider the following script.

prove_extcore do {
    print_goal;
    hoist_ifs_in_goal;
    print_goal;
  }
  (parse_core "(x : Integer) -> (y:Integer) -> (z:Integer) -> (b:Bool) -> EqTrue (intEq z (ite Integer b x y)) -> EqTrue (ite Bool b (intEq z x) (intEq z y))");

It will produce the following output, where you can see the dangling variables in the output (!0, !1, etc.)

$ saw hoist-bug.saw



[16:11:17.498] Loading file "/Users/rdockins/code/saw-script/hoist-bug.saw"
[16:11:17.501] Goal prove_extcore (goal number 0): prove
at /Users/rdockins/code/saw-script/hoist-bug.saw:3:1-8:160

(x : Integer)
-> (y : Integer)
-> (z : Integer)
-> (b : Bool)
-> EqTrue (intEq z (ite Integer b x y))
-> EqTrue (ite Bool b (intEq z x) (intEq z y))

[16:11:17.502] Goal prove_extcore (goal number 0): prove
at /Users/rdockins/code/saw-script/hoist-bug.saw:3:1-8:160

(x : Integer)
-> (y : Integer)
-> (z : Integer)
-> (b : Bool)
-> EqTrue (intEq !1 (ite Integer !0 !3 !2))
-> EqTrue
     (Prelude.and (Prelude.or (not b) (intEq z x))
        (Prelude.or b (intEq z y)))

[16:11:17.502] Stack trace:
"prove_extcore" (/Users/rdockins/code/saw-script/hoist-bug.saw:3:1-3:14)
prove: 1 unsolved subgoal(s)
Unfinished: 1 goals remaining

[robdockins]

The fix for this is to either unbind a single Pi binder at a time, making sure to instantiate in the body on every step (which will rewrite in the type of further Pi binders as necessary) or to be a bit more clever to avoid re-traversing the term multiple times and only rewrite in the type of each Pi binder as necessary.