Rewriter ignores types, creates incorrect term that fails check_goal

[msaaltink]

This is a boiled-down example of something that affects a more serious proof effort. Consider this SawScript

let {{ n1: [8] -> [8]
       n1 x = x + 1

       n2: ([8],[8]) -> ([8],[8])
       n2 (x, y) = (x+1, y+1)

       n3: ([8],[8],[8]) -> ([8],[8],[8])
       n3 (x,y,z) = (x+1, y+1, z+1)
       }};

th3 <- prove_print z3 {{ \ p3 -> n1 (p3.0) == (n3 p3).0 }};
print th3;

prove do { simplify (addsimp th3 empty_ss); print_goal; check_goal; z3; }
      {{ \ p -> n1 ((n2 p).0) == n1 (n1 p.0) }};

The rule th3 should not apply, as the types do not match up. And yet it does:

[18:21:52.560] Loading file "tuple_rules.saw"
[18:21:52.630] Theorem (let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in (p3 : (x@1 * x@1 * x@1))
-> Prelude.EqTrue
     (Cryptol.ecEq x@1 (Cryptol.PEqSeqBool (Cryptol.TCNum 8))
        (cryptol:n1#4682 p3.1)
        (cryptol:n3#4680 p3).1))
[18:21:52.661] Goal prove (goal number 0):
[18:21:52.661] let { x@1 = Vec 8 Bool
    }
 in (p : (x@1 * x@1))
-> EqTrue
     (ecEq x@1 (PEqSeqBool (Cryptol.TCNum 8)) (n3 (n2 p)).1
        (n3 (n3 p)).1)
[18:21:52.708] Stack trace:
"prove" (tuple_rules.saw:19:1-19:6):
"check_goal" (tuple_rules.saw:19:57-19:67):
Inferred type
  let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in x@1 * x@1
Not a subtype of expected type
  let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in x@1 * x@1 * x@1
For term
  cryptol:n2#4681 p

I'm not sure if this is actually unsound, but it is a bit unnerving.

[robdockins]

We do, in fact, have a rewriter on terms that is more careful about potentially type-incorrect rewrites. See: https://github.com/GaloisInc/saw-script/blob/c8edab39ec734d9b1dbceebaf037ab8f4a5d949b/saw-core/src/Verifier/SAW/Rewriter.hs#L678

I don't know offhand if there is a reason we don't use it here.

[brianhuffman]

I don't think rewriteSharedTermTypeSafe would actually help; that variant of the rewriter makes sure not to rewrite any subterm that is a type argument, to ensure that rewriting doesn't change the types of things. The problem here is actually with the matcher: Each rewrite rule includes a list of the types of the unification variables, but when the matcher produces a substitution we don't bother to check that the substitution has the correct types. For nearly all rewrite rules this is not a problem, because the variables usually occur in a context that already fixes its type; that is, if the rest of the rule matches, then the variable's type must match. This particular rule is special because it uses tuple projections, which do not have type arguments that would fix the type of the entire tuple.

https://github.com/GaloisInc/saw-script/blob/c8edab39ec734d9b1dbceebaf037ab8f4a5d949b/saw-core/src/Verifier/SAW/Rewriter.hs#L87-L88

[msaaltink]

Unsurprisingly, with a small tweak this type of thing can crash saw:

let {{ n1: [8] -> [8]
       n1 x = x + 1

       n2: ([8],[8]) -> ([8],[8])
       n2 (x, y) = (x+2, y+3)

       n3: ([8],[8],[8]) -> ([8],[8],[8])
       n3 (x,y,z) = (x+z, y, z)

       apply f x = f x
       }};

th3 <- prove_print z3 {{ \ p3 -> n1 p3.0 == if p3.2 == 1 then (n3 p3).0 else apply n1 p3.0 }};

prove_print do { simplify (addsimp th3 empty_ss); print_goal; z3; }
      {{ \ p -> n1 ((n2 p).0) == p.0 + 3 }};

results in (after printing the ill-typed term)

[02:27:45.010] You have encountered a bug in SawCore's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-script/issues

%< --------------------------------------------------- 
  Revision:  2e4fc0603da85bb1b188d4739a3386e25eea50ab
  Branch:    master (uncommited files present)
  Location:  Verifier.SAW.Simulator.Value.valPairRight
  Message:   Not a pair value:
             <<bitvector>>
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Utils.hs:37:9 in saw-core-0.1-inplace:Verifier.SAW.Utils
  panic, called at src/Verifier/SAW/Simulator/Value.hs:222:18 in saw-core-0.1-inplace:Verifier.SAW.Simulator.Value
  valPairRight, called at src/Verifier/SAW/Simulator.hs:145:32 in saw-core-0.1-inplace:Verifier.SAW.Simulator
%< --------------------------------------------------- 

This can be done with records, too:

let {{ type R2 = {x: Integer, y: Integer }
       type R3 = {x: Integer, y: Integer, z: Integer }

       f1: Integer -> Integer
       f1 = (+) 1

       f2: R2 -> R2
       f2 {x=x, y=y} = { x = x+2, y = y+2}

       f3: R3 -> R3
       f3 {x=x, y=y, z=z} = { x = x+z, y = y, z = z }
    }};

th <- prove_print z3 {{ \ (p3:R3) -> f1 p3.x == if p3.z == 1 then (f3 p3).x else apply f1 p3.x }};

prove_print do { simplify (addsimp th empty_ss); z3; }
      {{ \ (p:R2) -> f1 ((f2 p).x) == p.x + 3 }};

with a similar result

[02:38:49.120] You have encountered a bug in SawCore's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-script/issues

%< --------------------------------------------------- 
  Revision:  2e4fc0603da85bb1b188d4739a3386e25eea50ab
  Branch:    master (uncommited files present)
  Location:  Verifier.SAW.Simulator.Value.valPairRight
  Message:   Not a pair value:
             <<integer>>
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Utils.hs:37:9 in saw-core-0.1-inplace:Verifier.SAW.Utils
  panic, called at src/Verifier/SAW/Simulator/Value.hs:222:18 in saw-core-0.1-inplace:Verifier.SAW.Simulator.Value
  valPairRight, called at src/Verifier/SAW/Simulator.hs:145:32 in saw-core-0.1-inplace:Verifier.SAW.Simulator
%< --------------------------------------------------- 

Admittedly rare, but I did bump into the issue in a real proof, where both affine and projective representations were used.

[brianhuffman]

The right thing to do is to add an extra check after the matching algorithm comes up with a potentially matching rewrite rule. We just need to check the substitution against the ctxt field of the rewrite rule to make sure that the types are correct.

[brianhuffman]

I had a go at fixing this in #1351. However, I found that the type check I implemented was actually too strict, because I was requiring that the types of the variable instantiations syntactically match their declared types. What we really need in this situation is to use the same convertibility check that is used for type checking.

However, I hit a snag when trying to implement that: The convertibility check used by the type checker is actually implemented using the rewriter. So if I called the type checker from the rewriter, we would have a circular dependency, and possibly even an infinite loop.

To properly fix this, I think we would need to reimplement the convertibility check in the type checker so that it doesn't call the rewriter. In any reasonable theorem prover the type checker should be considered more fundamental than the rewriter, so the rewriter should be implemented in terms of it, not the other way around.