Suggestion: Val.of_bool and partial evaluation

[roconnor-blockstream]

The current definition of Val.of_bool is:

Definition of_bool (b: bool): val := if b then Vtrue else Vfalse.

While this definition is perfectly natural, it inhibits partial evaluation that could be possible. Notice that both Vtrue and Vfalse have a head term of Vint. If we pull this common term out of both branches we get the following definition.

Definition of_bool (b: bool): val := Vint (if b then Int.one else Int.zero).

Pulling out common head terms from match expressions can allow partial evaluation to proceed further because it doesn't get stuck on a neutral variable of the if expression as early. This is even more beneficial when the head term is a constructor like Vint which means that partial evaluation may be able to process a match expression surrounding a Val.of_bool b expression even with a neutral variable b passed to Val.of_bool.

With that in mind, we can go even further. Both Int.one and Int.zero begin with the head term Int.repr which in turn adds a Int.mkint constructor. We can enable even more partial evaluation with the following definition.

Definition of_bool (b: bool): val := Vint (Int.repr (Z.b2z  b)).

Changing this definition would make reasoning easier in certain situation in VST, where casting occurs (see PrincetonUniversity/VST#625). Generally speaking more partial evaluation makes reasoning easier for everyone, and presumably this would apply to CompCert itself.

Some downstream projects maybe be affected by this redefinition, requiring them to update (usually simplify) their proofs. The changes I have found to be needed in VST so far seem fairly modest.