Asm equivalence checker should handle: (neg 64, [9]) ≠ (slice 0 64, [(negZ, [9])])

[JasonGross]

No description provided.

[JasonGross]

Example (remove the extra newline and click synthesize again)

I see

Unable to unify: [inr [626, 631, 636, 641, 646]] == [inr [17, 24, 30, 36, 42]]
Could not unify the values at index 0: [#626, #631, #636, #641, #646] ≠ [#17, #24, #30, #36, #42]
index 0: #626 ≠ #17
(add 64, [#4, #11, #625]) ≠ (add 64, [#4, #11, #16])
index 2: #625 ≠ #16
(neg 64, [#9]) ≠ (slice 0 64, [#14])
(neg 64, [(old 64 9, [])]) ≠ (slice 0 64, [(negZ, [9])])
Operation mismatch: neg 64 ≠ slice 0 64

But we have

fiat-crypto/src/Assembly/Symbolic.v

Lines 2449 to 2455 in df1aa70

	Definition slice0 (d : dag) :=
	fun e => match e with
	ExprApp (slice 0 s, [(ExprApp ((addZ|mulZ|negZ|shlZ|shrZ|andZ|orZ|xorZ) as o, args))]) =>
	ExprApp ((match o with addZ=>add s|mulZ=>mul s|negZ=>neg s|shlZ=>shl s|shrZ => shr s|andZ => and s| orZ => or s|xorZ => xor s |_=>old 0%N 999999%N end), args)
	| _ => e end.
	#[local] Instance describe_slice0 : description_of Rewrite.slice0
	:= "Merges (slice 0 s) into addZ,mulZ,negZ,shlZ,shrZ,andZ,orZ,xorZ".

which seems like it should be triggering on the RHS (PHOAS)...

[JasonGross]

Plausibly the issue is that nodes are not revealed enough, and we should be revealing nodes before (or after) running rewriting passes