Merge pull request #4381 from unisonweb/cp/pull-hash-validation-types

Add decl verification

codebase2/codebase-sqlite-hashing-v2/package.yaml

@@ -20,6 +20,7 @@ dependencies:
   - unison-hashing-v2
   - unison-prelude
   - unison-sqlite
+  - unison-syntax
   - unison-util-base32hex
   - unison-util-term
   - vector

codebase2/codebase-sqlite-hashing-v2/src/U/Codebase/Decl/Hashing.hs

@@ -0,0 +1,54 @@
+module U.Codebase.Decl.Hashing where
+
+import Control.Lens
+import Data.Foldable qualified as Foldable
+import Data.Map qualified as Map
+import U.Codebase.Decl qualified as C
+import U.Codebase.Decl qualified as C.Decl
+import U.Codebase.HashTags
+import U.Codebase.Reference qualified as Reference
+import U.Codebase.Sqlite.Decl.Format qualified as DeclFormat
+import U.Codebase.Sqlite.HashHandle (HashMismatch (..))
+import U.Codebase.Sqlite.HashHandle qualified as HH
+import U.Codebase.Sqlite.LocalIds qualified as LocalIds
+import U.Codebase.Sqlite.Queries qualified as Q
+import U.Codebase.Sqlite.Symbol qualified as S
+import U.Codebase.Sqlite.Symbol qualified as Sqlite
+import Unison.Hash32
+import Unison.Hash32 qualified as Hash32
+import Unison.Hashing.V2 qualified as H2
+import Unison.Hashing.V2.Convert2 qualified as H2
+import Unison.Prelude
+import Unison.Symbol qualified as Unison
+import Unison.Syntax.Name qualified as Name
+import Unison.Var qualified as Var
+
+verifyDeclFormatHash :: ComponentHash -> DeclFormat.HashDeclFormat -> Maybe HH.DeclHashingError
+verifyDeclFormatHash (ComponentHash hash) (DeclFormat.Decl (DeclFormat.LocallyIndexedComponent elements)) =
+  Foldable.toList elements
+    & fmap s2cDecl
+    & Reference.component hash
+    & fmap (\(decl, refId) -> (refId, (C.Decl.vmap symbol2to1 decl, ())))
+    & Map.fromList
+    & C.Decl.unhashComponent hash Var.unnamedRef
+    & Map.toList
+    & fmap (\(_refId, (v, decl, ())) -> (v, either H2.toDataDecl id $ H2.v2ToH2Decl decl))
+    & Map.fromList
+    & H2.hashDecls Name.unsafeFromVar
+    & \case
+      Left _err -> Just HH.DeclHashResolutionFailure
+      Right m ->
+        m
+          & altMap \(_, H2.ReferenceId hash' _, _) ->
+            if hash == hash'
+              then Nothing
+              else Just (HH.DeclHashMismatch $ HashMismatch hash hash')
+  where
+    symbol2to1 :: S.Symbol -> Unison.Symbol
+    symbol2to1 (S.Symbol i t) = Unison.Symbol i (Var.User t)
+
+s2cDecl :: (LocalIds.LocalIds' Text Hash32, DeclFormat.Decl Sqlite.Symbol) -> C.Decl Sqlite.Symbol
+s2cDecl (ids, decl) =
+  let Identity (substText, substHash) = Q.localIdsToLookups Identity pure (bimap id Hash32.toHash ids)
+      refmap = (bimap substText (fmap substHash))
+   in Q.x2cDecl refmap decl

codebase2/codebase-sqlite-hashing-v2/src/U/Codebase/Sqlite/V2/HashHandle.hs

@@ -7,13 +7,15 @@ import Data.Function ((&))
 import Data.Set qualified as Set
 import U.Codebase.Branch.Hashing qualified as H2
 import U.Codebase.Causal.Hashing qualified as H2
-import U.Codebase.HashTags (BranchHash (..))
+import U.Codebase.Decl.Hashing qualified as H2
+import U.Codebase.HashTags (BranchHash (..), PatchHash (..))
 import U.Codebase.Sqlite.Branch.Format qualified as BranchFormat
 import U.Codebase.Sqlite.HashHandle
+import U.Codebase.Sqlite.Patch.Format qualified as PatchFormat
 import U.Codebase.Term.Hashing as H2
 import U.Util.Type (removeAllEffectVars)
 import Unison.Hashing.V2 qualified as H2
-import Unison.Hashing.V2.Convert2 (h2ToV2Reference, hashBranchFormatToH2Branch, v2ToH2Type, v2ToH2TypeD)
+import Unison.Hashing.V2.Convert2 (h2ToV2Reference, hashBranchFormatToH2Branch, hashPatchFormatToH2Patch, v2ToH2Type, v2ToH2TypeD)
 
 v2HashHandle :: HashHandle
 v2HashHandle =
@@ -25,10 +27,19 @@ v2HashHandle =
       hashBranch = H2.hashBranch,
       hashBranchV3 = H2.hashBranchV3,
       hashCausal = H2.hashCausal,
-      hashBranchFormatFull = \localIds localBranch ->
-        BranchFormat.localToHashBranch localIds localBranch
-          & hashBranchFormatToH2Branch
-          & H2.contentHash
-          & BranchHash,
-      verifyTermFormatHash = H2.verifyTermFormatHash
+      hashBranchFormatFull,
+      hashPatchFormatFull,
+      verifyTermFormatHash = H2.verifyTermFormatHash,
+      verifyDeclFormatHash = H2.verifyDeclFormatHash
     }
+  where
+    hashBranchFormatFull localIds localBranch =
+      BranchFormat.localToHashBranch localIds localBranch
+        & hashBranchFormatToH2Branch
+        & H2.contentHash
+        & BranchHash
+    hashPatchFormatFull localIds localPatch =
+      PatchFormat.localPatchToHashPatch localIds localPatch
+        & hashPatchFormatToH2Patch
+        & H2.contentHash
+        & PatchHash

codebase2/codebase-sqlite-hashing-v2/src/Unison/Hashing/V2/Convert2.hs

@@ -6,22 +6,29 @@ module Unison.Hashing.V2.Convert2
     h2ToV2Reference,
     v2ToH2Branch,
     v2ToH2Term,
+    v2ToH2Decl,
     hashBranchFormatToH2Branch,
+    hashPatchFormatToH2Patch,
   )
 where
 
 import Data.Map qualified as Map
 import Data.Set qualified as Set
+import Data.Text qualified as Text
 import U.Codebase.Branch qualified as V2
 import U.Codebase.Branch qualified as V2Branch
 import U.Codebase.BranchV3 (BranchV3 (..))
 import U.Codebase.Causal qualified as Causal
+import U.Codebase.Decl qualified as V2.Decl
 import U.Codebase.HashTags
 import U.Codebase.Kind qualified as V2
 import U.Codebase.Reference qualified as V2
 import U.Codebase.Reference qualified as V2Reference
 import U.Codebase.Referent qualified as V2Referent
 import U.Codebase.Sqlite.Branch.Full qualified as Memory.BranchFull
+import U.Codebase.Sqlite.Patch.Full qualified as Memory.PatchFull
+import U.Codebase.Sqlite.Patch.TermEdit qualified as Memory.TermEdit
+import U.Codebase.Sqlite.Patch.TypeEdit qualified as Memory.TypeEdit
 import U.Codebase.Term qualified as V2 (TypeRef)
 import U.Codebase.Term qualified as V2.Term
 import U.Codebase.Type qualified as V2.Type
@@ -30,6 +37,7 @@ import Unison.Hash (Hash)
 import Unison.Hashing.V2 qualified as H2
 import Unison.NameSegment (NameSegment (..))
 import Unison.Prelude
+import Unison.Symbol qualified as Unison
 import Unison.Util.Map qualified as Map
 
 -- | Convert a V3 branch to a hashing branch.
@@ -135,6 +143,29 @@ hashBranchFormatToH2Branch Memory.BranchFull.Branch {terms, types, patches, chil
       V2Referent.Con typeRef conId -> do
         (H2.ReferentCon (v2ToH2Reference $ second unComponentHash typeRef) conId)
 
+hashPatchFormatToH2Patch :: Memory.PatchFull.HashPatch -> H2.Patch
+hashPatchFormatToH2Patch Memory.PatchFull.Patch {termEdits, typeEdits} =
+  H2.Patch
+    { termEdits = Map.bimap cvreferent (Set.map cvTermEdit) termEdits,
+      typeEdits = Map.bimap cvreference (Set.map cvTypeEdit) typeEdits
+    }
+  where
+    cvTermEdit :: Memory.TermEdit.HashTermEdit -> H2.TermEdit
+    cvTermEdit = \case
+      Memory.TermEdit.Replace ref _typing -> H2.TermEditReplace (v2ToH2Referent . coerce $ ref)
+      Memory.TermEdit.Deprecate -> H2.TermEditDeprecate
+    cvTypeEdit :: Memory.TypeEdit.HashTypeEdit -> H2.TypeEdit
+    cvTypeEdit = \case
+      Memory.TypeEdit.Replace ref -> H2.TypeEditReplace (v2ToH2Reference . coerce $ ref)
+      Memory.TypeEdit.Deprecate -> H2.TypeEditDeprecate
+    cvreference :: V2Reference.Reference' Text ComponentHash -> H2.Reference
+    cvreference = v2ToH2Reference . second unComponentHash
+    cvreferent :: Memory.BranchFull.Referent'' Text ComponentHash -> H2.Referent
+    cvreferent = \case
+      V2Referent.Ref ref -> (H2.ReferentRef (v2ToH2Reference $ second unComponentHash ref))
+      V2Referent.Con typeRef conId -> do
+        (H2.ReferentCon (v2ToH2Reference $ second unComponentHash typeRef) conId)
+
 v2ToH2Term :: forall v. Ord v => V2.Term.HashableTerm v -> H2.Term v ()
 v2ToH2Term = ABT.transform convertF
   where
@@ -189,3 +220,27 @@ v2ToH2Term = ABT.transform convertF
       V2.Term.PCons -> H2.Cons
       V2.Term.PSnoc -> H2.Snoc
       V2.Term.PConcat -> H2.Concat
+
+v2ToH2Decl :: V2.Decl.HashableDecl Unison.Symbol -> H2.Decl Unison.Symbol ()
+v2ToH2Decl (V2.Decl.DataDeclaration {declType, modifier, bound, constructorTypes}) =
+  let tag = case declType of
+        V2.Decl.Effect -> Left . H2.EffectDeclaration
+        V2.Decl.Data -> Right
+   in tag $
+        H2.DataDeclaration
+          { modifier = v2ToH2Modifier modifier,
+            annotation = (),
+            bound = bound,
+            constructors' =
+              constructorTypes
+                & zip [0 ..]
+                & fmap mkCtor
+          }
+  where
+    mkCtor :: (Int, V2.Type.TypeR V2.Decl.HashableTypeRef Unison.Symbol) -> ((), Unison.Symbol, H2.Type Unison.Symbol ())
+    mkCtor (n, t) = ((), Unison.symbol . Text.pack $ "Constructor" ++ show n, v2ToH2Type t)
+
+    v2ToH2Modifier :: V2.Decl.Modifier -> H2.Modifier
+    v2ToH2Modifier = \case
+      V2.Decl.Structural -> H2.Structural
+      V2.Decl.Unique t -> H2.Unique t

codebase2/codebase-sqlite-hashing-v2/unison-codebase-sqlite-hashing-v2.cabal

@@ -21,6 +21,7 @@ library
   other-modules:
       U.Codebase.Branch.Hashing
       U.Codebase.Causal.Hashing
+      U.Codebase.Decl.Hashing
       U.Codebase.Term.Hashing
       Unison.Hashing.V2.Convert2
   hs-source-dirs:
@@ -69,6 +70,7 @@ library
     , unison-hashing-v2
     , unison-prelude
     , unison-sqlite
+    , unison-syntax
     , unison-util-base32hex
     , unison-util-term
     , vector

codebase2/codebase-sqlite/U/Codebase/Sqlite/Decl/Format.hs

@@ -10,12 +10,18 @@ import U.Codebase.Sqlite.LocalIds (LocalDefnId, LocalIds', LocalTextId)
 import U.Codebase.Sqlite.Symbol (Symbol)
 import U.Codebase.Type qualified as Type
 import U.Core.ABT qualified as ABT
+import Unison.Hash32 (Hash32)
 import Unison.Prelude
 
 -- | Add new formats here
-data DeclFormat = Decl LocallyIndexedComponent
+data DeclFormat' text defn = Decl (LocallyIndexedComponent' text defn)
   deriving (Show)
 
+type DeclFormat = DeclFormat' TextId ObjectId
+
+-- | A DeclFormat which uses hash references instead of database ids.
+type HashDeclFormat = DeclFormat' Text Hash32
+
 -- | V1: Decls included `Hash`es inline
 --   V2: Instead of `Hash`, we use a smaller index.
 type LocallyIndexedComponent =

codebase2/codebase-sqlite/U/Codebase/Sqlite/HashHandle.hs

@@ -1,6 +1,7 @@
 module U.Codebase.Sqlite.HashHandle
   ( HashHandle (..),
     HashMismatch (..),
+    DeclHashingError (..),
   )
 where
 
@@ -10,6 +11,9 @@ import U.Codebase.HashTags
 import U.Codebase.Reference qualified as C
 import U.Codebase.Sqlite.Branch.Format (HashBranchLocalIds)
 import U.Codebase.Sqlite.Branch.Full (LocalBranch)
+import U.Codebase.Sqlite.Decl.Format qualified as DeclFormat
+import U.Codebase.Sqlite.Patch.Format (HashPatchLocalIds)
+import U.Codebase.Sqlite.Patch.Full (LocalPatch)
 import U.Codebase.Sqlite.Symbol (Symbol)
 import U.Codebase.Sqlite.Term.Format qualified as TermFormat
 import U.Codebase.Term qualified as C.Term
@@ -22,6 +26,10 @@ data HashMismatch = HashMismatch
     actualHash :: Hash
   }
 
+data DeclHashingError
+  = DeclHashMismatch HashMismatch
+  | DeclHashResolutionFailure
+
 data HashHandle = HashHandle
   { -- | Hash type
     toReference :: C.Term.Type Symbol -> C.Reference,
@@ -43,5 +51,16 @@ data HashHandle = HashHandle
       HashBranchLocalIds ->
       LocalBranch ->
       BranchHash,
-    verifyTermFormatHash :: ComponentHash -> TermFormat.HashTermFormat -> Maybe (HashMismatch)
+    hashPatchFormatFull ::
+      HashPatchLocalIds ->
+      LocalPatch ->
+      PatchHash,
+    verifyTermFormatHash ::
+      ComponentHash ->
+      TermFormat.HashTermFormat ->
+      Maybe (HashMismatch),
+    verifyDeclFormatHash ::
+      ComponentHash ->
+      DeclFormat.HashDeclFormat ->
+      Maybe DeclHashingError
   }

codebase2/codebase-sqlite/U/Codebase/Sqlite/Patch/Format.hs

@@ -2,23 +2,26 @@ module U.Codebase.Sqlite.Patch.Format
   ( PatchFormat (..),
     PatchLocalIds,
     PatchLocalIds' (..),
+    HashPatchLocalIds,
     SyncPatchFormat,
     SyncPatchFormat' (..),
     applyPatchDiffs,
     localPatchToPatch,
     localPatchDiffToPatchDiff,
+    localPatchToHashPatch,
   )
 where
 
 import Data.Map.Strict qualified as Map
 import Data.Set qualified as Set
 import Data.Vector (Vector)
 import Data.Vector qualified as Vector
+import U.Codebase.HashTags
 import U.Codebase.Sqlite.DbId (HashId, ObjectId, PatchObjectId, TextId)
 import U.Codebase.Sqlite.LocalIds (LocalDefnId (LocalDefnId), LocalHashId (LocalHashId), LocalTextId (LocalTextId))
 import U.Codebase.Sqlite.Patch.Diff (LocalPatchDiff, PatchDiff, PatchDiff' (..))
 import U.Codebase.Sqlite.Patch.Diff qualified as Patch.Diff
-import U.Codebase.Sqlite.Patch.Full (LocalPatch, Patch, Patch' (..))
+import U.Codebase.Sqlite.Patch.Full (HashPatch, LocalPatch, Patch, Patch' (..))
 import U.Codebase.Sqlite.Patch.Full qualified as Patch.Full
 import Unison.Prelude
 
@@ -28,6 +31,9 @@ data PatchFormat
 
 type PatchLocalIds = PatchLocalIds' TextId HashId ObjectId
 
+-- | LocalIds type which can be used in hashing the Patch.
+type HashPatchLocalIds = PatchLocalIds' Text ComponentHash ComponentHash
+
 data PatchLocalIds' t h d = LocalIds
   { patchTextLookup :: Vector t,
     patchHashLookup :: Vector h,
@@ -64,22 +70,29 @@ applyPatchDiffs =
       let diff = Set.difference src del
        in if Set.null diff then Nothing else Just diff
 
-localPatchToPatch :: PatchLocalIds -> LocalPatch -> Patch
-localPatchToPatch li =
+localToPatch' :: (Ord t, Ord h, Ord d) => PatchLocalIds' t h d -> (Patch' LocalTextId LocalHashId LocalDefnId) -> Patch' t h d
+localToPatch' li =
   Patch.Full.trimap (lookupPatchLocalText li) (lookupPatchLocalHash li) (lookupPatchLocalDefn li)
 
+-- | Type specialized version of `localToPatch'`.
+localPatchToPatch :: PatchLocalIds -> LocalPatch -> Patch
+localPatchToPatch = localToPatch'
+
+localPatchToHashPatch :: HashPatchLocalIds -> LocalPatch -> HashPatch
+localPatchToHashPatch = localToPatch'
+
 localPatchDiffToPatchDiff :: PatchLocalIds -> LocalPatchDiff -> PatchDiff
 localPatchDiffToPatchDiff li =
   Patch.Diff.trimap
     (lookupPatchLocalText li)
     (lookupPatchLocalHash li)
     (lookupPatchLocalDefn li)
 
-lookupPatchLocalText :: PatchLocalIds -> LocalTextId -> TextId
+lookupPatchLocalText :: PatchLocalIds' t h d -> LocalTextId -> t
 lookupPatchLocalText li (LocalTextId w) = patchTextLookup li Vector.! fromIntegral w
 
-lookupPatchLocalHash :: PatchLocalIds -> LocalHashId -> HashId
+lookupPatchLocalHash :: PatchLocalIds' t h d -> LocalHashId -> h
 lookupPatchLocalHash li (LocalHashId w) = patchHashLookup li Vector.! fromIntegral w
 
-lookupPatchLocalDefn :: PatchLocalIds -> LocalDefnId -> ObjectId
+lookupPatchLocalDefn :: PatchLocalIds' t h d -> LocalDefnId -> d
 lookupPatchLocalDefn li (LocalDefnId w) = patchDefnLookup li Vector.! fromIntegral w

codebase2/codebase-sqlite/U/Codebase/Sqlite/Patch/Full.hs

@@ -4,6 +4,8 @@ import Control.Lens
 import Data.Map (Map)
 import Data.Set (Set)
 import Data.Set qualified as Set
+import Data.Text (Text)
+import U.Codebase.HashTags
 import U.Codebase.Reference (Reference')
 import U.Codebase.Reference qualified as Reference
 import U.Codebase.Referent (Referent')
@@ -26,6 +28,9 @@ import Unison.Util.Set qualified as Set
 -- @
 type Patch = Patch' Db.TextId Db.HashId Db.ObjectId
 
+-- | A version of Patch' which can be used for hashing.
+type HashPatch = Patch' Text ComponentHash ComponentHash
+
 -- |
 -- @
 -- LocalPatch

codebase2/codebase-sqlite/U/Codebase/Sqlite/Patch/TermEdit.hs

@@ -3,6 +3,8 @@ module U.Codebase.Sqlite.Patch.TermEdit where
 import Control.Lens
 import Data.Bifoldable (Bifoldable (bifoldMap))
 import Data.Bitraversable (Bitraversable (bitraverse))
+import Data.Text (Text)
+import U.Codebase.HashTags
 import U.Codebase.Reference (Reference')
 import U.Codebase.Reference qualified as Reference
 import U.Codebase.Referent qualified as Referent
@@ -11,6 +13,8 @@ import U.Codebase.Sqlite.LocalIds (LocalDefnId, LocalTextId)
 
 type TermEdit = TermEdit' Db.TextId Db.ObjectId
 
+type HashTermEdit = TermEdit' Text ComponentHash
+
 type LocalTermEdit = TermEdit' LocalTextId LocalDefnId
 
 type Referent' t h = Referent.Referent' (Reference' t h) (Reference' t h)