x86 lowering: use XOR instead of MOV 0 in division

There seem to be no good reason not to use “xor edx, edx” to set the
highest word to zero. The encoding is shorter and flags are obliterated
by the following DIV instruction.

CHANGELOG.md

@@ -56,6 +56,9 @@
   ([PR #531](https://github.com/jasmin-lang/jasmin/pull/531);
   fixes [#525](https://github.com/jasmin-lang/jasmin/issues/525)).
 
+- Unsigned division on x86 emits a xor instead of “mov 0“
+  ([PR #582](https://github.com/jasmin-lang/jasmin/pull/582)).
+
 # Jasmin 2023.06.1 — 2023-07-31
 
 ## New features

proofs/compiler/x86_lowering.v

@@ -504,7 +504,7 @@ Definition lower_cassgn (ii:instr_info) (x: lval) (tg: assgn_tag) (ty: stype) (e
     let i1 :=
       match s with
       | Signed => Copn [:: Lvar c ] tg (Ox86 (CQO sz)) [:: a]
-      | Unsigned => Copn [:: Lvar c ] tg (Ox86 (MOV sz)) [:: Papp1 (Oword_of_int sz) (Pconst 0)]
+      | Unsigned => Copn [:: f ; f ; f ; f ; f ; Lvar c ] tg (Oasm (ExtOp (Oset0 sz))) [::]
       end in
 
     [::MkI ii i1; MkI ii (Copn lv tg op [::Plvar c; a; b]) ]

proofs/compiler/x86_lowering_proof.v

@@ -1406,8 +1406,8 @@ Section PROOF.
               /check_size_16_64 hle1 hle2 /= write_var_eq_type //.
         + by rewrite get_var_eq //= cmp_le_refl orbT.
         + by split => //; apply vmap_eq_except_set; apply multiplicand_in_fv.
-        + by apply: EmkI;  apply: Eopn; rewrite /sem_sopn /exec_sopn /sopn_sem /= truncate_word_u /=
-               /x86_MOV /check_size_8_64 hle2 /= write_var_eq_type.
+        + by apply: EmkI; apply: Eopn; rewrite /sem_sopn /exec_sopn /sopn_sem /=
+                                         /Oset0_instr hle2 /= write_var_eq_type.
         + by rewrite /= get_var_eq /= cmp_le_refl orbT ?wrepr0.
         split => //.
         by apply vmap_eq_except_set; apply multiplicand_in_fv.