Repository: pytorch
Issue: Divisibility substitution does the wrong thing with non-trivial max that would be < 2 after division
Labels: triaged,oncall: pt2,module: dynamic shapes

### 🐛 Describe the bug

Internal xref: https://fb.workplace.com/groups/6829516587176185/posts/7042639765863865

Repro:

```
diff --git a/test/test_proxy_tensor.py b/test/test_proxy_tensor.py
index babb5ba85bb..6959a2f0e27 100644
--- a/test/test_proxy_tensor.py
+++ b/test/test_proxy_tensor.py
@@ -1413,6 +1413,15 @@ def forward(self, x_1, y_1):
             return r.view(12, -1, 192)
         make_fx(f, tracing_mode="symbolic")(torch.tensor(24))
 
+    def test_view_divisibility_unbacked_relatively_prime(self):
+        def f(x):
+            i0 = x.item()
+            torch._check_is_size(i0)
+            torch._check(i0 <= 448)
+            torch._check((256 * i0) % 447 == 0)
+            return torch.zeros(256 * i0).view(-1, 447)
+        make_fx(f, tracing_mode="symbolic")(torch.tensor(256*447))
+
     def test_unbacked_unify_guard(self):
         def f(x, y):
             z = torch.zeros(x.item())
```

Fails with

```
  File "/data/users/ezyang/a/pytorch/test/test_proxy_tensor.py", line 1421, in f                                                                 
    torch._check((256 * i0) % 447 == 0)                                                                                                          
  File "/data/users/ezyang/a/pytorch/torch/__init__.py", line 1145, in _check                                                                    
    _check_with(RuntimeError, cond, message)                                                                                                     
  File "/data/users/ezyang/a/pytorch/torch/__init__.py", line 1110, in _check_with                                                               
    if expect_true(cond):                                                                                                                        
  File "/data/users/ezyang/a/pytorch/torch/fx/experimental/symbolic_shapes.py", line 661, in expect_true                                         
    return a.node.expect_true(frame.f_code.co_filename, frame.f_lineno)                                                                          
  File "/data/users/ezyang/a/pytorch/torch/fx/experimental/sym_node.py", line 395, in expect_true                                      
    return self.shape_env.defer_runtime_assert(                                                                                                  
  File "/data/users/ezyang/a/pytorch/torch/fx/experimental/recording.py", line 265, in wrapper
    return event.run(self)                                                                                                                       
  File "/data/users/ezyang/a/pytorch/torch/fx/experimental/recording.py", line 160, in run                                                       
    return self.f(*args, **kwargs)                                                                                                               
  File "/data/users/ezyang/a/pytorch/torch/fx/experimental/symbolic_shapes.py", line 4370, in defer_runtime_assert                               
    self._maybe_guard_rel(expr)                                                                                                                  
  File "/data/users/ezyang/a/pytorch/torch/fx/experimental/symbolic_shapes.py", line 4027, in _maybe_guard_rel                                   
    self._set_replacement(i0, d * i1, "divisibility")                   
  File "/data/users/ezyang/a/pytorch/torch/fx/experimental/symbolic_shapes.py", line 3871, in _set_replacement                                   
    tgt_bound_so = self.bound_sympy(tgt, size_oblivious=True)                                                                                    
  File "/data/users/ezyang/a/pytorch/torch/fx/experimental/symbolic_shapes.py", line 3525, in bound_sympy                                        
    var_to_range[x] &= ValueRanges(2, sympy.oo)                         
  File "/data/users/ezyang/a/pytorch/torch/utils/_sympy/value_ranges.py", line 193, in __and__      
    return ValueRanges(                                                 
  File "/data/users/ezyang/a/pytorch/torch/utils/_sympy/value_ranges.py", line 139, in __init__                                
    raise ValueRangeError(f"Invalid ranges [{lower}:{upper}]")
torch.utils._sympy.value_ranges.ValueRangeError: Invalid ranges [2:448/447]   
```

Actually, the upper bound here doesn't have to be 448, it also fails with 447

```
  File "/data/users/ezyang/a/pytorch/torch/utils/_sympy/value_ranges.py", line 193, in __and__
    return ValueRanges(
  File "/data/users/ezyang/a/pytorch/torch/utils/_sympy/value_ranges.py", line 139, in __init__
    raise ValueRangeError(f"Invalid ranges [{lower}:{upper}]")
torch.utils._sympy.value_ranges.ValueRangeError: Invalid ranges [2:1]
```

The root cause of this is that if you had a bounded unbacked SymInt by max, if you divide it by too much (e.g., max), you will end up with a new unbacked SymInt that actually is just always one. When the upper bound is 447*2, on the other hand, it passes.

I'm not entirely sure what we're supposed to do here. It's sort of similar to an analogous situation in nonzero

```
        if not has_free_symbols(arg.numel()) and arg.numel() == 0:
            # If numel is zero, then the output size must be zero.
            # In this case, we must not allocate an unbacked SymInt,
            # because if we do, it will immediately get refined to
            # zero, but this will be inconsistent with size oblivious
            # tests (which will continue to claim that the unbacked
            # symint cannot equal zero).  We could also unconditionally
            # allocate an unbacked SymInt and not refine its range,
            # but this seems more precise.
            nnz = arg._nonzero_memo = 0
            arg._nonzero_memo_vc = arg._version
```

where sometimes we're like "oops, actually this unbacked symint has to be N".

cc @chauhang @penguinwu @msaroufim @bdhirsh @anijain2305 @lezcano 

### Versions

main