Add a mathematical constraint system

src/ir/CMakeLists.txt

@@ -2,6 +2,7 @@ FILE(GLOB ir_HEADERS *.h)
 set(ir_SOURCES
   ExpressionAnalyzer.cpp
   ExpressionManipulator.cpp
+  constraint.cpp
   drop.cpp
   effects.cpp
   eh-utils.cpp

src/ir/abstract.h

@@ -56,7 +56,8 @@ enum Op {
   GtS,
   GtU,
   GeS,
-  GeU
+  GeU,
+  Invalid
 };
 
 inline bool hasAnyRotateShift(BinaryOp op) {

src/ir/constraint.cpp

@@ -0,0 +1,156 @@
+/*
+ * Copyright 2026 WebAssembly Community Group participants
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#include <optional>
+
+#include "ir/constraint.h"
+#include "ir/properties.h"
+#include "wasm.h"
+
+namespace wasm::constraint {
+
+namespace {
+
+// Evaluate whether a => b, where a and b are operations on constants.
+Result provesConstantPair(Abstract::Op aOp,
+                          const Literal& aConstant,
+                          Abstract::Op bOp,
+                          const Literal& bConstant) {
+  // x == X =?=> x == Y. True iff X == Y.
+  if (aOp == Abstract::Eq && bOp == Abstract::Eq) {
+    return aConstant == bConstant ? True : False;
+  }
+
+  // x == X =?=> x != Y. True iff X != Y.
+  if (aOp == Abstract::Eq && bOp == Abstract::Ne) {
+    return aConstant == bConstant ? False : True;
+  }
+
+  // x != X =?=> x == Y. False if X = Y, else unknown.
+  if (aOp == Abstract::Ne && bOp == Abstract::Eq) {
+    if (aConstant == bConstant) {
+      return False;
+    }
+  }
+
+  // x != X =?=> x != Y. True if X = Y, else unknown.
+  if (aOp == Abstract::Ne && bOp == Abstract::Ne) {
+    if (aConstant == bConstant) {
+      return True;
+    }
+  }
+
+  // TODO: handle >, >=, <, and <=
+  return Unknown;
+}
+
+// Core comparison of two constraints: whether a => b
+Result provesPair(const Constraint& a, const Constraint& b) {
+  // A thing always implies itself.
+  if (a == b) {
+    return True;
+  }
+
+  // Comparisons of two constants.
+  auto* aConstant = std::get_if<Literal>(&a.term);
+  auto* bConstant = std::get_if<Literal>(&b.term);
+  if (aConstant && bConstant) {
+    return provesConstantPair(a.op, *aConstant, b.op, *bConstant);
+  }
+
+  return Unknown;
+}
+
+} // anonymous namespace
+
+Result AndedConstraintSet::proves(const Constraint& condition) const {
+  // Sometimes a single constraint is enough to determine the condition.
+  for (auto& c : *this) {
+    auto result = provesPair(c, condition);
+    if (result != Unknown) {
+      return result;
+    }
+  }
+
+  // TODO smarts for multiple constraints
+
+  // Otherwise, who knows.
+  return Unknown;
+}
+
+Result AndedConstraintSet::proves(const AndedConstraintSet& other) const {
+  if (other.empty()) {
+    // The empty set of constraints is always true.
+    return True;
+  }
+
+  bool hasUnknown = false;
+
+  for (auto& c : other) {
+    auto result = proves(c);
+    if (result == False) {
+      // The entire conjunction is proven false.
+      return False;
+    }
+    if (result == Unknown) {
+      hasUnknown = true;
+    }
+  }
+
+  return hasUnknown ? Unknown : True;
+}
+
+void AndedConstraintSet::fuzzyAnd(const Constraint& c) {
+  if (size() < MaxConstraints) {
+    push_back(c);
+    return;
+  }
+
+  // Otherwise, just do not add this one.
+  // TODO: We could try to be clever and see if one of the existing ones makes
+  //       more sense to drop.
+}
+
+void AndedConstraintSet::fuzzyOr(const AndedConstraintSet& other) {
+  // If one is empty (no constraints, everything is true, and we can prove
+  // nothing useful) then it does not add anything to the other.
+  if (empty()) {
+    *this = other;
+    return;
+  }
+  if (other.empty()) {
+    return;
+  }
+
+  // If this is already implied by current constraints, then it is redundant.
+  // E.g. if we are { x = 10 } and other is { x >= 0 } then all we need is
+  // { x >= 0 } as the result of the OR.
+  if (proves(other) == True) {
+    *this = other;
+    return;
+  }
+  if (other.proves(*this) == True) {
+    return;
+  }
+
+  // TODO smarts: handle <= > and so forth
+
+  // Otherwise, we don't know how to nicely OR these things, and expand to the
+  // trivial set of no constraints.
+  clear();
+}
+
+} // namespace wasm::constraint

src/ir/constraint.h

@@ -0,0 +1,125 @@
+/*
+ * Copyright 2026 WebAssembly Community Group participants
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+//
+// Constraints on the values of things, like x >=0, x < 42, and x == y. Allows
+// inference whether other things are true given a set of constraints, like
+// { x == 10 } => { x >= 5 }.
+//
+
+#ifndef wasm_ir_constraint_h
+#define wasm_ir_constraint_h
+
+#include <variant>
+
+#include "ir/abstract.h"
+#include "support/inplace_vector.h"
+#include "support/utilities.h"
+#include "wasm.h"
+
+namespace wasm::constraint {
+
+// A term in a constraint, either a local index or literal value.
+struct Term : public std::variant<Index, Literal> {
+  bool operator==(const Term&) const = default;
+};
+
+// A constraint: some operation and some value, like "is equal to 17" or "is
+// less than local 6".
+struct Constraint {
+  Abstract::Op op = Abstract::Invalid;
+  Term term;
+
+  bool operator==(const Constraint&) const = default;
+};
+
+// We limit constraints to a low number to ensure good performance even with
+// simple brute-force solving.
+// TODO: use a generic constraint solver..?
+inline constexpr std::size_t MaxConstraints = 3;
+
+// What we infer from one thing about another: true/false, or unknown.
+enum Result { True, False, Unknown };
+
+// A set of constraints connected by the logical "and" operation. That is, all
+// the constraints are simultaneously true about some value. In the examples in
+// the comments below, `x` is used for the thing all the constraints are talking
+// about, which looks like a local, but it could be a global or a struct field
+// or anything else in general.
+struct AndedConstraintSet : inplace_vector<Constraint, MaxConstraints> {
+  // Check a condition against this set, that is, whether the existing
+  // constraints prove that it must be true, false, or unknown: whether
+  //
+  //   { this } => { condition }
+  //
+  // https://en.wikipedia.org/wiki/Material_conditional#Truth_table
+  Result proves(const Constraint& condition) const;
+
+  // Check an entire other set.
+  Result proves(const AndedConstraintSet& other) const;
+
+  // Add a constraint to the set, ANDed with the others. This is a fuzzy
+  // operation because our capacity is bounded - we cannot have more than
+  // MaxConstraints. If too many are added, we will drop some, which means we
+  // will be able to prove less things (but we will never prove anything
+  // incorrectly).
+  void fuzzyAnd(const Constraint& c);
+
+  // Merge constraints using OR. We cannot represent such a thing directly
+  // (we only use AND), so we approximate it in a fuzzy way. For example, this
+  // would be valid:
+  //
+  //   fuzzyOr({ x == 5 }, { x == 10 }) == { x >= 5 && x <= 10 }
+  //
+  // Note how the result here still accepts the values 5 and 10, but it also
+  // allows more. Formally, this has the following mathematical property:
+  //
+  //   (X || Y) => fuzzyOr(X, Y)
+  //
+  // That is, if X or Y is true, the result of fuzzOr is also true. But the
+  // reverse is not always the case: fuzzyOr may be true without X || Y being
+  // true (see the truth table linked above, and the value 8 in the example).
+  //
+  // Returning to the example, we can use this to optimize as follows: if
+  // two code paths reaching a location have x == 5 and x == 10, so the value in
+  // the merge location is either 5 or 10, then if we see some i32.ge_s that
+  // does x >= 0 then we can evaluate it with proves():
+  //
+  //   { x >= 5 && x <= 10 }.proves({ x >= 0 }) == True
+  //
+  // And it is valid to optimize that i32.ge_s into a constant 1, since
+  //
+  //   { x == 5 || x == 10 } =>
+  //   { x >= 5 && x <= 10 } =>
+  //   { x >= 0 }
+  //
+  // I.e. the constraints imply the truth of the thing we are evaluating.
+  //
+  // Note that the fuzziness here means that fuzzyOr() can do a better or a
+  // worse job. It is always valid for fuzzyOr to return { } or any other
+  // always-true thing (see the truth table linked above). But then:
+  //
+  //   { x == 5 || x == 10 }  =>
+  //   { }                   =!!>
+  //   { x >= 0 }
+  //
+  // If we become too fuzzy, we lose the ability to imply anything useful.
+  void fuzzyOr(const AndedConstraintSet& other);
+};
+
+} // namespace wasm::constraint
+
+#endif // wasm_ir_constraint_h

test/gtest/CMakeLists.txt

@@ -9,6 +9,7 @@ set(unittest_SOURCES
   arena.cpp
   cast-check.cpp
   cfg.cpp
+  constraint.cpp
   dataflow.cpp
   delta_debugging.cpp
   dfa_minimization.cpp