Avoid redundant upcasts in UInt8/UInt16 comparisons

When both operands of a comparison are atomic (variables, field accesses,
function results — not arithmetic expressions), strip the unnecessary
Cast(_, UInt32) wrappers and compare at native width.

Before: (uint32_t)a == (uint32_t)b   (redundant casts)
After:  a == b                       (clean, no casts)

Arithmetic comparisons are unaffected — they still widen and mask:
  ((uint32_t)a + (uint32_t)b & 0xFFU) == (uint32_t)c

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

Author: Lef Ioannidis

lib/AstToCStar.ml

@@ -343,6 +343,11 @@ 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 when a1 && a2 ->
+          (* Both operands are atomic (no arithmetic widening) — compare at
+             native width without redundant upcasts. *)
+          let strip e = match e with CStar.Cast (inner, _) -> inner | _ -> e in
+          CStar.Call (Op op, [ strip e1; strip e2 ])
       | Eq | Neq | Lt | Lte | Gt | Gte ->
           CStar.Call (Op op, [ mask_if a1 w e1; mask_if a2 w e2 ])
       | _ ->

test/pulse/Break.expected.c

@@ -42,17 +42,17 @@ void Break_break_continue_and_return(uint8_t which)
   while (cond)
   {
     bool _continue = false;
-    if ((uint32_t)which == 0U)
+    if (which == 0U)
       _break = true;
     bool _break1 = _break;
     if (!_break1)
     {
-      if ((uint32_t)which == 1U)
+      if (which == 1U)
         _continue = true;
       bool _continue1 = _continue;
       if (!_continue1)
       {
-        if ((uint32_t)which == 2U)
+        if (which == 2U)
           _return = true;
         bool _return1 = _return;
         if (!_return1)