prove_core has unhelpful error message "Term is not a proposition"

[brianhuffman]

I have a polymorphic rewrite rule that I'd like to prove, which quantifies over a variable n : Nat that is used as a vector size parameter. It should be provable just by unfolding some definitions. But prove_core rejects it with an error message before even running the proof tactic, saying "Term is not a proposition".

prove_core
  do {
    simplify (cryptol_ss ());
    z3;
  }
  "\\ (n : Nat) -> \\ (x : Vec n Bool) -> Eq Integer (sbvToInt n x) (toSignedInteger (TCNum n) x)";

Stack trace:
"prove_core" (<stdin>:1:1-1:11):
termToProp: Term is not a proposition
\(n : Prelude.Nat) ->
  \(x : Prelude.Vec n Prelude.Bool) ->
    Prelude.Eq
      Prelude.Integer
      (Prelude.sbvToInt n x)
      (Cryptol.toSignedInteger (Cryptol.TCNum n) x)
(n : Prelude.Nat)
-> (x : Prelude.Vec n Prelude.Bool)
-> Prop

[robdockins]

I think you need to use Pi instead of lambda to state propositions.

[RyanGlScott]

Indeed, I ran into this issue in a separate context: aws/s2n-tls@d5a044b#diff-ae328ea2909d8141691e3a608d7acef67c9900d80e3c58a8ce08e341fb578d69R39

[robdockins]

You'll shortly run into a separate problem, though, which is that Nat isn't a first-order type.

[brianhuffman]

@robdockins Yes, of course, that's it. I was switching from prove_print (where you do need to use lambdas) to prove_core and forgot to switch from lambda to pi.

In that case, the bug is that the error message is unhelpful. I assumed it was complaining about quantification over Nat instead of the fact that it found a lambda instead of a pi.

[robdockins]

The following script just doesn't quite work. We should probably make "trivial" a little less trivial:

prove_core
  do {
    simplify (cryptol_ss ());
    print_goal;
    trivial;
  }
  "(n : Nat) -> (x : Vec n Bool) -> Eq Integer (sbvToInt n x) (toSignedInteger (TCNum n) x)";

[18:56:07.043] Goal prove (goal number 0):
[18:56:07.043] (n : Nat)
-> (x : Vec n Bool)
-> let { x@1 = sbvToInt n x
    }
 in Eq Integer x@1 x@1
[18:56:07.043] Stack trace:
"prove_core" (/Users/rdockins/code/pate/test.saw:1:1-1:11):
"trivial" (/Users/rdockins/code/pate/test.saw:5:5-5:12):
trivial tactic: not a trivial goal

[brianhuffman]

Yes, it would be good to make trivial handle any proofs by reflexivity. I'll make a separate ticket for that. I think I can work around it for now.

EDIT: See #1567.

[brianhuffman]

Here's my workaround, for the record:

fold_toSignedInteger <-
  prove_core
  do {
    simplify (addsimps [intEq_refl] (cryptol_ss ()));
    trivial;
  }
  "(n : Nat) -> (x : Vec n Bool) -> EqTrue (intEq (sbvToInt n x) (toSignedInteger (TCNum n) x))";

where intEq_refl is a previously-proved rewrite rule for intEq x x = True.

[robdockins]

The current error is produced here:

saw-script/src/SAWScript/Proof.hs

Lines 139 to 148 in db538d3

	-- | Turn a saw-core term into a proposition under the type-as-propositions
	-- regime. The given term must be a type, which means that its own type
	-- is a sort.
	termToProp :: SharedContext -> Term -> IO Prop
	termToProp sc tm =
	do mmap <- scGetModuleMap sc
	ty <- scTypeOf sc tm
	case evalSharedTerm mmap mempty mempty ty of
	TValue (VSort s) | s == propSort -> return (Prop tm)
	_ -> fail $ unlines [ "termToProp: Term is not a proposition", showTerm tm, showTerm ty ]

It would probably not be hard to add a little extra step there to check if the leading symbol is a lambda and print an additional hint in that case.

[robdockins]

Indeed, I ran into this issue in a separate context: aws/s2n-tls@d5a044b#diff-ae328ea2909d8141691e3a608d7acef67c9900d80e3c58a8ce08e341fb578d69R39

Well, hummm. I thought that GaloisInc/s2n#7 had been pushed upstream.

[robdockins]

Fixed via #1568