Merge pull request #2610 from GaloisInc/bh/sawcore-prelude

Remove unused definitions from SAWCore prelude

Author: brianhuffman

intTests/test2049/test.log.1.good

@@ -13,12 +13,12 @@ Literal equality postcondition
 Expected term: 
 let { x@1 = Prelude.Vec 8 Prelude.Bool
     }
- in fresh:zero::table#1583
+ in fresh:zero::table#1523
 Actual term:
 let { x@1 = Prelude.Vec 8 Prelude.Bool
     }
- in Cryptol.ecArrayUpdate x@1 x@1 fresh:zero::table#1583
-      fresh:zero::k#1584
+ in Cryptol.ecArrayUpdate x@1 x@1 fresh:zero::table#1523
+      fresh:zero::k#1524
       (Prelude.bvNat 8 0)
 
  SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = N}

intTests/test2049/test.log.2.good

@@ -13,12 +13,12 @@ Literal equality postcondition
 Expected term: 
 let { x@1 = Prelude.Vec 8 Prelude.Bool
     }
- in fresh:zero::table#1583
+ in fresh:zero::table#1523
 Actual term:
 let { x@1 = Prelude.Vec 8 Prelude.Bool
     }
- in Cryptol.ecArrayUpdate x@1 x@1 fresh:zero::table#1583
-      fresh:zero::k#1584
+ in Cryptol.ecArrayUpdate x@1 x@1 fresh:zero::table#1523
+      fresh:zero::k#1524
       (Prelude.bvNat 8 0)
 
  SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = N}

intTests/test_llvm_errors/err001.log.good

@@ -8,11 +8,11 @@ Expected term:
 let { x@1 = Prelude.Vec 32 Prelude.Bool
       x@2 = Cryptol.TCNum 32
     }
- in Cryptol.ecMul x@1 (Cryptol.PRingSeqBool x@2) fresh:x#1580
+ in Cryptol.ecMul x@1 (Cryptol.PRingSeqBool x@2) fresh:x#1520
       (Cryptol.ecNumber (Cryptol.TCNum 3) x@1
          (Cryptol.PLiteralSeqBool x@2))
 Actual term:
-Prelude.bvMul 32 (Prelude.bvNat 32 2) fresh:x#1580
+Prelude.bvMul 32 (Prelude.bvNat 32 2) fresh:x#1520
 
  SolverStats {solverStatsSolvers = fromList ["SBV->Z3"], solverStatsGoalSize = N}
  ----------Counterexample----------

saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v

@@ -83,47 +83,3 @@ Lemma bvToNat_bounds (w : nat) (x : bitvector w) :
 Proof.
   holds_for_bits_up_to_3; try repeat constructor.
 Qed.
-
-Theorem at_gen_BVVec :
-  forall (n : nat) (len : bitvector n) (a : Type)
-         (f : forall i : bitvector n, is_bvult n i len -> a)
-         (ix : bitvector n) (pf : is_bvult n ix len),
-  atBVVec n len a (genBVVec n len a f) ix pf = f ix pf.
-Proof.
-  intros n len a f ix pf.
-  unfold atBVVec, genBVVec.
-  rewrite at_gen_Vec.
-  generalize (IsLtNat_to_bvult n len (bvToNat n ix)
-               (bvult_to_IsLtNat n len (bvToNat n ix)
-                 (trans bool (bvult n (bvNat n (bvToNat n ix)) len) (bvult n ix len) 1%bool
-                   (eq_cong (bitvector n) (bvNat n (bvToNat n ix)) ix (bvNat_bvToNat n ix) bool
-                     (fun y : bitvector n => bvult n y len)) pf))) as pf2.
-  rewrite (bvNat_bvToNat n ix).
-  intros pf2.
-  rewrite (UIP_dec Bool.bool_dec pf2 pf).
-  reflexivity.
-Qed.
-
-Lemma gen_at_BVVec :
-  forall (n : nat) (len : bitvector n) (a : Type) (x : BVVec n len a),
-  genBVVec n len a (atBVVec n len a x) = x.
-Proof.
-  intros n len a x.
-  unfold genBVVec, atBVVec.
-  rewrite <- (gen_at_Vec _ _ x) at 1.
-  f_equal. extensionality i. extensionality pf.
-  generalize (bvult_to_IsLtNat n len (bvToNat n (bvNat n i))
-               (trans bool (bvult n (bvNat n (bvToNat n (bvNat n i))) len) (bvult n (bvNat n i) len) 1%bool
-                 (eq_cong (bitvector n) (bvNat n (bvToNat n (bvNat n i))) (bvNat n i)
-                    (bvNat_bvToNat n (bvNat n i)) bool (fun y : bitvector n => bvult n y len))
-                 (IsLtNat_to_bvult n len i pf))) as pf2.
-  assert (X : bvToNat n (bvNat n i) = i).
-  { apply bvToNat_bvNat.
-    transitivity (bvToNat n len).
-    - exact pf.
-    - apply bvToNat_bounds.
-  }
-  rewrite X. intros pf2.
-  rewrite (le_unique _ _ pf2 pf).
-  reflexivity.
-Qed.

saw-core-coq/src/SAWCoreCoq/SpecialTreatment.hs

@@ -375,7 +375,6 @@ sawCorePreludeSpecialTreatmentMap configuration =
   ++
   [ ("EmptyVec",      mapsTo vectorsModule "EmptyVec")
   , ("at",            rename "sawAt") -- `at` is a reserved keyword in Coq
-  , ("at_gen_BVVec",  mapsTo preludeExtraModule "at_gen_BVVec")
   , ("atWithDefault", mapsTo vectorsModule "atWithDefault")
   , ("atWithProof",   mapsTo vectorsModule "atWithProof")
   , ("at_single",     skip) -- is boring, could be proved on the Coq side
@@ -405,7 +404,6 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("foldl",         mapsTo vectorsModule "foldl")
   , ("foldl_nil",     mapsTo vectorsModule "foldl_nil")
   , ("foldl_cons",    mapsTo vectorsModule "foldl_cons")
-  , ("gen_at_BVVec",  mapsTo preludeExtraModule "gen_at_BVVec")
   , ("genWithProof",  mapsTo vectorsModule "genWithProof")
   , ("scanl",         mapsTo vectorsModule "scanl")
   , ("gen",           mapsTo vectorsModule "gen")
@@ -508,15 +506,6 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("Right",       mapsToExpl datatypesModule "inr")
   ]
 
-  -- Dependent pairs
-  ++
-  [ ("Sigma", replace (Coq.ExplVar "sigT"))
-  , ("exists", replace (Coq.ExplVar "existT"))
-  , ("Sigma__rec", replace (Coq.ExplVar "sigT_rect"))
-  , ("Sigma_proj1", replace (Coq.ExplVar "projT1"))
-  , ("Sigma_proj2", replace (Coq.ExplVar "projT2"))
-  ]
-
   -- Lists
   ++
   [ ("List", mapsToExpl datatypesModule "list")
@@ -525,16 +514,6 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("List__rec", mapsToExpl datatypesModule "list_rect")
   ]
 
-  -- Lists at sort 1
-  {- FIXME: in order to support lists at a higher sort, we need a universe
-     polymorphic version of them
-  ++
-  [ ("List1", mapsToExpl polyListModule "plist")
-  , ("Nil1", mapsToExpl polyListModule "pnil")
-  , ("Cons1", mapsToExpl polyListModule "pcons")
-  ]
-  -}
-
 escapeIdent :: Coq.Ident -> Coq.Ident
 escapeIdent (Coq.Ident str)
   | all okChar str = Coq.Ident str