add back multiplication to make the fiat-crypto backend possible

bedrock2/src/bedrock2/BasicCSyntax.v

@@ -14,6 +14,10 @@ Definition to_c_parameters : ToCString.parameters := {|
              match op with
              | add => e1++"+"++e2
              | sub => e1++"-"++e2
+             | mul => e1++"*"++e2
+             | mulhuu => "sizeof(intptr_t) == 4 ? ((uint64_t)"++e1++"*"++e2++")>>32 : ((__uint128_t)"++e1++"*"++e2++")>>64 /* TODO this has not been tested */"
+             | divu => e1++"/"++e2
+             | remu => e1++"%"++e2
              | and => e1++"&"++e2
              | or => e1++"|"++e2
              | xor => e1++"^"++e2

bedrock2/src/bedrock2/Semantics.v

@@ -71,6 +71,10 @@ Section binops.
     match bop with
     | bopname.add => word.add
     | bopname.sub => word.sub
+    | bopname.mul => word.mul
+    | bopname.mulhuu => word.mulhuu
+    | bopname.divu => word.divu
+    | bopname.remu => word.modu
     | bopname.and => word.and
     | bopname.or => word.or
     | bopname.xor => word.xor

bedrock2/src/bedrock2/Syntax.v

@@ -3,7 +3,7 @@ Require Coq.Strings.String.
 Require Import Coq.Numbers.BinNums.
 
 Module Import bopname.
-  Inductive bopname := add | sub | and | or | xor | sru | slu | srs | lts | ltu | eq.
+  Inductive bopname := add | sub | mul | mulhuu | divu | remu | and | or | xor | sru | slu | srs | lts | ltu | eq.
 End bopname.
 Notation bopname := bopname.bopname.
 

compiler/src/compiler/FlatToRiscvDef.v

@@ -118,6 +118,10 @@ Section FlatToRiscv1.
     match op with
     | Syntax.bopname.add => [[Add rd rs1 rs2]]
     | Syntax.bopname.sub => [[Sub rd rs1 rs2]]
+    | Syntax.bopname.mul => [[Mul rd rs1 rs2]]
+    | Syntax.bopname.mulhuu => [[Mulhu rd rs1 rs2]]
+    | Syntax.bopname.divu => [[Divu rd rs1 rs2]]
+    | Syntax.bopname.remu => [[Remu rd rs1 rs2]]
     | Syntax.bopname.and => [[And rd rs1 rs2]]
     | Syntax.bopname.or  => [[Or  rd rs1 rs2]]
     | Syntax.bopname.xor => [[Xor rd rs1 rs2]]