Fix UInt8/UInt16 comparison after wrapping arithmetic (#694)

Comparisons (Eq, Neq, Lt, Lte, Gt, Gte) on UInt8/UInt16 after wrapping
arithmetic (add_mod, sub_mod, mul_mod, shift_left, xor, or, etc.) produced
wrong C code. The uint32 intermediate from mk_arith was compared directly
without masking back to the original width.

For example, (255uy +%^ 1uy) = 0uy generated:
  (uint32_t)255 + (uint32_t)1 == 0  =>  256 == 0  =>  false (WRONG)

Fix: handle comparisons in mk_expr (not mk_arith) with a dedicated pattern
that only widens+masks operands containing arithmetic subexpressions.
Atomic operands (variables, field accesses, etc.) are compared at their
native width without unnecessary casts.

Now generates:
  simple:  a == b                              (no casts)
  arith:   ((uint32_t)a + (uint32_t)b & 0xFFU) == c   (only arith side)

Fixes #694. Also fixes #689, #691, #692, #693 (same root cause).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: Lef Ioannidis

lib/AstToCStar.ml

@@ -311,8 +311,7 @@ and mask w e =
 and is_integer_arith op w =
   w <> K.Bool && not (Constant.is_float w) && K.is_unsigned w && match op with
   | K.Add | AddW | Sub | SubW | Div | DivW | Mult | MultW | Mod
-  | BOr | BAnd | BXor | BShiftL | BShiftR | BNot
-  | Eq | Neq | Lt | Lte | Gt | Gte ->
+  | BOr | BAnd | BXor | BShiftL | BShiftR | BNot ->
       true
   | _ ->
       false
@@ -343,8 +342,6 @@ and mk_arith env e =
           CStar.Call (Op op, [ mask_if a1 w e1; mask_if a2 w e2 ])
       | BShiftR ->
           CStar.Call (Op op, [ mask_if a1 w e1; e2 ])
-      | Eq | Neq | Lt | Lte | Gt | Gte ->
-          CStar.Call (Op op, [ mask_if a1 w e1; mask_if a2 w e2 ])
       | _ ->
           assert false
       end, false, w1 || w2
@@ -417,6 +414,25 @@ and mk_expr env in_stmt under_initializer_list e =
       else
         e'
 
+  | EApp ({ node = EOp (op, w); _ }, [ e1; e2 ])
+      when Constant.is_comp_op op
+        && w <> K.Bool && not (Constant.is_float w) && K.is_unsigned w ->
+      (* Comparisons on narrow unsigned types: only widen+mask operands that
+         contain arithmetic. Atomic operands (variables, field accesses, etc.)
+         are compared at their native width without unnecessary casts. *)
+      let needs_arith e = match e.node with
+        | EApp ({ node = EOp (op, w); _ }, _) -> is_integer_arith op w
+        | _ -> false
+      in
+      let mk_cmp_operand e =
+        if needs_arith e then
+          let e', a, _ = mk_arith env e in
+          if a then e' else mask w e'
+        else
+          mk_expr env false e
+      in
+      CStar.Call (Op op, [ mk_cmp_operand e1; mk_cmp_operand e2 ])
+
   | EApp (e, es) ->
       (* Functions that only take a unit take no argument. *)
       let t, _ = flatten_arrow e.typ in