@@ -533,6 +533,12 @@ private Expr<?> getDefaultValueForType(CelType type) {
533533 if (type .equals (SimpleType .UINT )) {
534534 return typeSystem .mkUint (0 );
535535 }
536+ if (type .equals (SimpleType .TIMESTAMP )) {
537+ return typeSystem .wrapTimestamp (ctx .mkInt (0 ));
538+ }
539+ if (type .equals (SimpleType .DURATION )) {
540+ return typeSystem .wrapDuration (ctx .mkInt (0 ));
541+ }
536542 if (type instanceof ListType ) {
537543 if (emptyListCache == null ) {
538544 emptyListCache = typeSystem .mkListRefConst (EMPTY_LIST_PREFIX );
@@ -735,8 +741,10 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
735741 typeConstraints .add (ctx .mkNot (typeSystem .isUnknown (callRes )));
736742 typeConstraints .add (ctx .mkNot (typeSystem .isError (callRes )));
737743
744+ boolean isDynamic = ast .getType (exprId ).map (SimpleType .DYN ::equals ).orElse (true );
745+ BoolExpr isApprox = ctx .mkBool (!isDynamic );
738746 return TranslatedValue .propagateStrict (
739- ctx , typeSystem , callRes , Optional .of (expr ), ctx . mkTrue () , args );
747+ ctx , typeSystem , callRes , Optional .of (expr ), isApprox , args );
740748 });
741749 }
742750
@@ -1239,9 +1247,10 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
12391247 }
12401248 Expr <?> optRef = typeSystem .getOptionalRef (val );
12411249 BoolExpr hasValue = typeSystem .optHasValue (optRef );
1242- BoolExpr valConstraint =
1243- createTypeConstraintForType (typeSystem .getOptionalValue (optRef ), paramType );
1244- return ctx .mkAnd (isOpt , ctx .mkImplies (hasValue , valConstraint ));
1250+ Expr <?> optVal = typeSystem .getOptionalValue (optRef );
1251+ BoolExpr optValNotError = ctx .mkNot (typeSystem .isError (optVal ));
1252+ BoolExpr valConstraint = createTypeConstraintForType (optVal , paramType );
1253+ return ctx .mkAnd (isOpt , ctx .mkImplies (hasValue , ctx .mkAnd (optValNotError , valConstraint )));
12451254 }
12461255 if (type .equals (SimpleType .BOOL )) {
12471256 return (BoolExpr ) ctx .mkApp (typeSystem .boolCons ().getTesterDecl (), val );
@@ -1269,16 +1278,24 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
12691278 if (type .equals (SimpleType .BYTES )) {
12701279 return (BoolExpr ) ctx .mkApp (typeSystem .bytesCons ().getTesterDecl (), val );
12711280 }
1281+ if (type .equals (SimpleType .TIMESTAMP )) {
1282+ IntExpr seconds = typeSystem .getTimestamp (val );
1283+ return ctx .mkAnd (
1284+ typeSystem .isTimestamp (val ), ctx .mkNot (typeSystem .checkTimestampOverflow (seconds )));
1285+ }
1286+ if (type .equals (SimpleType .DURATION )) {
1287+ IntExpr seconds = typeSystem .getDuration (val );
1288+ return ctx .mkAnd (
1289+ typeSystem .isDuration (val ), ctx .mkNot (typeSystem .checkDurationOverflow (seconds )));
1290+ }
1291+
12721292 if (type instanceof ListType ) {
1273- // Lists are explicitly bounded (sequence theory). We're safe in using for-all quantifiers
1274- // here.
1293+ // Constrain list elements using bounded unrolling up to comprehensionUnrollLimit rather
1294+ // than Z3 forall quantifiers to prevent MBQI quantifier instantiation loops.
1295+ // Assert: isList(val) ∧ for all unrolled 0 <= i < length: ¬isError(seq[i]) ∧ typeConstraint(seq[i])
12751296 BoolExpr isList = typeSystem .isList (val );
12761297 CelType elemType = ((ListType ) type ).elemType ();
1277- if (elemType .equals (SimpleType .DYN )) {
1278- return isList ;
1279- }
12801298
1281- // isList(val) ∧ ∀i. (0 <= i < length) ⇒ elemType(seq[i])
12821299 Expr <?> listRef = typeSystem .getListRef (val );
12831300 SeqExpr seq = typeSystem .getSeq (listRef );
12841301 Expr length = ctx .mkLength (seq );
@@ -1288,20 +1305,61 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
12881305 for (int i = 0 ; i < comprehensionUnrollLimit ; i ++) {
12891306 IntExpr idx = ctx .mkInt (i );
12901307 Expr elem = ctx .mkNth (seq , idx );
1291- BoolExpr elemConstraint = createTypeConstraintForType (elem , elemType );
12921308 BoolExpr validIndex = ctx .mkLt (idx , length );
1293- boundsAndTypes .add (ctx .mkImplies (validIndex , elemConstraint ));
1294- BoolExpr outOfBounds = ctx .mkGe (idx , length );
1295- boundsAndTypes .add (ctx .mkImplies (outOfBounds , ctx .mkEq (elem , typeSystem .mkUnknown ())));
1309+ boundsAndTypes .add (ctx .mkImplies (validIndex , ctx .mkNot (typeSystem .isError (elem ))));
1310+ if (!elemType .equals (SimpleType .DYN )) {
1311+ BoolExpr elemConstraint = createTypeConstraintForType (elem , elemType );
1312+ boundsAndTypes .add (ctx .mkImplies (validIndex , elemConstraint ));
1313+ }
12961314 }
12971315
12981316 return CelZ3TypeSystem .mkAndFlattened (ctx , boundsAndTypes );
12991317 }
13001318 if (type instanceof MapType ) {
1301- // Do NOT emit a for-all quantifier over map keys here.
1302- // Doing so forces MBQI into an infinite loop. Structural equivalence of dynamic keys is
1303- // naturally constrained by the primitive key assertions in getStructuralEquality().
1304- return typeSystem .isMap (val );
1319+ // Do NOT emit a for-all quantifier over map keys or values here.
1320+ // Doing so forces MBQI into an infinite loop. Instead, constrain keys and values using
1321+ // bounded unrolling over the key sequence up to comprehensionUnrollLimit.
1322+ // Assert: isMap(val) ∧ for all unrolled 0 <= i < length: isPrimitiveKey(key) ∧ ¬isError(key)
1323+ // ∧ (presence(key) ⇒ ¬isError(val) ∧ typeConstraint(val))
1324+ BoolExpr isMap = typeSystem .isMap (val );
1325+ MapType mapType = (MapType ) type ;
1326+ CelType keyType = mapType .keyType ();
1327+ CelType valType = mapType .valueType ();
1328+
1329+ Expr <?> mapRef = typeSystem .getMapRef (val );
1330+ SeqExpr seq = typeSystem .getMapKeys (mapRef );
1331+ Expr length = ctx .mkLength (seq );
1332+ ArrayExpr mapValues = (ArrayExpr ) typeSystem .getMapValues (mapRef );
1333+ ArrayExpr mapPresence = (ArrayExpr ) typeSystem .getMapPresence (mapRef );
1334+
1335+ List <BoolExpr > boundsAndTypes = new ArrayList <>();
1336+ boundsAndTypes .add (isMap );
1337+
1338+ for (int i = 0 ; i < comprehensionUnrollLimit ; i ++) {
1339+ IntExpr idx = ctx .mkInt (i );
1340+ Expr key = ctx .mkNth (seq , idx );
1341+ BoolExpr validIndex = ctx .mkLt (idx , length );
1342+
1343+ BoolExpr isKeyPrim = typeSystem .isPrimitiveKey (key );
1344+ BoolExpr keyNotError = ctx .mkNot (typeSystem .isError (key ));
1345+ boundsAndTypes .add (ctx .mkImplies (validIndex , ctx .mkAnd (isKeyPrim , keyNotError )));
1346+ if (!keyType .equals (SimpleType .DYN )) {
1347+ boundsAndTypes .add (ctx .mkImplies (validIndex , createTypeConstraintForType (key , keyType )));
1348+ }
1349+
1350+ BoolExpr presence = (BoolExpr ) ctx .mkSelect (mapPresence , key );
1351+ BoolExpr validEntry = ctx .mkAnd (validIndex , presence );
1352+
1353+ Expr mapVal = ctx .mkSelect (mapValues , key );
1354+ BoolExpr valNotError = ctx .mkNot (typeSystem .isError (mapVal ));
1355+ boundsAndTypes .add (ctx .mkImplies (validEntry , valNotError ));
1356+ if (!valType .equals (SimpleType .DYN )) {
1357+ boundsAndTypes .add (
1358+ ctx .mkImplies (validEntry , createTypeConstraintForType (mapVal , valType )));
1359+ }
1360+ }
1361+
1362+ return CelZ3TypeSystem .mkAndFlattened (ctx , boundsAndTypes );
13051363 }
13061364 if (type .kind () == CelKind .STRUCT ) {
13071365 return ctx .mkAnd (
0 commit comments