Gappa creates invalid Coq output (contains $ signs)
Michael Hennebry reported on Zulip an issue that gappa creates invalid Coq output containing a $ sign. I can reproduce this on macOS (Michael H. is on Linux).
The reproduction sequence is as follows:
gappa -Bcoq -Echange-threshold=0 -Eprecision=200 -Eno-auto-dichotomy refine43s.g > refine43s.v
where refine43s.g is:
@rnd = float<ieee_64, ne> ;
@rnf = float<ieee_32, ne> ;
a0 = 0x1.9c3e9cp+1 ;
a1 = -0x1.e1d8fap+2 ;
a2 = 0x1.90a096p+3 ;
a3 = -0x1.87d8ecp+3 ;
a4 = 0x1.9c7ffcp+2 ;
a5 = -0x1.695746p+0 ;
mana = rnd(man0_) ;
SQRT2f rnf=0x1.6a09e6p+0;
manf =rnf(mana);
rsrf rnf=(((((a5*manf+a4)*manf+a3)*manf+a2)*manf+a1)*manf+a0);
rsrg rnf=rsrf *(1 + odd*(SQRT2f-1));
manb = rnd(mana*rnf(1 - rnf(0.5*odd)));
sr = sqrt(manb) ;
rsr = 1/sr ;
err4 = rsrg - rsr ;
werr4 = (sqrt(manb)*sqrt(sqrt(sqrt(manb))))*err4 ;
FE3f = (rsr + err4)*(3 - (manb*rsr*rsr + manb*2*rsr*err4 + manb*err4*err4))*0.5
- rsr ;
FE3g = (rsr + err4)*(3 - (1 + manb*2*rsr*err4 + manb*err4*err4))*0.5
- rsr ;
{
manb in [0.25, 1.0]
/\ werr4 in [-0x1.C0p-17, 0x1.C1p-17]
->
FE3f - FE3g in [0, 0]
}
# without the constraint, dollar sign goes away
manb*rsr*rsr -> 1 { sqrt(sqrt(manb)) >= 0 } ;