Error message for addsimp on non-equation is vague

[Isweet]

If a user tries to add a theorem to a Simplification Set which SAW believes is not an equation then SAW will produce an error. The error message that it produces in this case is vague and doesn't significantly help diagnose the issue.

Example

The following SAW script yields the subsequent error message.

let verify name p t = time do { print (str_concat (str_concat "Verifying " name) "..."); prove_print t (rewrite basic_ss p); };

Example <- verify "example" {{ \(i : [8]) -> i + i == 2 * i }} rme;

let exampleSimps = addsimps [Example] basic_ss;

[14:12:57.350] Stack trace:
"addsimps" (/.../proof.saw:5:20-5:28)
addsimp: theorem not an equation

Recommendations

If possible, it would be helpful if the error also included:

1. The name of the theorem that SAW concluded is not an equation.
2. The (pretty?) printed representation of the theorem that SAW concluded is not an equation.
3. A brief description of why SAW concluded that it is not an equation.

[RyanGlScott]

Since it wasn't obvious to me until I looked closer: this can be repaired by changing basic_ss to (cryptol_ss ()) here:

--- test.saw	2025-01-31 09:36:39.278074863 -0500
+++ test2.saw	2025-01-31 09:36:32.118209640 -0500
@@ -1,4 +1,4 @@
-let verify name p t = time do { print (str_concat (str_concat "Verifying " name) "..."); prove_print t (rewrite basic_ss p); };
+let verify name p t = time do { print (str_concat (str_concat "Verifying " name) "..."); prove_print t (rewrite (cryptol_ss ()) p); };
 
 Example <- verify "example" {{ \(i : [8]) -> i + i == 2 * i }} rme;

This is because SAW does not recognize the Cryptol == function as a primitive equality, but it does recognize it as such after unfolding the intermediate definitions that arise in the cryptol-saw-core translation. See also #1261 (comment).

[sauclovian-g]

Note that the underlying problem that makes this happen is #1261. However, I agree that this error message is nonsense and we should certainly be able to fix it.