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

@@ -417,6 +417,24 @@ 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.UInt8 || w = K.UInt16) ->
+      (* 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