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

@@ -409,6 +409,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

test/SmallIntPromotion.fst

@@ -0,0 +1,27 @@
+/// Regression test for karamel issue #694.
+/// Tests that UInt8/UInt16 integer promotion correctly masks results
+/// before comparisons.
+module SmallIntPromotion
+
+open FStar.UInt8
+
+/// Comparison after wrapping arithmetic must mask to 8 bits.
+/// Use runtime parameters to prevent constant folding.
+let check_add_compare (a b c: UInt8.t) : bool = (a +%^ b) = c
+let check_sub_compare (a b c: UInt8.t) : bool = (a -%^ b) = c
+let check_add_lt (a b c: UInt8.t) : bool = (a +%^ b) <^ c
+let check_shl_compare (a: UInt8.t) (s: FStar.UInt32.t{FStar.UInt32.v s < 8}) (c: UInt8.t) : bool =
+  (a <<^ s) = c
+
+/// Comparison in if-condition must also mask.
+let check_if_add (a b c: UInt8.t) : FStar.Int32.t =
+  if (a +%^ b) = c then 0l else 1l
+
+let main () : FStar.Int32.t =
+  if check_add_compare 255uy 2uy 1uy
+  && check_sub_compare 0uy 1uy 255uy
+  && check_add_lt 200uy 100uy 50uy
+  && check_shl_compare 0x80uy 1ul 0uy
+  && check_if_add 255uy 2uy 1uy = 0l
+  then 0l
+  else 1l