Add simple arithmetic solving to Index size solver

ChangeLog.md

@@ -4,6 +4,8 @@
 
 * Allow `@parameter`s to be used as network sizes.
 
+* More powerful index solver: `i` is now a valid index for vectors of size `n + 1 + i`.
+
 ## Version 0.11.1
 
 * Fixed bug properties involving the comparison of abstract `Index` values would throw

vehicle/src/Vehicle/Compile/Context/Free.hs

@@ -1,6 +1,7 @@
 module Vehicle.Compile.Context.Free
   ( module X,
     addDeclToContext,
+    mkDeclCtxEntry,
   )
 where
 
@@ -9,6 +10,12 @@ import Vehicle.Compile.Context.Free.Core as X
 import Vehicle.Compile.Context.Free.Instance as X
 import Vehicle.Compile.Normalise.NBE
 import Vehicle.Compile.Prelude
+import Vehicle.Data.NormalisedExpr
+
+mkDeclCtxEntry :: (MonadFreeContext builtin m) => Decl Ix builtin -> m (WHNFDecl builtin, Type Ix builtin)
+mkDeclCtxEntry decl = do
+  normDecl <- traverse normaliseInEmptyEnv decl
+  return (normDecl, typeOf decl)
 
 addDeclToContext :: (MonadFreeContext builtin m) => Decl Ix builtin -> m a -> m a
 addDeclToContext decl k = do

vehicle/src/Vehicle/Compile/ExpandResources.hs

@@ -53,12 +53,6 @@ mkFunctionDefFromResource p ident value = do
   let unnormType = Builtin mempty (BuiltinType Unit)
   (DefFunction p ident mempty VUnitType value, unnormType)
 
-addFunctionDefFromResource :: (MonadReadResources m) => Provenance -> Identifier -> WHNFValue Builtin -> m ()
-addFunctionDefFromResource p ident value = do
-  noteExplicitParameter ident value
-  let decl = mkFunctionDefFromResource p ident value
-  tell (Map.singleton ident decl)
-
 -- | Goes through the program finding all
 -- the resources, comparing the data against the type in the spec, and making
 -- note of the values for implicit parameters.
@@ -68,38 +62,48 @@ readResourcesInProg (Main ds) = Main <$> readResourcesInDecls ds
 readResourcesInDecls :: (MonadReadResources m) => [Decl Ix Builtin] -> m [Decl Ix Builtin]
 readResourcesInDecls = \case
   [] -> return []
-  decl : decls -> addDeclToContext decl $ do
-    maybeDecl <- case decl of
-      DefFunction {} -> return $ Just decl
+  decl : decls -> do
+    (newDecl, newDeclEntry) <- case decl of
+      DefFunction {} -> do
+        entry <- mkDeclCtxEntry decl
+        return (Just decl, entry)
       DefAbstract p ident defType declType -> do
         normalisedType <- normaliseInEmptyEnv declType
         let gluedType = Glued declType normalisedType
         case defType of
+          PostulateDef -> do
+            entry <- mkDeclCtxEntry decl
+            return (Just decl, entry)
           ParameterDef sort -> case sort of
             Inferable -> do
+              entry <- mkDeclCtxEntry decl
               noteInferableParameter p ident
-              return Nothing
+              return (Nothing, entry)
             NonInferable -> do
               parameterValues <- asks parameters
               parameterExpr <- parseParameterValue parameterValues (ident, p) gluedType
-              addFunctionDefFromResource p ident parameterExpr
-              return Nothing
+              let newDeclEntry = mkFunctionDefFromResource p ident parameterExpr
+              tell (Map.singleton ident newDeclEntry)
+              return (Nothing, newDeclEntry)
           DatasetDef -> do
             datasetLocations <- asks datasets
             datasetExpr <- parseDataset datasetLocations (ident, p) gluedType
-            addFunctionDefFromResource p ident datasetExpr
-            return Nothing
+            let newDeclEntry = mkFunctionDefFromResource p ident datasetExpr
+            tell (Map.singleton ident newDeclEntry)
+            return (Nothing, newDeclEntry)
           NetworkDef -> do
             networkLocations <- asks networks
             networkDetails <- checkNetwork networkLocations (ident, p) gluedType
             addNetworkType ident networkDetails
             tell (Map.singleton ident (DefAbstract p ident defType normalisedType, declType))
-            return Nothing
-          PostulateDef ->
-            return (Just decl)
+            entry <- mkDeclCtxEntry decl
+            return (Nothing, entry)
+
+    decls' <-
+      addDeclEntryToContext newDeclEntry $
+        readResourcesInDecls decls
 
-    decls' <- readResourcesInDecls decls
-    return $ maybeToList maybeDecl <> decls'
+    return $ maybeToList newDecl <> decls'
 
 checkForUnusedResources ::
   (MonadLogger m) =>

vehicle/src/Vehicle/Compile/Type/Constraint/IndexSolver.hs

@@ -14,6 +14,7 @@ import Vehicle.Data.BuiltinInterface
 import Vehicle.Data.BuiltinInterface.Expr
 import Vehicle.Data.BuiltinInterface.Value
 import Vehicle.Data.NormalisedExpr
+import Vehicle.Syntax.Builtin
 
 solveIndexConstraint ::
   forall builtin m.
@@ -53,15 +54,17 @@ solveInDomain c [value, typ] = case typ of
   VNatType {} -> return Nothing
   VIntType {} -> return Nothing
   VRatType {} -> return Nothing
-  VIndexType size -> case size of
-    (getNMeta -> Just {}) -> return $ blockOnMetas [size]
-    VNatLiteral m -> case value of
-      (getNMeta -> Just {}) -> return $ blockOnMetas [value]
-      VNatLiteral n
-        | m > n -> return Nothing
-        | otherwise -> throwError $ TypingError $ FailedIndexConstraintTooBig ctx n m
-      _ -> malformedConstraintError c
-    _ -> throwError $ TypingError $ FailedIndexConstraintUnknown ctx value size
+  VIndexType size -> case value of
+    VMeta {} -> return $ blockOnMetas [value]
+    VNatLiteral n -> do
+      (sizeBlockingMetas, sizeLowerBound) <- findLowerBound ctx value size
+      if n < sizeLowerBound
+        then return Nothing
+        else
+          if not (MetaSet.null sizeBlockingMetas)
+            then return $ Just sizeBlockingMetas
+            else throwError $ TypingError $ FailedIndexConstraintTooBig ctx n sizeLowerBound
+    _ -> malformedConstraintError c
   _ -> malformedConstraintError c
   where
     ctx = contextOf c
@@ -73,3 +76,26 @@ blockOnMetas args = do
   if null metas
     then Nothing
     else Just (MetaSet.fromList metas)
+
+findLowerBound ::
+  forall m builtin.
+  (TCM builtin m, HasStandardData builtin) =>
+  ConstraintContext builtin ->
+  WHNFType builtin ->
+  WHNFType builtin ->
+  m (MetaSet, Int)
+findLowerBound ctx value indexSize = go indexSize
+  where
+    go :: WHNFType builtin -> m (MetaSet, Int)
+    go = \case
+      VMeta m _ ->
+        return (MetaSet.singleton m, 0)
+      VNatLiteral n ->
+        return (mempty, n)
+      VFreeVar {} ->
+        return (mempty, 0)
+      VAdd AddNat e1 e2 -> do
+        (m1, b1) <- go e1
+        (m2, b2) <- go e2
+        return (m1 <> m2, b1 + b2)
+      _ -> throwError $ TypingError $ FailedIndexConstraintUnknown ctx value indexSize

vehicle/tests/golden/compile/issue770/spec.vcl

@@ -0,0 +1,9 @@
+@parameter
+n : Nat
+
+@network
+f : Vector Rat 1 -> Vector Rat (n + 1)
+
+@property
+p : Bool
+p = f [0] ! 0 >= 0

vehicle/tests/golden/compile/issue770/test.json

@@ -0,0 +1,8 @@
+{
+  "name": "MarabouQueries",
+  "run": "vehicle check -s spec.vcl",
+  "needs": [
+    "spec.vcl"
+  ],
+  "produces": []
+}