adding shl shlx to mul * imm

[dderjoel]

This adds two example files using different instructions to multiply by constants using lea / shl / shlx.
Also it enables the parser to parse those new instructions, but it is still unable to unify.
I think this is because it does not know that a + a == 2*a == 2<<1 and a * 19 == a + 2 * (8a + a), a * 2 * 2 == a * 4 ...
Also I'd need some pointers to parse MEM with scaled index, i.e. [ reg + N * reg ]; N being 2, 4, 8.

[JasonGross]

Also I'd need some pointers to parse MEM with scaled index, i.e. [ reg + N * reg ]; N being 2, 4, 8.

First, you need to update the representation of memory addresses to support this at

fiat-crypto/src/Assembly/Syntax.v

Line 26 in e612a32

Record MEM := { mem_is_byte : bool ; mem_reg : REG ; mem_extra_reg : option REG ; mem_offset : option Z }.

Presumably you want to change mem_extra_reg to be option (Z * REG)?

Then you want to change printing of this at

fiat-crypto/src/Assembly/Parse.v

Lines 268 to 286 in e612a32

	Global Instance show_lvl_MEM : ShowLevel MEM
	:= fun m
	=> (if m.(mem_is_byte) then show_lvl_app (fun 'tt => "byte") else show_lvl)
	(fun 'tt
	=> "[" ++ (show m.(mem_reg))
	++ (match m.(mem_extra_reg) with
	| None => ""
	| Some r => " + " ++ show r
	end)
	++ (match m.(mem_offset) with
	| None => ""
	| Some offset
	=> (if offset <? 0 then " - " else " + ")
	++ (let offset := Z.abs offset in
	if (Z.modulo offset 8 =? 0)%Z
	then "0x08 * " ++ Decimal.show_Z (offset / 8)
	else Hex.show_Z offset)
	end%Z)
	++ "]").

Then you want to update the parser combinator expression at

fiat-crypto/src/Assembly/Parse.v

Lines 173 to 189 in e612a32

	Definition parse_MEM : ParserAction MEM
	:= parse_map
	(fun '(has_byte, (r, (r', maybe_pm_z)))
	=> {| mem_is_byte := if has_byte:option _ then true else false
	; mem_reg := r
	; mem_extra_reg := r'
	; mem_offset := match maybe_pm_z with
	| inl (inl _ (* plus *), z) => Some z
	| inl (inr _ (* minus *), z) => Some (-z)
	| inr _ (* only whitespace *) => None
	end%Z |})
	(((strip_whitespace_after "byte ")?) ;;
	(strip_whitespace_after "[" ;;R
	parse_REG ;;
	((strip_whitespace_around "+" ;;R parse_REG)?) ;;
	((strip_whitespace_before ("+" ||->{id} "-") ;; parse_Z_arith_strict) ||->{id} parse_any_whitespace) ;;L
	"]")).

probably changing

fiat-crypto/src/Assembly/Parse.v

Line 187 in e612a32

((strip_whitespace_around "+" ;;R parse_REG)?) ;;

to something like

((strip_whitespace_around ("+" ||->{id} "-") ;; (parse_Z_arith_strict ;;L strip_whitespace_around "*")? ;; parse_REG)?) ;; 

Note that it's important to not have overlapping options for parsing whitespace, otherwise we end up with exponentially many possible parses. Roughly this line says "start with a + or - (and just give the string + string result transformed by id), then optionally (postfix ?) take a Z arithmetic expression followed by a * with maybe whitespace (and drop the * and whitespace in the parse result; the L in ;;L means 'only care about the left result'), and then parse a register".
Then you need to change

fiat-crypto/src/Assembly/Parse.v

Line 178 in e612a32

; mem_extra_reg := r'

to pull out the + or - and the optional Z and the register and combine them into the right representation.

Let me know if you have any trouble with this.

[JasonGross]

I think this is because it does not know that a + a == 2*a == 2<<1 and a * 19 == a + 2 * (8a + a), a * 2 * 2 == a * 4 ...

Do you mean a << 1 instead of 2 << 1?

@andres-erbsen do you have thoughts on encoding this into the canonicalizer? Presumably we want a variant of

fiat-crypto/src/Assembly/Symbolic.v

Lines 1137 to 1152 in 77731c4

	Definition consts_commutative :=
	fun e => match e with
	ExprApp (o, args) =>
	(* note: removing the next line makes tests fail *)
	if (match o with mul _ => true | _ => false end) then e else
	if commutative o then
	let csts_exprs := List.partition isCst args in
	if associative o
	then match interp0_expr (ExprApp (o, fst csts_exprs)) with
	| Some v => ExprApp (o, ExprApp (const v, nil):: snd csts_exprs)
	| _ => ExprApp (o, fst csts_exprs ++ snd csts_exprs)
	end
	else ExprApp (o, fst csts_exprs ++ snd csts_exprs)
	else e | _ => e end.
	Global Instance consts_commutative_ok : Ok consts_commutative.

that uses something like Haskell's groupBy on node equality or something? Maybe we can add a "groups_by" typeclass like associative or identity, which says for each associative commutative operation how to turn an n-fold operation on identical arguments into a single operation on n and the argument? I guess we need a two-step version of grouping, where we decompose each argument that's a product into the number of copies that it is?

[JasonGross]

2*a == a<<1

This one should be easy, just add a pass that unconditionally rewrites shifts by constants into multiplications

a * 2 * 2 == a * 4

Are you sure this one isn't already handled? I think it should be handled already. (If not, what's the error message?)

[dderjoel]

a * 2 * 2 == a * 4

Are you sure this one isn't already handled? I think it should be handled already. (If not, what's the error message?)

see commit 1ee484e;
end of the error message is:

Unable to unify: [inr [2110, 2114, 2113, 2045, 2055, 2065, 2075, 2086, 2096]] == [inr [569, 574, 576, 485, 499, 513, 527, 541, 558]]
Could not unify the values at index 0: [2110, 2114, 2113, 2045, 2055, 2065, 2075, 2086, 2096] != [569, 574, 576, 485, 499, 513, 527, 541, 558]
index 0: 2110 != 569
(slice 0 58, [2103]) != (slice 0 58, [559])
index 0: 2103 != 559                                                                                                                                     nul
(add 64, [2013, 2100]) != (add 64, [251, 554])
index 0: 2013 != 251
(slice 0 58, [2008]) != (slice 0 58, [235])                                                                                                              nul
index 0: 2008 != 235
(add 64, [106, 126, 150, 214, 1969]) != (add 64, [90, 106, 126, 150, 214])
index 0: 106 != 90
(mul 64, [2, 5, 10, 10]) != (mul 64, [3, 4, 10, 10])
index 0: 2 != 3
(old 64 2, []) != (old 64 3, [])
(old 64 2, []) != (old 64 3, [])
Operation mismatch: old 64 2 != old 64 3
2 is a special value no longer present in the symbolic machine state at the end of execution.
3 is a special value no longer present in the symbolic machine state at the end of execution.

Fatal error: exception Failure("Synthesis failed")

I don't really understand the old part; is that some kind of helper thing operation?

Do you mean a << 1 instead of 2 << 1?

yes, that's what I meant. My bad.

For the rest, I'll have a go on the Memory-adjustments, and for the *2 == <<1 I think @andres-erbsen will help out, or is that something, that I would want to look into, too ?

[JasonGross]

I don't really understand the old part; is that some kind of helper thing operation?

Could you rebase on top of #1125 and give me the error message after this? The old part is a red herring; roughly this means that you're comparing non-equal input arguments, but the real issue with (add 64, [106, 126, 150, 214, 1969]) != (add 64, [90, 106, 126, 150, 214]) is not that 90 != 106, but that 1969 != 90. #1125 compares argument lists of commutative operations modulo commutativity, so we should get a better error message here.

[JasonGross]

@dderjoel
File "./src/Assembly/WithBedrock/Semantics.v", line 158, characters 0-7741:
Error: Non exhaustive pattern-matching: no clause found for patterns shl, _
(Note that bedrock2-dependent files only build when you're running on a sufficiently new version of Coq)

[dderjoel]

rebased_on_better_errors.txt

Could you rebase on top of #1125 and give me the error message after this?
sure thing

Unable to unify: [inr [2110, 2114, 2113, 2045, 2055, 2065, 2075, 2086, 2096]] == [inr [569, 574, 576, 485, 499, 513, 527
Could not unify the values at index 0: [2110, 2114, 2113, 2045, 2055, 2065, 2075, 2086, 2096] != [569, 574, 576, 485, 49
index 0: 2110 != 569
(slice 0 58, [2103]) != (slice 0 58, [559])
index 0: 2103 != 559
(add 64, [2013, 2100]) != (add 64, [251, 554])
index 0: 2013 != 251
(slice 0 58, [2008]) != (slice 0 58, [235])
index 0: 2008 != 235
(add 64, [106, 126, 150, 214, 1969]) != (add 64, [90, 106, 126, 150, 214])
index 4: 1969 != 90
(mul 64, [3, 4, 1964]) != (mul 64, [3, 4, 10, 10])
index 2: 1964 != 10
(const 4, []) != (const 2, [])
(const 4, []) != (const 2, [])
Operation mismatch: const 4 != const 2

Fatal error: exception Failure("Synthesis failed")

Edit: full error in attached file

dderjoel
File "./src/Assembly/WithBedrock/Semantics.v", line 158, characters 0-7741:
Error: Non exhaustive pattern-matching: no clause found for patterns shl, _
(Note that bedrock2-dependent files only build when you're running on a sufficiently new version of Coq)

I must admit that I have trouble with the coq-version and ocaml versions on my system (or had, Can't really remember) And I am just happy that I can compile with SKIP_BEDROCK2=1 make standalone-ocaml

But what that error means, is that the matches that I've put into the Symbolic.v I also need to put into WithBedrock/Semantics.v? (Which for me will mostly be copy-adjust-paste-hope-that-it'll-compile)

[JasonGross]

But what that error means, is that the matches that I've put into the Symbolic.v I also need to put into WithBedrock/Semantics.v? (Which for me will mostly be copy-adjust-paste-hope-that-it'll-compile)

That's roughly right, though you need to describe how it acts on concrete machine state rather than symbolic state.

[JasonGross]

a * 2 * 2 == a * 4

Are you sure this one isn't already handled? I think it should be handled already. (If not, what's the error message?)

Hrm, I guess we explicitly disable this equivalence

fiat-crypto/src/Assembly/Symbolic.v

Lines 1140 to 1141 in e151e21

	(* note: removing the next line makes tests fail *)
	if (match o with mul _ => true | _ => false end) then e else

@andres-erbsen Do you know what's up with this?

[JasonGross]

I've created #1127 to enable constfolding on mul, let's see how it works

[dderjoel]

I've created #1127 to enable constfolding on mul, let's see how it works

I rebased on that one, and the test file (from commit 1ee484e) can now be proven correct.

[JasonGross]

and for the *2 == <<1 I think @andres-erbsen will help out, or is that something, that I would want to look into, too ?

I think both of us would prefer if you take a stab at it, but either of us can probably help out if need be.

[dderjoel]

Let me know if you have any trouble with this.

I think I have something for the syntax and parsing ; but I am struggling with the parser combinator expression.
I understand that with ; mem_extra_reg := r' a MEM object is build and in this case it is a "mem with an extra register" (as apposed to [rsp] or [rsp + offset] and for that mem_extra_reg I need that second register named r'.
And now I want this object also to have that z in there, but I don't know which part is declaring that variable, and how I'd access it, and where to put the data, and where to tell it that 4*RAX means (multiply rax 4).

When changing mem_extra_reg to option (Z*REG), cocq complains in Assembly/Equality.v

COQC src/Assembly/Equality.v
File "./src/Assembly/Equality.v", line 52, characters 29-46:
Error:
In environment
x : MEM
y : MEM
The term "mem_extra_reg x" has type "option (Z * REG)"
while it is expected to have type "option REG".

The code there is:
&& (option_beq REG_beq x.(mem_extra_reg) y.(mem_extra_reg))
and I assume REG_beq can check if two regs are the same, but since mem_exra_reg is not a single reg anymore, I need to also check that z is equal. A Similar check is done in the line after with Z.eqb, but first, how do I access the reg in that line from the mem_extra_reg-type?

2*a == a<<1

This one should be easy, just add a pass that unconditionally rewrites shifts by constants into multiplications

Where would I add such a pass? That is not in the Assembly-part I assume.

[JasonGross]

The code there is:
&& (option_beq REG_beq x.(mem_extra_reg) y.(mem_extra_reg))
and I assume REG_beq can check if two regs are the same, but since mem_exra_reg is not a single reg anymore, I need to also check that z is equal. A Similar check is done in the line after with Z.eqb, but first, how do I access the reg in that line from the mem_extra_reg-type?

You want something like prod_beq Z.eqb REG_beq instead of just REG_beq, to get boolean equality on Z * REG instead of REG. You may need some extra underscores for type variables that are not implicit.

And now I want this object also to have that z in there, but I don't know which part is declaring that variable, and how I'd access it, and where to put the data, and where to tell it that 4*RAX means (multiply rax 4).

It sounds like you already succeeded at the variable declaration part (adjusting the record). You put the data in mem_extra_reg and access it from there as well with match, let, or fst and snd (maybe I'm misunderstanding your question though?). You tell it the meaning in Semantics.v; if you just follow the type errors from changing the record, you should find almost everything you need to change (you might need to handle show separately, since it uses typeclasses and might happily allow you to change types without erroring).

Where would I add such a pass? That is not in the Assembly-part I assume.

It should be added to the list

fiat-crypto/src/Assembly/Symbolic.v

Lines 1370 to 1394 in af618d3

	Definition expr : expr -> expr :=
	List.fold_left (fun e f => f e)
	[constprop
	;slice0
	;slice01_addcarryZ
	;slice01_subborrowZ
	;set_slice_set_slice
	;slice_set_slice
	;set_slice0_small
	;flatten_associative
	;consts_commutative
	;fold_consts_to_and
	;drop_identity
	;opcarry_0_at1
	;opcarry_0_at3
	;opcarry_0_at2
	;unary_truncate
	;truncate_small
	;addoverflow_bit
	;addcarry_bit
	;addcarry_small
	;addoverflow_small
	;addbyte_small
	;xor_same
	].

[dderjoel]

You want something like prod_beq Z.eqb REG_beq instead of just REG_beq, to get boolean equality on Z * REG instead of REG. You may need some extra underscores for type variables that are not implicit.

okay, using && (Prod.prod_beq _ _ Z.eqb REG_beq x.(mem_extra_reg) y.(mem_extra_reg)) cocq complains with

> The term "mem_extra_reg x" has type "option (Z * REG)"
while it is expected to have type "(Z * REG)%type".

which, fair enough, makes sense. But the type cannot be non-option (i assume that mean optional) because there might not be an Z, let alone a Z * REG.
But as I couldn't find an Prod.prod_option_beq, I am thinking of getting the Z and reg and then falling back to option_beq.

   && (
       xr <- GetReg x.(mem_extra_reg);
       yr <- GetReg y.(mem_extra_reg);
      xz <- RevealConst x.(mem_extra_reg);
       yz <- RevealConst y.(mem_extra_reg);
       req <- (option_beq REG_beq xr yr);
      zeq <- (option_beq Z.beq xz yz);
       req && zeq
   )

But, probably unsurprisingly, that does not work.
Error: Unknown interpretation for notation "_ <- _ ; _".

All this syntax is so confusing to me, and since you suggested the Prod.prod_beq, I think that this long approach is not the way to go anyway.

Where would I add such a pass? That is not in the Assembly-part I assume.

It should be added to the list

fiat-crypto/src/Assembly/Symbolic.v

Lines 1370 to 1394 in af618d3

	Definition expr : expr -> expr :=
	List.fold_left (fun e f => f e)
	[constprop
	;slice0
	;slice01_addcarryZ
	;slice01_subborrowZ
	;set_slice_set_slice
	;slice_set_slice
	;set_slice0_small
	;flatten_associative
	;consts_commutative
	;fold_consts_to_and
	;drop_identity
	;opcarry_0_at1
	;opcarry_0_at3
	;opcarry_0_at2
	;unary_truncate
	;truncate_small
	;addoverflow_bit
	;addcarry_bit
	;addcarry_small
	;addoverflow_small
	;addbyte_small
	;xor_same
	].

uff. I don't even know where to start there. I am having a hard time understanding what is going on in those passes. Are they all rewriting? I can't find any that looks like anything I'd need for this shl->mul rewrite, But also I don't know what I am looking for. And does it make a difference it it is shl or shlx ? I think that this is on the shlZ level I think, and at that point it should maybe not matter?

[JasonGross]

okay, using && (Prod.prod_beq _ _ Z.eqb REG_beq x.(mem_extra_reg) y.(mem_extra_reg)) cocq complains with

You forgot to keep the option_beq; you want && (option_beq (Prod.prod_beq _ _ Z.eqb REG_beq) x.(mem_extra_reg) y.(mem_extra_reg)). (But please insert Require Import Crypto.Util.Prod near the top of the file so you don't need to qualify prod_beq.)

uff. I don't even know where to start there. I am having a hard time understanding what is going on in those passes. Are they all rewriting?

Yes

I can't find any that looks like anything I'd need for this shl->mul rewrite, But also I don't know what I am looking for.

Try starting with this (untested):

Definition shift_to_mul :=
  fun e => match e with
    ExprApp ((shl | shlx | shlZ) as o, [e'; ExprApp (const v, [])]) =>
      let o' := match o with shl | shlx => mul 64%N | shlZ => mulZ | _ => o (* impossible *) end in
      if Z.eqb v 0
      then e'
      else if Z.ltb 0 v
      then ExprApp (o', [e'; ExprApp (const (2^v)%Z, [])])
      else e | _ => e end.
Global Instance shift_to_mul_ok : Ok shift_to_mul_small.
Proof. t. cbn in *. firstorder (lia + eauto). Qed.

And does it make a difference it it is shl or shlx ?

What's the difference between these two (in assembly land)?

I think that this is on the shlZ level I think, and at that point it should maybe not matter?

What do you mean?

[JasonGross]

And does it make a difference it it is shl or shlx ?

I think you're right that it probably does not matter at this level, but you might need to add something that deals with the flags. The Ok proof will tell you whether or not you need to care; if you can prove Ok, then you're fine.

[dderjoel]

to something like

((strip_whitespace_around ("+" ||->{id} "-") ;; (parse_Z_arith_strict ;;L strip_whitespace_around "*")? ;; parse_REG)?) ;; 

Note that it's important to not have overlapping options for parsing whitespace, otherwise we end up with exponentially many possible parses. Roughly this line says "start with a + or - (and just give the string + string result transformed by id), then optionally (postfix ?) take a Z arithmetic expression followed by a * with maybe whitespace (and drop the * and whitespace in the parse result; the L in ;;L means 'only care about the left result'), and then parse a register". Then you need to change

I think I start to understand Parse.v. We define that function which takes arguments (has_byte, (r, (r', maybe_pm_z))) and we call that function instantly with the argument list below, separated by ;;. And MEM is a Record (in c it would be a struct`)

Okay. We have an issue then.
we need to be able to parse the following:

1. [reg] (for mov reg, [rsp])
2. [reg +/- z ] (for mov reg, [rsp +- 0x8], spills to memory)
3. [reg + reg] (for lea reg, [reg + reg], to calculate *2)
4. [z * reg] (for lea reg, [2/4/8 * reg], to calculate *2, *4, *8)
5. [reg + z * reg] (for lea reg, [reg + 2*reg] to calculate *3, *5, *9)

so the issue is, that the 4. makes mem_reg optional, but I am hesitant to change that in the record (I expect severe impacts on the rest of the code to then need to always check if mem_reg is actually there.

My question is, if a parse_REG for 4. would be able to parse the reg-part although it has that z* in front of it. But even then, reg would become mem_reg and I'd have no spot to store the z part.

So now I'm thinking to change the Record MEM to Record MEM := { mem_is_byte : bool ; mem_reg : REG ; mem_extra_reg : option REG ; mem_scale: option Z ; mem_offset : option Z }. with the semantics, that when there is a scale, it always scales the mem_reg (to support 4.) Matter of fact, it does not need to be option Z, it can be Z and if there is nothing in the string it defaults to 1.

But then I think all this ends up being a bigger change, right? Do you have a better Idea?
Oh and in case there are two regs, they do not necessarily need to be identical.

[dderjoel]

And does it make a difference it it is shl or shlx ?

What's the difference between these two (in assembly land)?

And does it make a difference it it is shl or shlx ?

I think you're right that it probably does not matter at this level, but you might need to add something that deals with the flags. The Ok proof will tell you whether or not you need to care; if you can prove Ok, then you're fine.

Just for completeness-sake:
they both shift left, but they have different syntax and affect the flags differently shl r/m, imm, operand 1 is source and destination, operand 2 is the shift count; and it affects the flags, in the sense that the first shifted bit is in the CF (or undefined in some cases) OF undefined for imm != 1, for imm==1: OF= xor first-two-bits-of-original-value (but in our case It is enough to just kill both flags), and I don't use shl m, imm, I only use shl r, imm but I don't think that that matters much here.
shlx ra, r/m, rb. does not affect any flags. reads the shift count from rb, masks the least 5/6 bits (depends on the whether r's are 32/64 bit) and reads from r/m, shifts by shift count and stores in ra.

I think that this is on the shlZ level I think, and at that point it should maybe not matter?

What do you mean?

I am not too sure about what shlZ is tbh. I thought that from the parsing level (shl, shlx) it gets translated into a logical 'shift something by Z to the left'. Hence I should after the parsing we deal with shlZ which I'd parse both into. I mean the correctness-prove should not care if it shifts because of a shl or shlx, (as long as the Flags are updated accordingly of cause). Hence I thought the re-writer is at shlZ-level.

Edit: the shlx is syntax-wise similar to bzhi and logic-wise similar to shl. That's how I copy-pasted the definitions to Symbolic.v

[dderjoel]

Try starting with this (untested):

Definition shift_to_mul :=
  fun e => match e with
    ExprApp ((shl | shlx | shlZ) as o, [e'; ExprApp (const v, [])]) =>
      let o' := match o with shl | shlx => mul 64%N | shlZ => mulZ | _ => o (* impossible *) end in
      if Z.eqb v 0
      then e'
      else if Z.ltb 0 v
      then ExprApp (o', [e'; ExprApp (const (2^v)%Z, [])])
      else e | _ => e end.
Global Instance shift_to_mul_ok : Ok shift_to_mul_small.
Proof. t. cbn in *. firstorder (lia + eauto). Qed.

just adding this errors in

File "./src/Assembly/Symbolic.v", line 1373, characters 14-17:
Error: The constructor shl (in type op) is expected to be applied to
1 argument while it is actually applied to no arguments.

And the char's are the shl in the first parenthesis.
So what I do understand from this code is, that we are trying to match an operation of type shl, shlx, shlz with that below, match and rewrite shl and shlx to mul to a 64-bit positive whole number; and rewrite shlZ as mulZ. But all that only if the constant is >0. Otherwise , if v==0, (i.e. shift left by 0) we return the value itself (then e') and if v<0 we return the original expression else e...
Which seems correct to me, too. Is coqc complaining about that 'impossible'-case there, that from that definition, as we know it cant happen, because if o is from type (shl|shlx|zhlZ) we must have matched earlier. But does coq not know that and expects o' to possibly be o and (i.e. possibly shl), but even then in the then ExprApp (o', [e'; ExprApp (const (2^v)%Z, [])]) we still give it arguments. So I dont really see, where we would construct shl with no arguments.

[JasonGross]

So now I'm thinking to change the Record MEM to Record MEM := { mem_is_byte : bool ; mem_reg : REG ; mem_extra_reg : option REG ; mem_scale: option Z ; mem_offset : option Z }. with the semantics, that when there is a scale, it always scales the mem_reg (to support 4.) Matter of fact, it does not need to be option Z, it can be Z and if there is nothing in the string it defaults to 1.

But then I think all this ends up being a bigger change, right? Do you have a better Idea?

This sounds good to me, and I don't have a better idea. Perhaps the best way to do the parsing is to have five alternatives separated by ||->{id}, one for each bullet point. You could combine some of them if you want (making various parts optional), but make sure you don't have overlapping alternatives.

I am not too sure about what shlZ is tbh.

shlZ is for a left-shift that doesn't truncate the output to any bit width, i.e., left-shift in Z (rather than, e.g., uint64)

Is coqc complaining about that 'impossible'-case there, that from that definition, as we know it cant happen, because if o is from type (shl|shlx|zhlZ) we must have matched earlier.

It's saying that shl needs to be shl bitwidth because shl takes an argument. Presumably shlx does as well, and so you want (shl _|shlx _|zhlZ) here and match o with shl biteidth | shlx biteidth => mul bitwidth | shlZ => mulZ | _ => o (* impossible *) end later on. (Your analysis of what the entire function is doing is correct)

[dderjoel]

okay, I removed the MEM-changes, I will create another PR for that, lets focus here on the shl-> mul rewrite.
I added that rewrite with the bit widths, but now it complains about an a missing shift_to_mul_small (and I can confirm. It does not exist :) ). Looking at the other Proofs, there is none where the Global Instance line has A and then A_small, they all end with the same name as the rewrite itself is called. Replacing shift_to_mul_small with shift_to_mul. cocq complains with

File "./src/Assembly/Symbolic.v", line 1381, characters 46-50:
Error: (in proof shift_to_mul_ok): Attempt to save an incomplete proof

Also I cannot find any similar Proofs in the any other rewrites. None starts with Proof. t., and all the other ones I could find just say Qed. right after it, but I assume we don't want that.
So, (1) I don't understand what the Global Instance line means, and (2) what we need to proof, and (3) how we are trying to achieve that with that line Proof. t. cbn in *. firstorder (lia + eauto). Qed. 6efb428

[dderjoel]

Wonderful. Thanks. I just built successfully from this commit, and I can confirm, that it does everything that I need.
from my side, we can merge and close this.