Merge pull request #1790 from GaloisInc/bugfix/normalize-cryptol-types

Normalize Cryptol types on import

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -44,6 +44,7 @@ import qualified Cryptol.Eval.Value as V
 import qualified Cryptol.Eval.Concrete as V
 import Cryptol.Eval.Type (evalValType)
 import qualified Cryptol.TypeCheck.AST as C
+import qualified Cryptol.TypeCheck.SimpType as ST
 import qualified Cryptol.TypeCheck.Subst as C (Subst, apSubst, listSubst, singleTParamSubst)
 import qualified Cryptol.ModuleSystem.Name as C
   (asPrim, asParamName, nameUnique, nameIdent, nameInfo, NameInfo(..))
@@ -230,10 +231,11 @@ importPC sc pc =
     C.PFLiteral        -> panic "importPC PFLiteral" []
     C.PValidFloat      -> panic "importPC PValidFloat" []
 
--- | Translate size types to SAW values of type Num, value types to SAW types of sort 0.
+-- | Normalize according to Cryptol's rules, then translate size types to SAW
+-- values of type Num and value types to SAW types of sort 0.
 importType :: SharedContext -> Env -> C.Type -> IO Term
 importType sc env ty =
-  case ty of
+  case ST.tRebuild ty of
     C.TVar tvar ->
       case tvar of
         C.TVFree{} {- Int Kind (Set TVar) Doc -} -> unimplemented "TVFree"

intTests/test_join_split/README.md

@@ -0,0 +1,7 @@
+This test addresses the issue resolved in [#1790](https://github.com/GaloisInc/saw-script/pull/1790). 
+
+In this script, we prove the same theorem - that ```join`{each=32, parts=4, a=Bool} (split x) == x``` - twice; once purely via `z3`, and once via manual rewriting, trying to use the former to prove the latter. 
+
+Lack of type normalization introduces reflexive type coercions in the SAWCore representation of the expression under proof. The manual proof proceeds by eliminating any extant reflexive coercions, then attempting to use the `z3`-proven theorem as a simplification. When no coercions existed in the first place, the simplification applies cleanly. When coercions existed, the simplification does not apply cleanly, since we eliminated them from the goal, but not from the simplification.
+
+Since this proof is possible to resolve in its entirety via evaluation/appeal to `z3`, we need to maintain the core `join` and `split` functions uninterpreted when manually massaging (via `goal_normalize` and `goal_eval_unint`) the goal into a `trivial`ly resolvable form.

intTests/test_join_split/join_split.saw

@@ -0,0 +1,10 @@
+enable_experimental; // for `goal_normalize`
+
+join_split_thm_z3 <- prove_print z3 {{ \x -> join`{each=32, parts=4, a=Bool} (split x) == x }};
+
+join_split_thm_manual <- prove_print (do {
+    goal_normalize ["ecJoin", "ecSplit"];
+    simplify (addsimp join_split_thm_z3 empty_ss);
+    goal_eval_unint ["ecJoin", "ecSplit"];
+    trivial;
+}) {{ \x -> join`{each=32, parts=4, a=Bool} (split x) == x }};

intTests/test_join_split/test.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+
+$SAW join_split.saw