Make functions in numeric.md total functional

[ehildenb]

Right now there are #Ceil side-condition generated by the backend for the operators defined in numeric.md:

    syntax Val ::= IValType "." IUnOp Int   [klabel(intUnOp)  , function] 
                 | FValType "." FUnOp Float [klabel(floatUnOp), function] 
 // --------------------------------------------------------------------- 
    syntax Val ::= IValType "." IBinOp Int   Int   [klabel(intBinOp)  , function] 
                 | FValType "." FBinOp Float Float [klabel(floatBinOp), function] 
 // ----------------------------------------------------------------------------- 
    syntax Val ::= IValType "." TestOp Int [klabel(intTestOp), function] 
 // -------------------------------------------------------------------- 
    syntax Val ::= IValType "." IRelOp Int   Int   [klabel(intRelOp)  , function] 
                 | FValType "." FRelOp Float Float [klabel(floatRelOp), function] 
 // ----------------------------------------------------------------------------- 
    syntax Val ::= AValType "." CvtOp Number [klabel(numberCvtOp), function] 
 // ------------------------------------------------------------------------ 

I'm pretty sure these all can be made functional, with the appropriate changes to the helper functions they use.

For example:

• The functions #minWidth, #ctz, #popcnt, #round, #signed, #unsigned, #isInfinityOrNan, and truncFloat need to be made total.
• rule FTYPE . sqrt => ... needs to either have (i) sqrtFloat be made functional in domains.k, or (ii) explicitely handle the cases that sqrtFloat does not.

[hjorthjort]

These are indeed all total. The question is how to check whether the corresponding numeric function is defined or not.

[hjorthjort]

Could we put an explicit #Ceil side condition in the semantics? That would mimic the official spec closely.

[ehildenb]

Well, in many cases the numeric functions we use are marked as functional in domains.k already, so we can just rely on that.

In the cases where it's a function we define ourselves, we can also mark it a functional and make them total.

In the cases where we rely on a function defined in domains.k which is not marked as functional, we need to (i) make sure the appropriate #Ceil axioms for that function in domains.k, and (ii) make sure we only rely on the hooked function when the #Ceil axiom will simplify to #Top, and (iii) handle all the other cases explicitely/directly in our semantics.