Merge pull request #1216 from GaloisInc/proof-summary

Proof summary improvements

cabal.project

@@ -4,6 +4,7 @@ packages:
     crux-mir-comp
     cryptol-saw-core
     rme
+    verif-viewer
     saw-core
     saw-core-aig
     saw-core-sbv

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

@@ -1624,9 +1624,9 @@ scCryptolType sc t =
 scCryptolEq :: SharedContext -> Term -> Term -> IO Term
 scCryptolEq sc x y =
   do rules <- concat <$> traverse defRewrites defs
-     let ss = addConvs natConversions (addRules rules emptySimpset)
-     tx <- scTypeOf sc x >>= rewriteSharedTerm sc ss >>= scCryptolType sc
-     ty <- scTypeOf sc y >>= rewriteSharedTerm sc ss >>= scCryptolType sc
+     let ss = addConvs natConversions (addRules rules emptySimpset :: Simpset ())
+     tx <- scTypeOf sc x >>= rewriteSharedTerm sc ss >>= scCryptolType sc . snd
+     ty <- scTypeOf sc y >>= rewriteSharedTerm sc ss >>= scCryptolType sc . snd
      unless (tx == ty) $
        panic "scCryptolEq"
                  [ "scCryptolEq: type mismatch between"

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

@@ -18,7 +18,7 @@ import Verifier.SAW.Rewriter
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.Term.Functor
 
-mkCryptolSimpset :: SharedContext -> IO Simpset
+mkCryptolSimpset :: SharedContext -> IO (Simpset a)
 mkCryptolSimpset sc =
   do m <- scFindModule sc cryptolModuleName
      scSimpset sc (cryptolDefs m) [] []

examples/ecdsa/ecdsa.saw

@@ -289,7 +289,7 @@ let ss0 = add_prelude_eqs [ "bvShiftL_bvShl"
                           , "bvShiftR_bvShr"
                           ] cry_ss;
 
-let crule t = rewrite ss0 t;
+let assume_rule t = prove_print (admit "assume rule") (rewrite ss0 t);
 let prove_rule t = prove_print abc (rewrite ss0 t);
 
 let ss1 = add_prelude_eqs
@@ -365,16 +365,19 @@ ec_join_split_768 <- prove_rule {{ \x -> ec_join768 (ec_split768 x) == x }};
 ec_split_join_768 <- prove_rule {{ \x -> ec_split768 (ec_join768 x) == x }};
 
 // Axiomatic rules: For now, we assume these without proof.
-let mul_java_elim = crule {{ \(a:[768]) -> \(x:[384]) -> \(y:[384]) ->
-                     mul_java::mul_java (a, x, y) == p384_field::p384_safe_product (x, y) }};
-let sq_java_elim = crule {{ \(a:[768]) -> \(x:[384]) ->
-                     mul_java::sq_java (a, x) == p384_field::p384_safe_product (x, x) }};
+mul_java_elim <- assume_rule
+  {{ \(a:[768]) -> \(x:[384]) -> \(y:[384]) ->
+       mul_java::mul_java (a, x, y) == p384_field::p384_safe_product (x, y) }};
+
+sq_java_elim <- assume_rule
+  {{ \(a:[768]) -> \(x:[384]) ->
+       mul_java::sq_java (a, x) == p384_field::p384_safe_product (x, x) }};
 
 let basic_simps  = [ ec_join_split
                    , at12, at24
                    ];
 let ss3 = addsimps basic_simps ss2;
-let ss4 = addsimps' [mul_java_elim, sq_java_elim] ss3;
+let ss4 = addsimps [mul_java_elim, sq_java_elim] ss3;
 let ss = add_prelude_defs
   [ "bvUpd"
   , "bvAt"

examples/misc/rewrite.saw

@@ -1,9 +1,12 @@
-let crule t = do { ss <- cryptol_ss ; rewrite ss t; };
+let ss = cryptol_ss ();
+let crule t = rewrite ss t;
 
 rule <- crule {{ \(x:[384]) -> join ((split x) : [12][32]) == x }};
+rule_thm <- prove_print (admit "assume rule") rule;
+
 print "== Original version of rule:";
 print_term rule;
-let rule_ss = addsimps' [rule] empty_ss;
+let rule_ss = addsimps [rule_thm] empty_ss;
 t <- rewrite rule_ss rule;
 print "== Rule rewritten with itself:";
 print_term t;

saw-core/src/Verifier/SAW/Constant.hs

@@ -18,5 +18,5 @@ import Verifier.SAW.Conversion
 scConst :: SharedContext -> Text -> Term -> IO Term
 scConst sc name t = do
   ty <- scTypeOf sc t
-  ty' <- rewriteSharedTerm sc (addConvs natConversions emptySimpset) ty
+  (_,ty') <- rewriteSharedTerm sc (addConvs natConversions emptySimpset :: Simpset ()) ty
   scConstant sc name t ty'