From 37e3f98618a5b9b5538d01a4388103a1cbe4642e Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 12:30:25 -0700
Subject: [PATCH 1/8] comparisons

---
 src/ir/constraint.cpp | 41 +++++++++++++++++++++++++++++------------
 1 file changed, 29 insertions(+), 12 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index e6119600442..3e438337f72 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -24,36 +24,53 @@ namespace wasm::constraint {
 
 namespace {
 
+Result TrueFalse(bool x) {
+  return x ? True : False;
+}
+
+Result TrueFalse(Literal x) {
+  return TrueFalse(x.getUnsigned());
+}
+
 // 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;
+  // a == A =?=> a op B. Simply apply A to the operation against B.
+  if (aOp == Abstract::Eq) {
+    switch (bOp) {
+      case Abstract::Eq:
+        return TrueFalse(aConstant == bConstant);
+      case Abstract::Ne:
+        return TrueFalse(aConstant != bConstant);
+      case Abstract::LtS:
+        return TrueFalse(aConstant.ltS(bConstant));
+      case Abstract::LeS:
+        return TrueFalse(aConstant.leS(bConstant));
+      case Abstract::GtS:
+        return TrueFalse(aConstant.gtS(bConstant));
+      case Abstract::GeS:
+        return TrueFalse(aConstant.geS(bConstant));
+      default: {}
+    }
   }
 
-  // x != X =?=> x == Y. False if X = Y, else unknown.
+  // a != A =?=> a == B. False if A = B, else unknown.
   if (aOp == Abstract::Ne && bOp == Abstract::Eq) {
     if (aConstant == bConstant) {
       return False;
     }
   }
 
-  // x != X =?=> x != Y. True if X = Y, else unknown.
+  // a != A =?=> a != B. True if A = B, else unknown.
   if (aOp == Abstract::Ne && bOp == Abstract::Ne) {
     if (aConstant == bConstant) {
       return True;
     }
-  }
+  }  
 
-  // TODO: handle >, >=, <, and <=
+  // TODO: handle all the rest of >, >=, <, and <=
   return Unknown;
 }
 

From aa3dc24ca0f5fc530a02f22a08e0f6f562d15914 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 12:30:31 -0700
Subject: [PATCH 2/8] fmt

---
 src/ir/constraint.cpp | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 3e438337f72..cde009bfdca 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -24,13 +24,9 @@ namespace wasm::constraint {
 
 namespace {
 
-Result TrueFalse(bool x) {
-  return x ? True : False;
-}
+Result TrueFalse(bool x) { return x ? True : False; }
 
-Result TrueFalse(Literal x) {
-  return TrueFalse(x.getUnsigned());
-}
+Result TrueFalse(Literal x) { return TrueFalse(x.getUnsigned()); }
 
 // Evaluate whether a => b, where a and b are operations on constants.
 Result provesConstantPair(Abstract::Op aOp,
@@ -52,7 +48,8 @@ Result provesConstantPair(Abstract::Op aOp,
         return TrueFalse(aConstant.gtS(bConstant));
       case Abstract::GeS:
         return TrueFalse(aConstant.geS(bConstant));
-      default: {}
+      default: {
+      }
     }
   }
 
@@ -68,7 +65,7 @@ Result provesConstantPair(Abstract::Op aOp,
     if (aConstant == bConstant) {
       return True;
     }
-  }  
+  }
 
   // TODO: handle all the rest of >, >=, <, and <=
   return Unknown;

From 6c7e2b02f9295fd240ef42f8be49b14984c21c15 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 12:34:06 -0700
Subject: [PATCH 3/8] work

---
 test/lit/passes/constraint-analysis.wast | 76 ++++++++++++++++++++++++
 1 file changed, 76 insertions(+)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 14e804a53f7..fe8967a55be 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -3924,5 +3924,81 @@
       )
     )
   )
+
+  ;; CHECK:      (func $constant-inequalities-lt_s (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-lt_s (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.lt_u
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 41)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.lt_u
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 42)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.lt_u
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 43)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-lt_s
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.lt_s
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.lt_s
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.lt_s
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.lt_s
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
 )
 

From 88547337dcdfcf9752287957aabd8388ea3316dc Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 12:35:57 -0700
Subject: [PATCH 4/8] work

---
 src/ir/constraint.cpp                    |   8 +
 test/lit/passes/constraint-analysis.wast | 485 ++++++++++++++++++++++-
 2 files changed, 480 insertions(+), 13 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index cde009bfdca..7366a7645b5 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -48,6 +48,14 @@ Result provesConstantPair(Abstract::Op aOp,
         return TrueFalse(aConstant.gtS(bConstant));
       case Abstract::GeS:
         return TrueFalse(aConstant.geS(bConstant));
+      case Abstract::LtU:
+        return TrueFalse(aConstant.ltU(bConstant));
+      case Abstract::LeU:
+        return TrueFalse(aConstant.leU(bConstant));
+      case Abstract::GtU:
+        return TrueFalse(aConstant.gtU(bConstant));
+      case Abstract::GeU:
+        return TrueFalse(aConstant.geU(bConstant));
       default: {
       }
     }
diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index fe8967a55be..ed98a224652 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -3949,22 +3949,13 @@
   ;; OPTIN-NEXT:   (i32.const 42)
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT:  (drop
-  ;; OPTIN-NEXT:   (i32.lt_u
-  ;; OPTIN-NEXT:    (local.get $x)
-  ;; OPTIN-NEXT:    (i32.const 41)
-  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (i32.const 0)
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT:  (drop
-  ;; OPTIN-NEXT:   (i32.lt_u
-  ;; OPTIN-NEXT:    (local.get $x)
-  ;; OPTIN-NEXT:    (i32.const 42)
-  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (i32.const 0)
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT:  (drop
-  ;; OPTIN-NEXT:   (i32.lt_u
-  ;; OPTIN-NEXT:    (local.get $x)
-  ;; OPTIN-NEXT:    (i32.const 43)
-  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (i32.const 1)
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT:  (drop
   ;; OPTIN-NEXT:   (i32.const 0)
@@ -4000,5 +3991,473 @@
       )
     )
   )
-)
 
+  ;; CHECK:      (func $constant-inequalities-le_s (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-le_s (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-le_s
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.le_s
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.le_s
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.le_s
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.le_s
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
+
+  ;; CHECK:      (func $constant-inequalities-gt_s (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-gt_s (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-gt_s
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.gt_s
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.gt_s
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.gt_s
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.gt_s
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
+
+  ;; CHECK:      (func $constant-inequalities-ge_s (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-ge_s (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-ge_s
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.ge_s
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.ge_s
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.ge_s
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.ge_s
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
+
+  ;; CHECK:      (func $constant-inequalities-lt_u (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-lt_u (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-lt_u
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.lt_u
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.lt_u
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.lt_u
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.lt_u
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
+
+  ;; CHECK:      (func $constant-inequalities-le_u (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-le_u (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-le_u
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.le_u
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.le_u
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.le_u
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.le_u
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
+
+  ;; CHECK:      (func $constant-inequalities-gt_u (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-gt_u (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-gt_u
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.gt_u
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.gt_u
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.gt_u
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.gt_u
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
+
+  ;; CHECK:      (func $constant-inequalities-ge_u (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-ge_u (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-ge_u
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.ge_u
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.ge_u
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.ge_u
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.ge_u
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
+)

From f9ae5f1ccde34e3c151ab83078d67d113f8f3881 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 12:38:22 -0700
Subject: [PATCH 5/8] work

---
 test/lit/passes/constraint-analysis.wast | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index ed98a224652..f8c9af32993 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -3962,6 +3962,7 @@
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT: )
   (func $constant-inequalities-lt_s
+    ;; A constant in $x is checked against inequalities using constants.
     (local $x i32)
     (local.set $x
       (i32.const 42)

From f708a61ce1b2e7e549249497b038f5e8fa76fa85 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 13:49:44 -0700
Subject: [PATCH 6/8] work

---
 src/ir/constraint.cpp                    | 12 ++++++-
 test/lit/passes/constraint-analysis.wast | 46 ++++++++++++++++++++++++
 2 files changed, 57 insertions(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 7366a7645b5..72c0d125803 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -32,7 +32,8 @@ Result TrueFalse(Literal x) { return TrueFalse(x.getUnsigned()); }
 Result provesConstantPair(Abstract::Op aOp,
                           const Literal& aConstant,
                           Abstract::Op bOp,
-                          const Literal& bConstant) {
+                          const Literal& bConstant,
+                          bool recursing=false) {
   // a == A =?=> a op B. Simply apply A to the operation against B.
   if (aOp == Abstract::Eq) {
     switch (bOp) {
@@ -75,6 +76,15 @@ Result provesConstantPair(Abstract::Op aOp,
     }
   }
 
+  if (!recursing) {
+    // The flipped operation may tell us something:  y ==> !x  implies
+    // x ==> y  is false (because if not, then x would prove y, and y would
+    // prove !x, a contradiction).
+    if (provesConstantPair(bOp, bConstant, aOp, aConstant, true) == False) {
+      return False;
+    }
+  }
+
   // TODO: handle all the rest of >, >=, <, and <=
   return Unknown;
 }
diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index f8c9af32993..35d3b003c8d 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -4461,4 +4461,50 @@
       )
     )
   )
+
+  ;; CHECK:      (func $flipped-contradiction (type $9) (result i32)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (loop $loop
+  ;; CHECK-NEXT:   (br_if $loop
+  ;; CHECK-NEXT:    (i32.const 1)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (br_if $loop
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (unreachable)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $flipped-contradiction (type $9) (result i32)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (loop $loop
+  ;; OPTIN-NEXT:   (br_if $loop
+  ;; OPTIN-NEXT:    (i32.const 1)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (br_if $loop
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (unreachable)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $flipped-contradiction (result i32)
+    (local $x i32)
+    (loop $loop (result i32)
+      ;; If we do not branch, we add the constraint x >= 1.
+      (br_if $loop
+        (i32.lt_u
+          (local.get $x)
+          (i32.const 1)
+        )
+      )
+      ;; If we do not branch, we add the constraint x == 0. This contradicts the
+      ;; one before, making the code after us unreachable.
+      (br_if $loop
+        (local.get $x)
+      )
+      ;; An eqz that will become unreachable.
+      (i32.eqz
+        (i32.const 0)
+      )
+    )
+  )
 )

From d00bed6d8460d6a77809b369533f6303519a4712 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 13:50:39 -0700
Subject: [PATCH 7/8] work

---
 src/ir/constraint.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 72c0d125803..78cad40f2bb 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -33,7 +33,7 @@ Result provesConstantPair(Abstract::Op aOp,
                           const Literal& aConstant,
                           Abstract::Op bOp,
                           const Literal& bConstant,
-                          bool recursing=false) {
+                          bool recursing = false) {
   // a == A =?=> a op B. Simply apply A to the operation against B.
   if (aOp == Abstract::Eq) {
     switch (bOp) {

From e58adf7e4db3731fe544fd2462862a043d7726e8 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 13:52:28 -0700
Subject: [PATCH 8/8] work

---
 test/lit/passes/constraint-analysis.wast | 64 +++++++++++++++++++++---
 1 file changed, 56 insertions(+), 8 deletions(-)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 35d3b003c8d..0f9a7f02d90 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -2854,7 +2854,7 @@
     )
   )
 
-  ;; CHECK:      (func $local-changes-if (type $6) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+  ;; CHECK:      (func $local-changes-if (type $7) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
   ;; CHECK-NEXT:  (if
   ;; CHECK-NEXT:   (i32.eq
   ;; CHECK-NEXT:    (local.get $x)
@@ -2911,7 +2911,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $local-changes-if (type $6) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+  ;; OPTIN:      (func $local-changes-if (type $7) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
   ;; OPTIN-NEXT:  (if
   ;; OPTIN-NEXT:   (i32.eq
   ;; OPTIN-NEXT:    (local.get $x)
@@ -3547,7 +3547,7 @@
     )
   )
 
-  ;; CHECK:      (func $simple-array-sum (type $7) (param $param (ref $array)) (result i32)
+  ;; CHECK:      (func $simple-array-sum (type $8) (param $param (ref $array)) (result i32)
   ;; CHECK-NEXT:  (local $index i32)
   ;; CHECK-NEXT:  (local $sum i32)
   ;; CHECK-NEXT:  (local $len i32)
@@ -3592,7 +3592,7 @@
   ;; CHECK-NEXT:   (br $loop)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $simple-array-sum (type $7) (param $param (ref $array)) (result i32)
+  ;; OPTIN:      (func $simple-array-sum (type $8) (param $param (ref $array)) (result i32)
   ;; OPTIN-NEXT:  (local $index i32)
   ;; OPTIN-NEXT:  (local $sum i32)
   ;; OPTIN-NEXT:  (local $len i32)
@@ -3767,7 +3767,7 @@
     )
   )
 
-  ;; CHECK:      (func $iloop (type $8) (param $0 f32)
+  ;; CHECK:      (func $iloop (type $9) (param $0 f32)
   ;; CHECK-NEXT:  (local $1 f32)
   ;; CHECK-NEXT:  (local.set $0
   ;; CHECK-NEXT:   (local.get $1)
@@ -3792,7 +3792,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $iloop (type $8) (param $0 f32)
+  ;; OPTIN:      (func $iloop (type $9) (param $0 f32)
   ;; OPTIN-NEXT:  (local $1 f32)
   ;; OPTIN-NEXT:  (local.set $0
   ;; OPTIN-NEXT:   (local.get $1)
@@ -4462,7 +4462,7 @@
     )
   )
 
-  ;; CHECK:      (func $flipped-contradiction (type $9) (result i32)
+  ;; CHECK:      (func $flipped-contradiction (type $6) (result i32)
   ;; CHECK-NEXT:  (local $x i32)
   ;; CHECK-NEXT:  (loop $loop
   ;; CHECK-NEXT:   (br_if $loop
@@ -4474,7 +4474,7 @@
   ;; CHECK-NEXT:   (unreachable)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $flipped-contradiction (type $9) (result i32)
+  ;; OPTIN:      (func $flipped-contradiction (type $6) (result i32)
   ;; OPTIN-NEXT:  (local $x i32)
   ;; OPTIN-NEXT:  (loop $loop
   ;; OPTIN-NEXT:   (br_if $loop
@@ -4507,4 +4507,52 @@
       )
     )
   )
+
+  ;; CHECK:      (func $flipped-contradiction-no (type $6) (result i32)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (loop $loop (result i32)
+  ;; CHECK-NEXT:   (br_if $loop
+  ;; CHECK-NEXT:    (i32.const 0)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (br_if $loop
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (i32.eqz
+  ;; CHECK-NEXT:    (i32.const 0)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $flipped-contradiction-no (type $6) (result i32)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (loop $loop (result i32)
+  ;; OPTIN-NEXT:   (br_if $loop
+  ;; OPTIN-NEXT:    (i32.const 0)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (br_if $loop
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (i32.eqz
+  ;; OPTIN-NEXT:    (i32.const 0)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $flipped-contradiction-no (result i32)
+    ;; As above, but with lt replaced by gt. Now the constraints are x <= 1 and
+    ;; x == 0, which do not contradict, and nothing becomes unreachable.
+    (local $x i32)
+    (loop $loop (result i32)
+      (br_if $loop
+        (i32.gt_u
+          (local.get $x)
+          (i32.const 1)
+        )
+      )
+      (br_if $loop
+        (local.get $x)
+      )
+      (i32.eqz
+        (i32.const 0)
+      )
+    )
+  )
 )