sqrt(x*x) not improved correctly

[DerekJuba-NIST]

When using "improve" on sqrt(x*x), the returned result is x. The result should be abs(x), so the returned result has high error. The Herbie example at https://herbie.uwplse.org/ processes this correctly.

[elmisback]

Definitely a bug, thank you for reporting!

I confirmed that this is the result we are obtaining from the /alternatives endpoint, so it is a problem in Herbie. I will cross-file this with herbie-fp/herbie as an issue with that endpoint and close this issue once that issue is closed.

[zaneenders]

I started looking into this.

[elmisback]

This seems to be blocked on server changes which Zane isn't around to finish. I've added this to the Monday meeting agenda.

[ztatlock]

FWIW, the relevant rewrites seem sound (at first glance anyway). Perhaps something is smuggled through a pow rewrite?

Next step is probably to try to repro with unsound rules disabled. Then to check the eqsat proof terms.

[elmisback]

There must be a difference between the alternatives considered by make-alternatives-result (https://github.com/herbie-fp/herbie/blob/d270acbc7fdb70c022858d48c7001216797499b1/src/api/server.rkt#L532) and make-improve-result (https://github.com/herbie-fp/herbie/blob/d270acbc7fdb70c022858d48c7001216797499b1/src/api/server.rkt#L435). I think Zane mentioned that it might have to do with improve running a processing step that doesn't run for alternatives?

[zaneenders]

I started on this on this PR but didn't conclude on a solution before I got pulled away by end-of-semester items.
The demo also does not display a valid FPCore which is part of the problem.