Function rules with partial heads are unsound

[ttuegel]

The translation of K function rules as equalities in Kore is unsound if the left-hand side of a function rule may be undefined. Consider this K definition,

syntax Int ::= unsound ( Map ) [function]
rule unsound ( K |-> V M ) => 1

This definition is translated to the following Kore (approximately):

symbol unsound(Map) : Int [function]
axiom ∀ K V M. ⊤ → unsound(K |-> V M) = 1

(I am misusing the Kore syntax slightly; there is no syntax for maps, nor infix operators, but I hope the meaning is clear.)

Note the universal quantification of the rule variables! I can instantiate this rule at M = K |-> V, yielding:

axiom ⊤ → unsound(K |-> V K |-> V) = 1

The concatenation of two maps with the same key is undefined, so that

axiom ⊤ → unsound(⊥) = 1
axiom ⊤ → ⊥ = 1
axiom ⊤ → ⊥
axiom ⊥

This is not an immediate problem for the backend because we would never choose to instantiate the rule that way, but nevertheless it is unsound and we should decide how to fix the frontend's translation of this rule.

Attn: @traiansf @yzhang90

[yzhang90]

i think it should be OK to generate the following equation:

symbol unsound(Map) : Int [function]
axiom ∀ K V M. ⊤ → unsound(K |-> V M) = 1 /\ Ceil(K |-> V M)

basically we need to make sure all the arguments are defined. Most of the time, the arguments are just variables and the frontend can omit generating Ceil(V)

[virgil-serbanuta]

@yzhang90 Shouldn't that be

axiom ∀ K V M. Ceil(K |-> V M) → unsound(K |-> V M) = 1

?

Otherwise, if the ceil is bottom, you still get ⊤ → ⊥.

[virgil-serbanuta]

@ttuegel This might be an immediate problem for the backend: Consider applying this axiom to unsound(1->2 N). We would get 1, but we could later have a branch where N=1->2 (or we could discover it on the main branch). If so, then we have applied the axiom in an invalid case, losing information in the process.

[ttuegel]

@virgil-serbanuta I think we apply the pre-condition that all of the arguments are defined when we evaluate functions, so in that example, we would carry the condition \ceil(1->2 N).

[virgil-serbanuta]

Ok, interesting. Where are we doing that?

[yzhang90]

@virgil-serbanuta I think my encoding will produce ⊤ → ⊥ = ⊥ if map is not defined. and my encoding will automatically generate the constraint \ceil(1->2 N).

[virgil-serbanuta]

Ah, I see, so this was supposed to be parenthesized as

axiom ∀ K V M. ⊤ → (unsound(K |-> V M) = (1 /\ Ceil(K |-> V M)))

I assumed it would be

axiom ∀ K V M. ⊤ → (unsound(K |-> V M) = 1) /\ Ceil(K |-> V M)

Ok, then I agree it would work.