From f73a9638bc4410d90e6c070849a765b9b1701ef3 Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Fri, 6 Jan 2023 15:09:24 -0800 Subject: [PATCH 1/2] Revert "Add test" This reverts commit 16b3e3bdf8b8dc75d903d9ebf5ef7613436a725f. --- intTests/test_join_split/README.md | 7 ------- intTests/test_join_split/join_split.saw | 10 ---------- intTests/test_join_split/test.sh | 3 --- 3 files changed, 20 deletions(-) delete mode 100644 intTests/test_join_split/README.md delete mode 100644 intTests/test_join_split/join_split.saw delete mode 100644 intTests/test_join_split/test.sh diff --git a/intTests/test_join_split/README.md b/intTests/test_join_split/README.md deleted file mode 100644 index 03180efab4..0000000000 --- a/intTests/test_join_split/README.md +++ /dev/null @@ -1,7 +0,0 @@ -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. \ No newline at end of file diff --git a/intTests/test_join_split/join_split.saw b/intTests/test_join_split/join_split.saw deleted file mode 100644 index 455b68aafa..0000000000 --- a/intTests/test_join_split/join_split.saw +++ /dev/null @@ -1,10 +0,0 @@ -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 }}; diff --git a/intTests/test_join_split/test.sh b/intTests/test_join_split/test.sh deleted file mode 100644 index deed8e9fc4..0000000000 --- a/intTests/test_join_split/test.sh +++ /dev/null @@ -1,3 +0,0 @@ -#!/usr/bin/env bash - -$SAW join_split.saw \ No newline at end of file From d768a025cd2a9e207bbec8eb5f27bda46ca79fa2 Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Fri, 6 Jan 2023 15:09:38 -0800 Subject: [PATCH 2/2] Revert "Apply `tRebuild` to Cryptol types on import" This reverts commit 8898637709884b720df78862217d6c696e22ae9e. --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index dcbe6db9b4..73d58e3a7d 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -44,7 +44,6 @@ 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(..)) @@ -231,11 +230,10 @@ importPC sc pc = C.PFLiteral -> panic "importPC PFLiteral" [] C.PValidFloat -> panic "importPC PValidFloat" [] --- | 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. +-- | Translate size types to SAW values of type Num, value types to SAW types of sort 0. importType :: SharedContext -> Env -> C.Type -> IO Term importType sc env ty = - case ST.tRebuild ty of + case ty of C.TVar tvar -> case tvar of C.TVFree{} {- Int Kind (Set TVar) Doc -} -> unimplemented "TVFree"