Merge pull request #1470 from GaloisInc/coq-inhabited

Coq inhabited errors

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

@@ -174,7 +174,7 @@ normalizeProp prop
 importKind :: SharedContext -> C.Kind -> IO Term
 importKind sc kind =
   case kind of
-    C.KType       -> scSort sc (mkSort 0)
+    C.KType       -> scISort sc (mkSort 0)
     C.KNum        -> scDataTypeApp sc "Cryptol.Num" []
     C.KProp       -> scSort sc (mkSort 0)
     (C.:->) k1 k2 -> join $ scFun sc <$> importKind sc k1 <*> importKind sc k2

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

@@ -528,7 +528,7 @@ Definition multiFixM {lrts:LetRecTypes}
   multiTupleFixM lrts (fun fs => lrtApply F fs).
 
 (* A letrec construct for binding 0 or more mutually recursive functions *)
-Definition letRecM {lrts : LetRecTypes} {B} (F: lrtPi lrts (lrtTupleType lrts))
+Definition letRecM (lrts : LetRecTypes) {B} (F: lrtPi lrts (lrtTupleType lrts))
            (body:lrtPi lrts (CompM B)) : CompM B :=
   lrtApply body (multiFixM F).
 

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

@@ -120,7 +120,7 @@ Proof.
   unfold sawAt. now simpl.
 Qed.
 
-Lemma gen_sawAt T
+Lemma gen_sawAt T {HT : Inhabited T}
   : forall (m : Nat) a, gen m T (fun i => sawAt m T a i) = a.
 Proof.
   apply Vector.t_ind.
@@ -132,20 +132,19 @@ Proof.
     move => h n t IH.
     simpl.
     f_equal.
-    setoid_rewrite sawAt_S.
-    apply IH.
+    exact IH.
   }
 Qed.
 
-Lemma append_cons m n T h t v
+Lemma append_cons m n T {HT:Inhabited T} h t v
   : append m.+1 n T (cons T h m t) v
     =
     cons T h _ (append m n T t v).
 Proof.
   reflexivity.
 Qed.
 
-Theorem rewrite_append T n (w : Vec n T)
+Theorem rewrite_append T {HT:Inhabited T} n (w : Vec n T)
   : forall m (v : Vec m T),
     existT _ (addNat m n) (append m n T v w)
     =
@@ -161,7 +160,7 @@ Proof.
   }
   {
     simpl => h m t IH.
-    setoid_rewrite append_cons.
+    rewrite append_cons.
     dependent rewrite IH.
     reflexivity.
   }

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

@@ -6,12 +6,42 @@ From Coq Require        Numbers.NatInt.NZLog.
 From Coq Require Import Strings.String.
 From CryptolToCoq Require Export CompM.
 
+(** A typeclass we use to restrict applications of the "error" axiom
+  * to inhabited types. This allows the axiom to be realizable, and
+  * prevents us from constructing an inconsistent environment.
+  *
+  * The basic idea is that typeclass instances will be used to construct
+  * the necessary inhabitants at use sites, so instances will be needed
+  * for all the types expected to be involved in calls to "error".
+  *)
+Class Inhabited (a:Type) := MkInhabited { inhabitant : a }.
+
+Axiom error : forall (a : Type) {HI:Inhabited a}, String.string -> a.
+
+Definition error_realizable : forall {a : Type} {HI:Inhabited a}, String.string -> a.
+Proof. intros; exact inhabitant. Qed.
+
 Definition sort (n : nat) := Type.
 
-Axiom error : forall {a : Type}, String.string -> a.
+Instance Inhabited_Type : Inhabited Type :=
+  MkInhabited Type unit.
+Instance Inhabited_sort (n:nat) : Inhabited (sort n) :=
+  MkInhabited (sort n) unit.
+
+Instance Inhabited_Intro (a:Type) (b:a -> Type) (Hb: forall x, Inhabited (b x))
+  : Inhabited (forall x, b x)
+  := MkInhabited (forall x, b x) (fun x => @inhabitant (b x) (Hb x)).
+
+Global Hint Extern 5 (Inhabited ?A) =>
+  (apply (@MkInhabited A); intuition (eauto with typeclass_instances inh)) : typeclass_instances.
 
 Definition String := String.string.
 
+Instance Inhabited_String : Inhabited String :=
+  MkInhabited String ""%string.
+Instance Inhabited_string : Inhabited String.string :=
+  MkInhabited String.string ""%string.
+
 Definition equalString (s1 s2: String) : bool :=
   match String.string_dec s1 s2 with
   | left _ => true
@@ -37,6 +67,16 @@ Definition or     := orb.
 Definition xor    := xorb.
 Definition boolEq := Coq.Bool.Bool.eqb.
 
+Instance Inhabited_Unit : Inhabited UnitType :=
+  MkInhabited UnitType tt.
+Instance Inhabited_Bool : Inhabited Bool :=
+  MkInhabited Bool false.
+
+Instance Inhabited_unit : Inhabited unit :=
+  MkInhabited unit tt.
+Instance Inhabited_bool : Inhabited bool :=
+  MkInhabited bool false.
+
 (* SAW uses an alternate form of eq_rect where the motive function P also
 depends on the equality proof itself *)
 Definition Eq__rec (A : Type) (x : A) (P: forall y, x=y -> Type) (p:P x eq_refl) y (e:x=y) :
@@ -117,6 +157,14 @@ Definition sawUnsafeCoerce (a b : Type) (x : a) := x.
 Definition Nat := nat.
 Definition Nat_rect := nat_rect.
 
+Instance Inhabited_Nat : Inhabited Nat :=
+  MkInhabited Nat 0%nat.
+Instance Inhabited_nat : Inhabited nat :=
+  MkInhabited nat 0%nat.
+
+Global Hint Resolve (0%nat : nat) : inh.
+Global Hint Resolve (0%nat : Nat) : inh.
+
 (* Definition minNat := Nat.min. *)
 
 Definition uncurry (a b c : Type) (f : a -> b -> c) (p : a * (b * unit)) : c  :=
@@ -141,6 +189,10 @@ Definition snd {A B} := @snd A B.
 Definition Zero := O.
 Definition Succ := S.
 
+Instance Inhabited_Pair (a b:Type) {Ha : Inhabited a} {Hb : Inhabited b} : Inhabited (PairType a b) :=
+    MkInhabited (PairType a b) (PairValue a b inhabitant inhabitant).
+Instance Inhabited_prod (a b:Type) {Ha : Inhabited a} {Hb : Inhabited b} : Inhabited (prod a b) :=
+    MkInhabited (prod a b) (pair inhabitant inhabitant).
 
 Definition Integer := Z.
 Definition intAdd : Integer -> Integer -> Integer := Z.add.
@@ -158,6 +210,15 @@ Definition intLt : Integer -> Integer -> Bool := Z.ltb.
 Definition intToNat : Integer -> Nat := Z.to_nat.
 Definition natToInt : Nat -> Integer := Z.of_nat.
 
+Instance Inhabited_Intger : Inhabited Integer :=
+  MkInhabited Integer 0%Z.
+Instance Inhabited_Z : Inhabited Z :=
+  MkInhabited Z 0%Z.
+
+Global Hint Resolve (0%Z : Z) : inh.
+Global Hint Resolve (0%Z : Integer) : inh.
+
+
 (* NOTE: the following will be nonsense for values of n <= 1 *)
 Definition IntMod (n : nat) := Z.
 Definition toIntMod (n : Nat) : Integer -> IntMod n := fun i => Z.modulo i (Z.of_nat n).
@@ -174,6 +235,8 @@ Definition intModMul : forall (n : Nat), (IntMod n) -> (IntMod n) -> IntMod n
 Definition intModNeg : forall (n : Nat), (IntMod n) -> IntMod n
   := fun _ => ZModulo.opp.
 
+Instance Inhabited_IntMod (n:nat) : Inhabited (IntMod n) :=
+  MkInhabited (IntMod n) 0%Z.
 
 (***
  *** A simple typeclass-based implementation of SAW record types
@@ -194,6 +257,13 @@ Variant RecordTypeCons (str:String.string) (tp:Type) (rest_tp:Type) : Type :=
 Arguments RecordTypeCons str%string_scope tp rest_tp.
 Arguments RecordCons str%string_scope {tp rest_tp} x rest.
 
+Instance Inhabited_RecordNil : Inhabited RecordTypeNil :=
+    MkInhabited RecordTypeNil RecordNil.
+Instance Inhabited_RecordCons (fnm:String.string) (tp rest_tp:Type)
+  {Htp : Inhabited tp} {Hrest : Inhabited rest_tp}
+  : Inhabited (RecordTypeCons fnm tp rest_tp)
+  := MkInhabited (RecordTypeCons fnm tp rest_tp) (RecordCons fnm inhabitant inhabitant).
+
 (* Get the head element of a non-empty record type *)
 Definition recordHead {str tp rest_tp} (r:RecordTypeCons str tp rest_tp) : tp :=
   match r with

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

@@ -32,6 +32,9 @@ Fixpoint gen (n : nat) (a : Type) (f : nat -> a) {struct n} : Vec n a.
     ).
 Defined.
 
+Instance Inhabited_Vec (n:nat) (a:Type) {Ha:Inhabited a} : Inhabited (Vec n a) :=
+  MkInhabited (Vec n a) (gen n a (fun _ => inhabitant)).
+
 Theorem gen_domain_eq n T : forall f g (domain_eq : forall i, f i = g i),
     gen n T f = gen n T g.
 Proof.
@@ -282,11 +285,13 @@ Definition bvSShr (w : nat) (a : bitvector w.+1) (n : nat)
   := a.
 Global Opaque bvSShr.
 
+(* FIXME this is not implemented *)
 Definition bvShl (w : nat) (a : bitvector w) (n : nat)
   : bitvector w
   := a.
 Global Opaque bvShl.
 
+(* FIXME this is not implemented *)
 Definition bvShr (w : nat) (a : bitvector w) (n : nat)
   : bitvector w
   := a.

saw-core-coq/src/Language/Coq/AST.hs

@@ -42,10 +42,12 @@ type Type = Term
 
 data Binder
   = Binder Ident (Maybe Type)
+  | ImplicitBinder Ident (Maybe Type)
     deriving (Show)
 
 data PiBinder
   = PiBinder (Maybe Ident) Type
+  | PiImplicitBinder (Maybe Ident) Type
     deriving (Show)
 
 -- Because saw-core does not give very helpful access to the parameters and

saw-core-coq/src/Language/Coq/Pretty.hs

@@ -58,11 +58,16 @@ ppIdent = text
 ppBinder :: Binder -> Doc ann
 ppBinder (Binder x Nothing)  = ppIdent x
 ppBinder (Binder x (Just t)) = parens (ppIdent x <+> colon <+> ppTerm PrecNone t)
+ppBinder (ImplicitBinder x Nothing)  = braces (ppIdent x)
+ppBinder (ImplicitBinder x (Just t)) = braces (ppIdent x <+> colon <+> ppTerm PrecNone t)
 
 ppPiBinder :: PiBinder -> Doc ann
 ppPiBinder (PiBinder Nothing t)  = ppTerm PrecApp t <+> text "->"
 ppPiBinder (PiBinder (Just x) t) =
   text "forall" <+> parens (ppIdent x <+> colon <+> ppTerm PrecNone t) <> comma
+ppPiBinder (PiImplicitBinder Nothing t)  = braces (ppTerm PrecApp t) <+> text "->"
+ppPiBinder (PiImplicitBinder (Just x) t) =
+  text "forall" <+> braces (ppIdent x <+> colon <+> ppTerm PrecNone t) <> comma
 
 ppBinders :: [Binder] -> Doc ann
 ppBinders = hsep . map ppBinder

saw-core-coq/src/Verifier/SAW/Translation/Coq.hs

@@ -149,6 +149,7 @@ translateCryptolModule nm configuration globalDecls m =
   in
   Coq.ppDecl . Coq.Section nm <$> decls
 
-moduleDeclName :: ModuleDecl -> String
-moduleDeclName (TypeDecl (DataType { dtName })) = identName dtName
-moduleDeclName (DefDecl  (Def      { defIdent })) = identName defIdent
+moduleDeclName :: ModuleDecl -> Maybe String
+moduleDeclName (TypeDecl (DataType { dtName })) = Just (identName dtName)
+moduleDeclName (DefDecl  (Def      { defIdent })) = Just (identName defIdent)
+moduleDeclName InjectCodeDecl{} = Nothing

saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs

@@ -27,7 +27,7 @@ module Verifier.SAW.Translation.Coq.SAWModule where
 import qualified Control.Monad.Except                          as Except
 import           Control.Monad.Reader                          hiding (fail)
 import           Prelude                                       hiding (fail)
-import           Prettyprinter                                 (Doc)
+import           Prettyprinter                                 (Doc, pretty)
 
 import qualified Language.Coq.AST                              as Coq
 import qualified Language.Coq.Pretty                           as Coq
@@ -84,10 +84,10 @@ translateDataType :: ModuleTranslationMonad m => DataType -> m Coq.Decl
 --   | trace ("translateDataType: " ++ show dtName) False = undefined
 translateDataType (DataType {..}) =
   atDefSite <$> findSpecialTreatment dtName >>= \case
-  DefPreserve              -> translateNamed $ identName dtName
-  DefRename   _ targetName -> translateNamed $ targetName
-  DefReplace  str          -> return $ Coq.Snippet str
-  DefSkip                  -> return $ skipped dtName
+  DefPreserve            -> translateNamed $ identName dtName
+  DefRename   targetName -> translateNamed $ targetName
+  DefReplace  str        -> return $ Coq.Snippet str
+  DefSkip                -> return $ skipped dtName
   where
     translateNamed :: ModuleTranslationMonad m => Coq.Ident -> m Coq.Decl
     translateNamed name = do
@@ -128,10 +128,10 @@ translateDef (Def {..}) = {- trace ("translateDef " ++ show defIdent) $ -} do
   where
 
     translateAccordingly :: ModuleTranslationMonad m => DefSiteTreatment -> m Coq.Decl
-    translateAccordingly  DefPreserve             = translateNamed $ identName defIdent
-    translateAccordingly (DefRename _ targetName) = translateNamed $ targetName
-    translateAccordingly (DefReplace  str)        = return $ Coq.Snippet str
-    translateAccordingly  DefSkip                 = return $ skipped defIdent
+    translateAccordingly  DefPreserve           = translateNamed $ identName defIdent
+    translateAccordingly (DefRename targetName) = translateNamed $ targetName
+    translateAccordingly (DefReplace  str)      = return $ Coq.Snippet str
+    translateAccordingly  DefSkip               = return $ skipped defIdent
 
     translateNamed :: ModuleTranslationMonad m => Coq.Ident -> m Coq.Decl
     translateNamed name = liftTermTranslationMonad (go defQualifier defBody)
@@ -179,3 +179,6 @@ translateDecl configuration modname decl =
     case runModuleTranslationMonad configuration modname (translateDef dd) of
       Left e -> error $ show e
       Right (tdecl, _) -> Coq.ppDecl tdecl
+  InjectCodeDecl ns txt
+    | ns == "Coq" -> pretty txt
+    | otherwise   -> mempty

saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs

@@ -43,15 +43,31 @@ data SpecialTreatment = SpecialTreatment
   , identSpecialTreatment :: Map.Map ModuleName (Map.Map String IdentSpecialTreatment)
   }
 
+-- | How to handle SAWCore identifiers at their definition sites.
 data DefSiteTreatment
-  = DefPreserve
-  | DefRename   (Maybe ModuleName) String -- optional module rename, then identifier itself
-  | DefReplace  String
+  = -- | Translate the identifier unchanged, and directly translate the assocated
+    --   SAWCore declaration.
+    DefPreserve
+  | -- | Translate the identifier into the given Coq identifer,
+    --   and otherwise directly translate the associated SAWCore declaration.
+    DefRename String
+  | -- | Replace the declaration of the identifier with the given text.
+    DefReplace  String
+    -- | Skip the declartion of the identifier altogether.
   | DefSkip
 
+-- | How to translate SAWCore identifiers at their use sites.
 data UseSiteTreatment
-  = UsePreserve
-  | UseRename   (Maybe ModuleName) String
+  = -- | Translate the identifier unchanged
+    UsePreserve
+    -- | Rename the given identifier into the given (optionally qualified)
+    --   Coq identifier.  The boolean value, if true, indicates that the
+    --   identifier should be an "explicit" identifier with a leading \"\@\"
+    --   symbol, which indicates to Coq that all implicit arguments should be
+    --   treated as explicit.
+  | UseRename   (Maybe ModuleName) String Bool
+    -- | Drop the first @n@ SAWCore arguments to this identifier, then replace
+    --   the occurence with the given Coq term.
   | UseReplaceDropArgs  Int Coq.Term
 
 data IdentSpecialTreatment = IdentSpecialTreatment
@@ -91,9 +107,16 @@ findSpecialTreatment ident = do
 mapsTo :: ModuleName -> String -> IdentSpecialTreatment
 mapsTo targetModule targetName = IdentSpecialTreatment
   { atDefSite = DefSkip
-  , atUseSite = UseRename (Just targetModule) targetName
+  , atUseSite = UseRename (Just targetModule) targetName False
   }
 
+-- Like @mapsTo@ but use an explicit variable reference so
+-- that all implicit arguments must be provided.
+mapsToExpl :: ModuleName -> String -> IdentSpecialTreatment
+mapsToExpl targetModule targetName = IdentSpecialTreatment
+  { atDefSite = DefSkip
+  , atUseSite = UseRename (Just targetModule) targetName True
+  }
 -- Use `realize` for axioms that can be realized, or for primitives that must be
 -- realized.  While some primitives can be written directly in a standalone Coq
 -- module, some primitives depend on code from the extracted module, and are
@@ -113,8 +136,8 @@ realize code = IdentSpecialTreatment
 -- Also useful for translation notations, until they are better supported.
 rename :: String -> IdentSpecialTreatment
 rename ident = IdentSpecialTreatment
-  { atDefSite = DefRename Nothing ident
-  , atUseSite = UseRename Nothing ident
+  { atDefSite = DefRename ident
+  , atUseSite = UseRename Nothing ident False
   }
 
 -- Replace any occurrences of identifier applied to @n@ arguments with the
@@ -259,8 +282,8 @@ sawCorePreludeSpecialTreatmentMap configuration =
   [ ("PairType",  mapsTo sawDefinitionsModule "PairType")
   , ("PairValue", mapsTo sawDefinitionsModule "PairValue")
   , ("Pair__rec", mapsTo sawDefinitionsModule "Pair__rec")
-  , ("fst",       mapsTo sawDefinitionsModule "fst")
-  , ("snd",       mapsTo sawDefinitionsModule "snd")
+  , ("fst",       replaceDropArgs 2 $ Coq.Var "fst")
+  , ("snd",       replaceDropArgs 2 $ Coq.Var "snd")
   ]
 
   -- Equality
@@ -425,8 +448,8 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("LRT_Nil",              mapsTo compMModule "LRT_Nil")
   , ("lrtPi",                mapsTo compMModule "lrtPi")
   , ("lrtTupleType",         mapsTo compMModule "lrtTupleType")
-  , ("multiFixM",            mapsTo compMModule "multiFixM")
-  , ("letRecM",              mapsTo compMModule "letRecM")
+  , ("multiFixM",            mapsToExpl compMModule "multiFixM")
+  , ("letRecM",              mapsToExpl compMModule "letRecM")
   ]
 
   -- Dependent pairs