Model one-operand imul as a signed multiply in the assembly checker

Fixes scrutineer security finding #2514.

The one-operand form of `imul r/m` (rdx:rax := rax * src, or ax := al * src
for 8-bit operands) shared a single branch with `mul` in both the symbolic
executor (src/Assembly/Symbolic.v, SymexNormalInstruction) and the concrete
semantics (src/Assembly/WithBedrock/Semantics.v, DenoteNormalInstruction).
Both computed the *unsigned* full product.  On real x86-64 hardware `mul` is
unsigned but one-operand `imul` is signed (Intel SDM Vol. 2A, IMUL), so the
high word written to rdx (ah for 8-bit) differs whenever an operand has its
top bit set; the low word agrees.  For example, with rax = 0xffffffff00000001
(the top limb of the P-256 prime) and rcx = 3, `imul rcx` leaves rdx =
0xffffffffffffffff on hardware, but the model computed 0x2.

Consequently the equivalence checker (`--hints-file`) could certify assembly
that uses `imul rcx` where the reference computation needs the unsigned high
word from `mul rcx` / `mulx`, i.e. accept non-equivalent assembly.  The two-
and three-operand forms of `imul` only write the low half and were already
correct.

The fix splits the shared branch:

- `mul` keeps its previous (unsigned) behaviour unchanged.
- One-operand `imul` now computes the high word as
  `keep s ((Z.signed s rax * Z.signed s src) >> s)` in the concrete
  semantics, and in the symbolic executor as
  `shr s (mulZ (signed rax) (signed src)) s` where `signed x` is spelled
  with existing operators as `addZ (add s x (2^(s-1))) (-(2^(s-1)))`, which
  is exactly `Z.signed s x` unfolded.  The low word is still the (unsigned)
  `mulZ` product, which agrees with the signed one after truncation.  Flags
  are havocked as before.  The 8-bit form (ah:al) is handled by the same
  code.
- The symbolic high-word computation lives in a new definition
  `SignedMulHigh` rather than inline in `SymexNormalInstruction`, with its
  own `same_reg_some_of_success` / `same_mem_addressed_of_success`
  instances in EquivalenceProofs.v (derived by typeclass resolution, like
  `Symeval`).  Inlining it made the generic tactics of
  `SymexNormalInstruction_reg_same`/`_mem_same` blow up (they are
  exponential in the number of binds of a branch), and nesting the whole
  expression in a single `Symeval` made the `Qed` of
  `SymexNornalInstruction_R` take over an hour; with the separate
  definition all three files compile in about the same time as before.
- SymbolicProofs.v unfolds `SignedMulHigh` alongside
  `SymexNormalInstruction` and gains a small case for the new branch
  relating the unfolded sign extension to `Z.signed`.

A new test file src/Assembly/WithBedrock/SemanticsTests.v pins down the
hardware values of `mul`/`imul` (64- and 8-bit, top bit set or clear) for
both the concrete semantics and the symbolic executor; the imul cases fail
against the previous model.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016Rbn2gww3MGhvrh52fNjpD

Author: JasonGross

src/Assembly/EquivalenceProofs.v

@@ -2845,6 +2845,12 @@ Typeclasses Opaque Symeval.
 #[global]
 Typeclasses Transparent AddressSize OperationSize.
 
+(* TODO: move? *)
+Local Instance SignedMulHigh_reg_same {opts : symbolic_options_computed_opt} {descr:description} {sz:OperationSize} {sa:AddressSize} src1 src2 : same_reg_some_of_success (SignedMulHigh src1 src2).
+Proof. cbv [SignedMulHigh]; typeclasses eauto. Qed.
+#[global]
+Typeclasses Opaque SignedMulHigh.
+
 (* TODO: move? *)
 Local Instance SymexNormalInstruction_reg_same {opts : symbolic_options_computed_opt} {descr:description} instr : same_reg_some_of_success (SymexNormalInstruction instr).
 Proof.
@@ -3015,6 +3021,12 @@ Typeclasses Opaque Symeval.
 #[global]
 Typeclasses Transparent AddressSize OperationSize.
 
+(* TODO: move? *)
+Local Instance SignedMulHigh_mem_same {opts : symbolic_options_computed_opt} {descr:description} {sz:OperationSize} {sa:AddressSize} src1 src2 : same_mem_addressed_of_success (SignedMulHigh src1 src2).
+Proof. cbv [SignedMulHigh]; typeclasses eauto. Qed.
+#[global]
+Typeclasses Opaque SignedMulHigh.
+
 (* TODO: move? *)
 Local Instance SymexNormalInstruction_mem_same {opts : symbolic_options_computed_opt} {descr:description} instr : same_mem_addressed_of_success (SymexNormalInstruction instr).
 Proof.

src/Assembly/Symbolic.v

@@ -4184,6 +4184,25 @@ Definition rcrcnt s cnt : Z :=
   Z.land cnt (Z.of_N s-1).
 
 Notation "f @ ( x , y , .. , z )" := (PreApp f (@cons pre_expr x (@cons pre_expr y .. (@cons pre_expr z nil) ..))) (at level 10) : x86symex_scope.
+
+(** [SignedMulHigh src1 src2] is the high [s] bits of the product of the
+    [s]-bit operands [src1] and [src2] interpreted as signed (two's
+    complement) values, i.e. what the one-operand form of [imul] writes to
+    [rdx] (resp. [ah]).  [Z.signed s x] is spelled with existing operators
+    as [addZ (add s x 2^(s-1)) (-(2^(s-1)))].  This is a separate definition
+    rather than being inlined into [SymexNormalInstruction] so that the
+    proofs about [SymexNormalInstruction] can treat it as a unit, the way
+    they treat [Symeval]. *)
+Definition SignedMulHigh {opts : symbolic_options_computed_opt} {descr:description} {s : OperationSize} {sa : AddressSize} (src1 src2 : ARG) : M idx :=
+  (let half : Z := Z.shiftl 1 (Z.of_N s-1) in
+   let signed_ (x : idx) : pre_expr
+     := addZ@(add s@(x, PreApp (const half) nil), PreApp (const (-half)) nil) in
+   a  <- GetOperand src1;
+   b  <- GetOperand src2;
+   xa <- Symeval (signed_ a);
+   xb <- Symeval (signed_ b);
+   p  <- Symeval (mulZ@(xa,xb));
+   Symeval (shr s@(p, PreApp (const (Z.of_N s)) nil)))%x86symex.
 Definition SymexNormalInstruction {opts : symbolic_options_computed_opt} {descr:description} (instr : NormalInstruction) : M unit :=
   let stack_addr_size : AddressSize := 64%N in
   let sa : AddressSize := 64%N in
@@ -4298,7 +4317,7 @@ Definition SymexNormalInstruction {opts : symbolic_options_computed_opt} {descr:
     vh <- Symeval (shrZ@(v,PreARG (Z.of_N s)));
     _ <- SetOperand lo v;
          SetOperand hi vh
-  | (Syntax.mul | imul), [src2] =>
+  | Syntax.mul, [src2] =>
     let src1 : ARG := rax in
     v  <- Symeval (mulZ@(src1,src2));
     vh <- Symeval (shrZ@(v,PreARG (Z.of_N s)));
@@ -4309,6 +4328,22 @@ Definition SymexNormalInstruction {opts : symbolic_options_computed_opt} {descr:
     _ <- SetOperand (lo:ARG) v;
     _ <- SetOperand (hi:ARG) vh;
     HavocFlags (* This is conservative and can be made more precise *)
+  | imul, [src2] =>
+    (* One-operand [imul] is a *signed* widening multiply (Intel SDM Vol. 2A,
+       IMUL): rdx:rax (ah:al for s = 8) := signed(rax) * signed(src2).  The low
+       half agrees with the unsigned product, but the high half does not
+       whenever an operand has its top bit set, so it must not share the
+       unsigned [mul] branch above. *)
+    let src1 : ARG := rax in
+    v  <- Symeval (mulZ@(src1,src2));
+    vh <- SignedMulHigh src1 src2;
+    lo <- resize_reg rax;
+    hi <- (if (s =? 8)%N
+           then ret ah
+           else resize_reg rdx);
+    _ <- SetOperand (lo:ARG) v;
+    _ <- SetOperand (hi:ARG) vh;
+    HavocFlags (* This is conservative and can be made more precise *)
   | Syntax.shl, [dst; cnt] =>
     let cnt := andZ@(cnt, (PreApp (const (Z.of_N s-1)%Z) nil)) in
     v <- Symeval (shl s@(dst, cnt));

src/Assembly/WithBedrock/Semantics.v

@@ -245,7 +245,7 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
     let v := v1 * v2 in
     st <- SetOperand sa s st lo v;
     SetOperand sa s st hi (Z.shiftr v (Z.of_N s))
-  | (Syntax.mul | imul), [src2] =>
+  | Syntax.mul, [src2] =>
     let src1 : ARG := rax in
     v1 <- DenoteOperand sa s st src1;
     v2 <- DenoteOperand sa s st src2;
@@ -257,6 +257,24 @@ Definition DenoteNormalInstruction (st : machine_state) (instr : NormalInstructi
     st <- SetOperand sa s st lo v;
     st <- SetOperand sa s st hi (Z.shiftr v (Z.of_N s));
     Some (HavocFlags st) (* conservative *)
+  | imul, [src2] =>
+    (* One-operand [imul] is a *signed* widening multiply (Intel SDM Vol. 2A,
+       IMUL): rdx:rax (ah:al for s = 8) := signed(rax) * signed(src2).  The low
+       half agrees with the unsigned product [v1 * v2], but the high half does
+       not whenever an operand has its top bit set, so it must not share the
+       unsigned [mul] branch above. *)
+    let src1 : ARG := rax in
+    v1 <- DenoteOperand sa s st src1;
+    v2 <- DenoteOperand sa s st src2;
+    let v := v1 * v2 in
+    let vs := Z.signed s v1 * Z.signed s v2 in
+    lo <- resize_reg rax;
+    hi <- (if (s =? 8)%N
+           then Some ah
+           else resize_reg rdx);
+    st <- SetOperand sa s st lo v;
+    st <- SetOperand sa s st hi (Z.land (Z.shiftr vs (Z.of_N s)) (Z.ones (Z.of_N s)));
+    Some (HavocFlags st) (* conservative *)
   | imul, ([src1 as dst; src2] | [dst; src1; src2]) =>
     v1 <- DenoteOperand sa s st src1;
     v2 <- DenoteOperand sa s st src2;

src/Assembly/WithBedrock/SemanticsTests.v

@@ -0,0 +1,108 @@
+(** Regression tests for the semantics of one-operand [mul] and [imul].
+
+    The one-operand form of [imul] is a *signed* widening multiply
+    (rdx:rax := signed(rax) * signed(src)), whereas [mul] is unsigned.  The
+    two agree on the low half of the product but not on the high half
+    whenever an operand has its top bit set.  The concrete semantics
+    ([Semantics.DenoteNormalInstruction]) and the symbolic executor
+    ([Symbolic.SymexNormalInstruction]) used to share a single unsigned
+    branch for both mnemonics (scrutineer finding #2514); these tests pin
+    down the hardware behaviour for both models, on the same inputs.
+
+    The expected values were obtained by executing the instructions on
+    x86-64 hardware. *)
+From Coq Require Import ZArith.
+From Coq Require Import List.
+From Coq Require Import String.
+Require Import Crypto.Util.ErrorT.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Assembly.Syntax.
+Require Import Crypto.Assembly.Symbolic.
+Require Import Crypto.Assembly.Equivalence.
+Require Import Crypto.Assembly.WithBedrock.Semantics.
+Require Import coqutil.Map.Interface.
+Import ListNotations.
+Local Open Scope Z_scope.
+Local Open Scope list_scope.
+Local Open Scope string_scope.
+
+(** ** Concrete semantics *)
+
+Definition initial_machine_state (rax_val rcx_val : Z) : machine_state
+  := {| machine_reg_state := Semantics.set_reg (Semantics.set_reg (Tuple.repeat 0 _) rax rax_val) rcx rcx_val
+      ; machine_flag_state := havoc_flags
+      ; machine_mem_state := map.empty |}.
+
+Definition denote_one (instr : NormalInstruction) (rax_val rcx_val : Z) (out : REG) : option Z
+  := option_map (fun st : machine_state => Semantics.get_reg st out) (DenoteNormalInstruction (initial_machine_state rax_val rcx_val) instr).
+
+Definition mul_rcx  : NormalInstruction := {| Syntax.prefix := None ; Syntax.op := Syntax.mul  ; Syntax.args := [reg rcx] |}.
+Definition imul_rcx : NormalInstruction := {| Syntax.prefix := None ; Syntax.op := Syntax.imul ; Syntax.args := [reg rcx] |}.
+Definition mul_cl   : NormalInstruction := {| Syntax.prefix := None ; Syntax.op := Syntax.mul  ; Syntax.args := [reg cl] |}.
+Definition imul_cl  : NormalInstruction := {| Syntax.prefix := None ; Syntax.op := Syntax.imul ; Syntax.args := [reg cl] |}.
+
+(** rax = 0xffffffff00000001 (the top limb of the P-256 prime; bit 63 set), rcx = 3 *)
+Example denote_mul_rcx_hi  : denote_one mul_rcx  0xffffffff00000001 3 rdx = Some 0x2.                Proof. vm_compute; reflexivity. Qed.
+Example denote_mul_rcx_lo  : denote_one mul_rcx  0xffffffff00000001 3 rax = Some 0xfffffffd00000003. Proof. vm_compute; reflexivity. Qed.
+Example denote_imul_rcx_hi : denote_one imul_rcx 0xffffffff00000001 3 rdx = Some 0xffffffffffffffff. Proof. vm_compute; reflexivity. Qed.
+Example denote_imul_rcx_lo : denote_one imul_rcx 0xffffffff00000001 3 rax = Some 0xfffffffd00000003. Proof. vm_compute; reflexivity. Qed.
+
+(** both operands with bit 63 set: rax = -2, rcx = -2^63+1 as signed values *)
+Example denote_mul_rcx_hi'  : denote_one mul_rcx  0xfffffffffffffffe 0x8000000000000001 rdx = Some 0x7fffffffffffffff. Proof. vm_compute; reflexivity. Qed.
+Example denote_imul_rcx_hi' : denote_one imul_rcx 0xfffffffffffffffe 0x8000000000000001 rdx = Some 0x0.                Proof. vm_compute; reflexivity. Qed.
+Example denote_mul_rcx_lo'  : denote_one mul_rcx  0xfffffffffffffffe 0x8000000000000001 rax = Some 0xfffffffffffffffe. Proof. vm_compute; reflexivity. Qed.
+Example denote_imul_rcx_lo' : denote_one imul_rcx 0xfffffffffffffffe 0x8000000000000001 rax = Some 0xfffffffffffffffe. Proof. vm_compute; reflexivity. Qed.
+
+(** no top bit set: signed and unsigned agree *)
+Example denote_mul_rcx_hi''  : denote_one mul_rcx  0x123456789 0x23456789a rdx = Some 0x2. Proof. vm_compute; reflexivity. Qed.
+Example denote_imul_rcx_hi'' : denote_one imul_rcx 0x123456789 0x23456789a rdx = Some 0x2. Proof. vm_compute; reflexivity. Qed.
+
+(** 8-bit form writes ah:al; al = 0xff (-1), cl = 3 *)
+Example denote_mul_cl_ah  : denote_one mul_cl  0xff 3 ah = Some 0x2.  Proof. vm_compute; reflexivity. Qed.
+Example denote_mul_cl_al  : denote_one mul_cl  0xff 3 al = Some 0xfd. Proof. vm_compute; reflexivity. Qed.
+Example denote_imul_cl_ah : denote_one imul_cl 0xff 3 ah = Some 0xff. Proof. vm_compute; reflexivity. Qed.
+Example denote_imul_cl_al : denote_one imul_cl 0xff 3 al = Some 0xfd. Proof. vm_compute; reflexivity. Qed.
+(** the untouched upper bytes of rax are preserved *)
+Example denote_imul_cl_rax : denote_one imul_cl 0x11223344556677ff 3 rax = Some 0x112233445566fffd. Proof. vm_compute; reflexivity. Qed.
+
+(** ** Symbolic executor *)
+
+Local Instance test_symbolic_options : symbolic_options_computed_opt
+  := {| asm_rewriting_passes := default_rewriting_passes (rewriting_pipeline:=default_rewrite_pass_order) (rewriting_pass_filter:=fun _ => true)
+      ; asm_debug_symex_asm_first_computed := false
+      ; asm_node_reveal_depth_computed := default_node_reveal_depth |}.
+
+(** Symbolically execute [instr] from a state where every register holds a
+    fresh symbol, then evaluate the requested output register with the
+    symbols for [rax] and [rcx] instantiated to the given values (and every
+    other register to [0]). *)
+Definition symex_one (instr : NormalInstruction) (rax_val rcx_val : Z) (out : REG) : option Z
+  := let st := init_symbolic_state dag.empty in
+     let ctx : symbol -> option Z
+       := fun n => if (n =? reg_index rax)%N then Some rax_val
+                   else if (n =? reg_index rcx)%N then Some rcx_val
+                        else Some 0 in
+     match (_ <- SymexNormalInstruction (descr:=Build_description "SemanticsTests" true) instr;
+            GetReg (descr:=Build_description "SemanticsTests" true) out)%x86symex st with
+     | Success (i, st) => interp_expr ctx (reveal st 100 i)
+     | Error _ => None
+     end.
+
+Example symex_mul_rcx_hi  : symex_one mul_rcx  0xffffffff00000001 3 rdx = Some 0x2.                Proof. vm_compute; reflexivity. Qed.
+Example symex_mul_rcx_lo  : symex_one mul_rcx  0xffffffff00000001 3 rax = Some 0xfffffffd00000003. Proof. vm_compute; reflexivity. Qed.
+Example symex_imul_rcx_hi : symex_one imul_rcx 0xffffffff00000001 3 rdx = Some 0xffffffffffffffff. Proof. vm_compute; reflexivity. Qed.
+Example symex_imul_rcx_lo : symex_one imul_rcx 0xffffffff00000001 3 rax = Some 0xfffffffd00000003. Proof. vm_compute; reflexivity. Qed.
+
+Example symex_mul_rcx_hi'  : symex_one mul_rcx  0xfffffffffffffffe 0x8000000000000001 rdx = Some 0x7fffffffffffffff. Proof. vm_compute; reflexivity. Qed.
+Example symex_imul_rcx_hi' : symex_one imul_rcx 0xfffffffffffffffe 0x8000000000000001 rdx = Some 0x0.                Proof. vm_compute; reflexivity. Qed.
+Example symex_mul_rcx_lo'  : symex_one mul_rcx  0xfffffffffffffffe 0x8000000000000001 rax = Some 0xfffffffffffffffe. Proof. vm_compute; reflexivity. Qed.
+Example symex_imul_rcx_lo' : symex_one imul_rcx 0xfffffffffffffffe 0x8000000000000001 rax = Some 0xfffffffffffffffe. Proof. vm_compute; reflexivity. Qed.
+
+Example symex_mul_rcx_hi''  : symex_one mul_rcx  0x123456789 0x23456789a rdx = Some 0x2. Proof. vm_compute; reflexivity. Qed.
+Example symex_imul_rcx_hi'' : symex_one imul_rcx 0x123456789 0x23456789a rdx = Some 0x2. Proof. vm_compute; reflexivity. Qed.
+
+Example symex_mul_cl_ah  : symex_one mul_cl  0xff 3 ah = Some 0x2.  Proof. vm_compute; reflexivity. Qed.
+Example symex_mul_cl_al  : symex_one mul_cl  0xff 3 al = Some 0xfd. Proof. vm_compute; reflexivity. Qed.
+Example symex_imul_cl_ah : symex_one imul_cl 0xff 3 ah = Some 0xff. Proof. vm_compute; reflexivity. Qed.
+Example symex_imul_cl_al : symex_one imul_cl 0xff 3 al = Some 0xfd. Proof. vm_compute; reflexivity. Qed.
+Example symex_imul_cl_rax : symex_one imul_cl 0x11223344556677ff 3 rax = Some 0x112233445566fffd. Proof. vm_compute; reflexivity. Qed.

src/Assembly/WithBedrock/SymbolicProofs.v

@@ -1110,7 +1110,7 @@ Lemma SymexNornalInstruction_R {opts : symbolic_options_computed_opt} {descr:des
   exists m', Semantics.DenoteNormalInstruction m instr = Some m' /\ R s' m' /\ s :< s'.
 Proof using Type.
   intros [] s' H.
-  case instr as [op args]; cbv [SymexNormalInstruction OperationSize] in H.
+  case instr as [op args]; cbv [SymexNormalInstruction SignedMulHigh OperationSize] in H.
   repeat (repeat destruct_one_match_hyp; repeat step01).
 
   all : repeat
@@ -1361,6 +1361,10 @@ Proof using Type.
   Unshelve. all : match goal with H : context[push] |- _ => idtac | H : context[pop] |- _ => idtac | _ => shelve end; shelve_unifiable.
   all: rewrite !Z.land_ones by lia; push_Zmod; pull_Zmod; f_equal; lia.
 
+  Unshelve. all : match goal with H : context[Syntax.imul] |- _ => idtac | _ => shelve end; shelve_unifiable.
+  (* one-operand imul: the symbolic sign extension [(x + 2^(s-1)) land ones s - 2^(s-1)] is [Z.signed s x] unfolded *)
+  all: cbv [Z.signed]; rewrite ?Z.add_opp_r, ?(Z.add_comm _ (Z.shiftl 1 _)); reflexivity.
+
   Unshelve. all: shelve_unifiable.
   all: fail_if_goals_remain ().
 Qed.