add proper BlameVerCors explanations to col

src/col/vct/col/failure/BlameVerCorsReasons.scala

@@ -0,0 +1,42 @@
+package vct.col.failure
+
+import vct.col.ast.{Blame1, BlameVerCors}
+import vct.col.origin.Origin
+
+object BlameVerCorsReasons {
+  implicit object VerCorsBlameOrigin extends Origin {
+    override def preferredName: String = "unknown"
+    override def context: String = "At: [generated]"
+    override def inlineContext: String = "[generated]"
+    override def shortPosition: String = "generated"
+  }
+
+  private def blame[G](reason: String): Blame1[G] = Blame1(BlameVerCors(reason), Nil)
+
+  object Structure {
+    def AssignLocal[G]: Blame1[G] = blame("Assigning to a local is infallible.")
+    def AssignField[G]: Blame1[G] = blame(
+      "Dereferences that are the target of an assignment must not fail. " +
+      "Instead, the assignment itself must fail."
+    )
+    def Trigger[G]: Blame1[G] = blame("Expressions in a trigger are not evaluated, and thus infallible.")
+  }
+
+  object Contract {
+    def TrueIsSatisfiable[G]: Blame1[G] = blame("The constant `true` is always satisfiable.")
+  }
+
+  object Applicable {
+    def PreIsTrue[G]: Blame1[G] = blame("The precondition `true` always holds.")
+    def PostIsTrue[G]: Blame1[G] = blame("The postcondition `true` always holds.")
+    def PostOfAbstract[G]: Blame1[G] = blame("The postcondition of an abstract applicable is not checked.")
+  }
+
+  object WellFormedness {
+    def OptNotEmpty[G]: Blame1[G] = blame("The path condition ensures this option cannot be empty.")
+    def EitherNotLeft[G]: Blame1[G] = blame("The path condition ensures this either cannot be left.")
+    def EitherNotRight[G]: Blame1[G] = blame("The path condition ensures this either cannot be right.")
+    def SeqBound[G]: Blame1[G] = blame("The path condition ensures this subscript cannot be out of bounds.")
+    def MapContains[G]: Blame1[G] = blame("The path condition ensures this key is in the map.")
+  }
+}

src/col/vct/col/resolve/lang/Java.scala

@@ -3,7 +3,7 @@ package vct.col.resolve.lang
 import com.typesafe.scalalogging.LazyLogging
 import vct.col.ast.lang.JavaAnnotationEx
 import vct.col.ast.`type`.TFloats
-import vct.col.ast.{BlameVerCors, ADTFunction, ApplicableContract, AxiomaticDataType, BipPortType, Blame1, Block, CType, EmptyProcess, Expr, JavaAnnotation, JavaAnnotationInterface, JavaClass, JavaClassDeclaration, JavaClassOrInterface, JavaConstructor, JavaFields, JavaFinal, JavaImport, JavaInterface, JavaMethod, JavaName, JavaNamedType, JavaNamespace, JavaParam, JavaStatic, JavaTClass, JavaType, JavaVariableDeclaration, LiteralBag, LiteralMap, LiteralSeq, LiteralSet, Node, Null, OptNone, PVLType, TAny, TAnyClass, TArray, TAxiomatic, TBag, TBool, TBoundedInt, TChar, TClass, TEither, TEnum, TFloat, TFraction, TInt, TMap, TMatrix, TModel, TNotAValue, TNothing, TNull, TOption, TPointer, TProcess, TProverType, TRational, TRef, TResource, TSeq, TSet, TString, TTuple, TType, TUnion, TVar, TVoid, TZFraction, Type, UnitAccountedPredicate, Variable, Void}
+import vct.col.ast.{ADTFunction, ApplicableContract, AxiomaticDataType, BipPortType, Blame1, BlameVerCors, Block, CType, EmptyProcess, Expr, JavaAnnotation, JavaAnnotationInterface, JavaClass, JavaClassDeclaration, JavaClassOrInterface, JavaConstructor, JavaFields, JavaFinal, JavaImport, JavaInterface, JavaMethod, JavaName, JavaNamedType, JavaNamespace, JavaParam, JavaStatic, JavaTClass, JavaType, JavaVariableDeclaration, LiteralBag, LiteralMap, LiteralSeq, LiteralSet, Node, Null, OptNone, PVLType, TAny, TAnyClass, TArray, TAxiomatic, TBag, TBool, TBoundedInt, TChar, TClass, TEither, TEnum, TFloat, TFraction, TInt, TMap, TMatrix, TModel, TNotAValue, TNothing, TNull, TOption, TPointer, TProcess, TProverType, TRational, TRef, TResource, TSeq, TSet, TString, TTuple, TType, TUnion, TVar, TVoid, TZFraction, Type, UnitAccountedPredicate, Variable, Void}
 import vct.col.origin._
 import vct.col.ref.Ref
 import vct.col.resolve.ResolveTypes.JavaClassPathEntry
@@ -20,6 +20,9 @@ import java.io.File
 import java.lang.reflect.{Modifier, Parameter}
 import java.nio.file.Path
 import hre.util.FuncTools
+import vct.col.failure.BlameVerCorsReasons.Applicable.PostOfAbstract
+import vct.col.failure.BlameVerCorsReasons.Contract.TrueIsSatisfiable
+
 import scala.collection.mutable
 import scala.annotation.tailrec
 
@@ -147,8 +150,8 @@ case object Java extends LazyLogging {
         typeParameters = Nil,
         signals = Nil,
         body = Block(Nil),
-        contract = ApplicableContract(UnitAccountedPredicate(tt), UnitAccountedPredicate(tt), tt, Nil, Nil, Nil, None, Blame1(BlameVerCors("?"), Nil)),
-        blame = Blame1(BlameVerCors("?"), Nil),
+        contract = ApplicableContract(UnitAccountedPredicate(tt), UnitAccountedPredicate(tt), tt, Nil, Nil, Nil, None, TrueIsSatisfiable),
+        blame = PostOfAbstract,
       )(SourceNameOrigin(cls.getSimpleName, o))
     })
 
@@ -162,8 +165,8 @@ case object Java extends LazyLogging {
         typeParameters = Nil,
         signals = Nil,
         body = None,
-        contract = ApplicableContract(UnitAccountedPredicate(tt), UnitAccountedPredicate(tt), tt, Nil, Nil, Nil, None, Blame1(BlameVerCors("?"), Nil)),
-        blame = Blame1(BlameVerCors("?"), Nil),
+        contract = ApplicableContract(UnitAccountedPredicate(tt), UnitAccountedPredicate(tt), tt, Nil, Nil, Nil, None, TrueIsSatisfiable),
+        blame = PostOfAbstract,
       )(SourceNameOrigin(method.getName, o))
     })
 

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -4,6 +4,10 @@ import com.typesafe.scalalogging.LazyLogging
 import hre.util.FuncTools
 import vct.col.ast._
 import vct.col.ast.`type`.TFloats
+import vct.col.failure.BlameVerCorsReasons.Applicable.{PostOfAbstract, PreIsTrue}
+import vct.col.failure.BlameVerCorsReasons.Contract.TrueIsSatisfiable
+import vct.col.failure.BlameVerCorsReasons.Structure.Trigger
+import vct.col.failure.BlameVerCorsReasons.WellFormedness.{EitherNotLeft, EitherNotRight, MapContains, OptNotEmpty, SeqBound}
 import vct.col.origin._
 import vct.col.ref.Ref
 import vct.col.rewrite.{Generation, Rewritten}
@@ -68,22 +72,22 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
       case CoerceNothingSomething(_) => e
       case CoerceSomethingAny(_) => e
       case CoerceMapOption(inner, _, target) =>
-        Select(OptEmpty(e), OptNoneTyped(dispatch(target)), OptSomeTyped(dispatch(target), applyCoercion(OptGet(e, Blame1(BlameVerCors("?"), Nil)), inner)))
+        Select(OptEmpty(e), OptNoneTyped(dispatch(target)), OptSomeTyped(dispatch(target), applyCoercion(OptGet(e, OptNotEmpty), inner)))
       case CoerceMapEither((innerLeft, innerRight), _, _) =>
         Select(IsRight(e),
-          EitherRight(applyCoercion(GetRight(e, Blame1(BlameVerCors("?"), Nil)), innerRight)),
-          EitherLeft(applyCoercion(GetLeft(e, Blame1(BlameVerCors("?"), Nil)), innerLeft)),
+          EitherRight(applyCoercion(GetRight(e, EitherNotLeft), innerRight)),
+          EitherLeft(applyCoercion(GetLeft(e, EitherNotRight), innerLeft)),
         )
       case CoerceMapSeq(inner, source, target) =>
         val f: Function[Post] = withResult((result: Result[Post]) => {
           val v = new Variable[Post](TSeq(dispatch(source)))
           val i = new Variable[Post](TInt())
-          val result_i = SeqSubscript(result, i.get, Blame1(BlameVerCors("?"), Nil))
-          val v_i = SeqSubscript(v.get, i.get, Blame1(BlameVerCors("?"), Nil))
+          val result_i = SeqSubscript(result, i.get, SeqBound)
+          val v_i = SeqSubscript(v.get, i.get, SeqBound)
 
           function(
-            blame = Blame1(BlameVerCors("?"), Nil),
-            contractBlame = Blame1(BlameVerCors("?"), Nil),
+            blame = PostOfAbstract,
+            contractBlame = TrueIsSatisfiable,
             returnType = TSeq(dispatch(target)),
             args = Seq(v),
             ensures = UnitAccountedPredicate(
@@ -96,15 +100,15 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
         })
 
         globalDeclarations.declare(f)
-        FunctionInvocation[Post](f.ref, Seq(e), Nil, Nil, Nil, Blame1(BlameVerCors("?"), Nil))
+        FunctionInvocation[Post](f.ref, Seq(e), Nil, Nil, Nil, PreIsTrue)
       case CoerceMapSet(inner, source, target) =>
         val f: Function[Post] = withResult((result: Result[Post]) => {
           val v = new Variable(TSet(dispatch(source)))
           val elem = new Variable(dispatch(source))
 
           function(
-            blame = Blame1(BlameVerCors("?"), Nil),
-            contractBlame = Blame1(BlameVerCors("?"), Nil),
+            blame = PostOfAbstract,
+            contractBlame = TrueIsSatisfiable,
             returnType = TSet(dispatch(target)),
             args = Seq(v),
             ensures = UnitAccountedPredicate(
@@ -116,15 +120,15 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
         })
 
         globalDeclarations.declare(f)
-        FunctionInvocation[Post](f.ref, Seq(e), Nil, Nil, Nil, Blame1(BlameVerCors("?"), Nil))
+        FunctionInvocation[Post](f.ref, Seq(e), Nil, Nil, Nil, PreIsTrue)
       case CoerceMapBag(inner, source, target) =>
         val f: Function[Post] = withResult((result: Result[Post]) => {
           val v = new Variable(TBag(dispatch(source)))
           val elem = new Variable(dispatch(source))
 
           function(
-            blame = Blame1(BlameVerCors("?"), Nil),
-            contractBlame = Blame1(BlameVerCors("?"), Nil),
+            blame = PostOfAbstract,
+            contractBlame = TrueIsSatisfiable,
             returnType = TBag(dispatch(target)),
             args = Seq(v),
             ensures = UnitAccountedPredicate(
@@ -136,7 +140,7 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
         })
 
         globalDeclarations.declare(f)
-        FunctionInvocation[Post](f.ref, Seq(e), Nil, Nil, Nil, Blame1(BlameVerCors("?"), Nil))
+        FunctionInvocation[Post](f.ref, Seq(e), Nil, Nil, Nil, PreIsTrue)
       case CoerceMapMatrix(inner, source, target) =>
         ???
       case CoerceMapMap(inner, (sourceKey, sourceValue), (targetKey, targetValue)) =>
@@ -145,20 +149,20 @@ abstract class CoercingRewriter[Pre <: Generation]() extends AbstractRewriter[Pr
           val k = new Variable(dispatch(sourceKey))
 
           function(
-            blame = Blame1(BlameVerCors("?"), Nil),
-            contractBlame = Blame1(BlameVerCors("?"), Nil),
+            blame = PostOfAbstract,
+            contractBlame = TrueIsSatisfiable,
             returnType = TMap(dispatch(targetKey), dispatch(targetValue)),
             args = Seq(v),
             ensures = UnitAccountedPredicate(
               Eq(MapKeySet(result), MapKeySet(v.get)) &&
-                Forall(Seq(k), Seq(Seq(MapGet(result, k.get, Blame1(BlameVerCors("?"), Nil)))),
-                  SetMember(k.get, MapKeySet(result)) ==> Eq(MapGet(result, k.get, Blame1(BlameVerCors("?"), Nil)), MapGet(v.get, k.get, Blame1(BlameVerCors("?"), Nil))))
+                Forall(Seq(k), Seq(Seq(MapGet(result, k.get, Trigger))),
+                  SetMember(k.get, MapKeySet(result)) ==> Eq(MapGet(result, k.get, MapContains), MapGet(v.get, k.get, MapContains)))
             ),
           )
         })
 
         globalDeclarations.declare(f)
-        FunctionInvocation[Post](f.ref, Seq(e), Nil, Nil, Nil, Blame1(BlameVerCors("?"), Nil))
+        FunctionInvocation[Post](f.ref, Seq(e), Nil, Nil, Nil, PreIsTrue)
       case CoerceMapTuple(inner, sourceTypes, targetTypes) =>
         LiteralTuple(targetTypes.map(dispatch), inner.zipWithIndex.map { case (c, i) => applyCoercion(TupGet(e, i), c) })
       case CoerceMapType(inner, source, target) =>

src/col/vct/col/util/AstBuildHelpers.scala

@@ -3,6 +3,7 @@ package vct.col.util
 import vct.col.ast.RewriteHelpers._
 import vct.col.ast._
 import vct.col.ast.expr.apply.FunctionInvocationImpl
+import vct.col.failure.BlameVerCorsReasons.Structure.{AssignField, AssignLocal}
 import vct.col.origin._
 import vct.col.ref.{DirectRef, Ref}
 
@@ -388,10 +389,10 @@ object AstBuildHelpers {
   }
 
   def assignLocal[G](local: Local[G], value: Expr[G])(implicit o: Origin): Assign[G] =
-    Assign(local, value, Blame1(BlameVerCors("?"), Nil))
+    Assign(local, value, AssignLocal)
 
   def assignField[G](obj: Expr[G], field: Ref[G, InstanceField[G]], value: Expr[G], blame: Blame1[G])(implicit o: Origin): Assign[G] =
-    Assign(Deref(obj, field, Blame1(BlameVerCors("?"), Nil)), value, blame)
+    Assign(Deref(obj, field, AssignField), value, blame)
 
   def fieldPerm[G](obj: Expr[G], field: Ref[G, InstanceField[G]], amount: Expr[G])(implicit o: Origin): Perm[G] =
     Perm(FieldLocation(obj, field), amount)