@@ -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,25 @@ 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]) ∧
1296+ // typeConstraint(seq[i])
12751297 BoolExpr isList = typeSystem .isList (val );
12761298 CelType elemType = ((ListType ) type ).elemType ();
1277- if (elemType .equals (SimpleType .DYN )) {
1278- return isList ;
1279- }
12801299
1281- // isList(val) ∧ ∀i. (0 <= i < length) ⇒ elemType(seq[i])
12821300 Expr <?> listRef = typeSystem .getListRef (val );
12831301 SeqExpr seq = typeSystem .getSeq (listRef );
12841302 Expr length = ctx .mkLength (seq );
@@ -1288,20 +1306,69 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
12881306 for (int i = 0 ; i < comprehensionUnrollLimit ; i ++) {
12891307 IntExpr idx = ctx .mkInt (i );
12901308 Expr elem = ctx .mkNth (seq , idx );
1291- BoolExpr elemConstraint = createTypeConstraintForType (elem , elemType );
12921309 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 ())));
1310+ // Assert ¬isError(elem) as a domain invariant so Z3 never synthesizes an Error element in
1311+ // list(dyn). For concrete types, this is already implied by createTypeConstraintForType.
1312+ boundsAndTypes .add (ctx .mkImplies (validIndex , ctx .mkNot (typeSystem .isError (elem ))));
1313+ // Short-circuit DYN element types to prevent generating redundant validIndex ⇒ TRUE
1314+ // clauses.
1315+ if (!elemType .equals (SimpleType .DYN )) {
1316+ BoolExpr elemConstraint = createTypeConstraintForType (elem , elemType );
1317+ boundsAndTypes .add (ctx .mkImplies (validIndex , elemConstraint ));
1318+ }
12961319 }
12971320
12981321 return CelZ3TypeSystem .mkAndFlattened (ctx , boundsAndTypes );
12991322 }
13001323 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 );
1324+ // Do NOT emit a for-all quantifier over map keys or values here.
1325+ // Doing so forces MBQI into an infinite loop. Instead, constrain keys and values using
1326+ // bounded unrolling over the key sequence up to comprehensionUnrollLimit.
1327+ // Assert: isMap(val) ∧ for all unrolled 0 <= i < length: isPrimitiveKey(key) ∧ ¬isError(key)
1328+ // ∧ (presence(key) ⇒ ¬isError(val) ∧ typeConstraint(val))
1329+ BoolExpr isMap = typeSystem .isMap (val );
1330+ MapType mapType = (MapType ) type ;
1331+ CelType keyType = mapType .keyType ();
1332+ CelType valType = mapType .valueType ();
1333+
1334+ Expr <?> mapRef = typeSystem .getMapRef (val );
1335+ SeqExpr seq = typeSystem .getMapKeys (mapRef );
1336+ Expr length = ctx .mkLength (seq );
1337+ ArrayExpr mapValues = (ArrayExpr ) typeSystem .getMapValues (mapRef );
1338+ ArrayExpr mapPresence = (ArrayExpr ) typeSystem .getMapPresence (mapRef );
1339+
1340+ List <BoolExpr > boundsAndTypes = new ArrayList <>();
1341+ boundsAndTypes .add (isMap );
1342+
1343+ for (int i = 0 ; i < comprehensionUnrollLimit ; i ++) {
1344+ IntExpr idx = ctx .mkInt (i );
1345+ Expr key = ctx .mkNth (seq , idx );
1346+ BoolExpr validIndex = ctx .mkLt (idx , length );
1347+
1348+ BoolExpr isKeyPrim = typeSystem .isPrimitiveKey (key );
1349+ BoolExpr keyNotError = ctx .mkNot (typeSystem .isError (key ));
1350+ // Assert isKeyPrim ∧ ¬isError(key) so Z3 never synthesizes a non-primitive or Error key in
1351+ // map(dyn, ...). For concrete map types, this is already implied by keyType constraints.
1352+ boundsAndTypes .add (ctx .mkImplies (validIndex , ctx .mkAnd (isKeyPrim , keyNotError )));
1353+ // Short-circuit DYN key types to prevent generating redundant validIndex ⇒ TRUE clauses.
1354+ if (!keyType .equals (SimpleType .DYN )) {
1355+ boundsAndTypes .add (ctx .mkImplies (validIndex , createTypeConstraintForType (key , keyType )));
1356+ }
1357+
1358+ BoolExpr presence = (BoolExpr ) ctx .mkSelect (mapPresence , key );
1359+ BoolExpr validEntry = ctx .mkAnd (validIndex , presence );
1360+
1361+ Expr mapVal = ctx .mkSelect (mapValues , key );
1362+ BoolExpr valNotError = ctx .mkNot (typeSystem .isError (mapVal ));
1363+ boundsAndTypes .add (ctx .mkImplies (validEntry , valNotError ));
1364+ // Short-circuit DYN value types to prevent generating redundant validEntry ⇒ TRUE clauses.
1365+ if (!valType .equals (SimpleType .DYN )) {
1366+ boundsAndTypes .add (
1367+ ctx .mkImplies (validEntry , createTypeConstraintForType (mapVal , valType )));
1368+ }
1369+ }
1370+
1371+ return CelZ3TypeSystem .mkAndFlattened (ctx , boundsAndTypes );
13051372 }
13061373 if (type .kind () == CelKind .STRUCT ) {
13071374 return ctx .mkAnd (
0 commit comments