search

runtimeverification / proof-generation

University of Illinois/NCSA Open Source License
10 stars 4 forks source link

Modeling of Kore #29

Open amelieled opened 2 years ago

amelieled commented 2 years ago

In the file theory/kore.mm, someone can read:

kore-bottom-is-pattern $a #Pattern ( \kore-bottom ph0 ) $.
kore-bottom-is-sugar $a #Notation ( \kore-bottom ph0 ) \bot $.

kore-top-is-pattern $a #Pattern ( \kore-top ph0 ) $.
kore-top-is-sugar $a #Notation ( \kore-top ph0 ) ( \inh ph0 ) $.

kore-not-is-pattern $a #Pattern ( \kore-not ph0 ph1 ) $.
kore-not-is-sugar $a #Notation ( \kore-not ph0 ph1 ) ( \and ( \not ph1 ) ( \kore-top ph0 ) ) $.

kore-and-is-pattern $a #Pattern ( \kore-and ph0 ph1 ph2 ) $.
kore-and-is-sugar $a #Notation ( \kore-and ph0 ph1 ph2 ) ( \and ph1 ph2 ) $.

kore-or-is-pattern $a #Pattern ( \kore-or ph0 ph1 ph2 ) $.
kore-or-is-sugar $a #Notation ( \kore-or ph0 ph1 ph2 ) ( \or ph1 ph2 ) $.

Why do you use ph0 to define \kore-not, but not in the case of \kore-and or kore-or? Is it a tricky detail?

Moreover, \ceil and floor (in ML so) have only one argument, but someone can read (in the same file as previously):

kore-ceil-is-pattern $a #Pattern ( \kore-ceil ph0 ph1 ph2 ) $.
kore-ceil-is-sugar $a #Notation ( \kore-ceil ph0 ph1 ph2 ) ( \and ( \ceil ph2 ) ( \kore-top ph1 ) ) $.

kore-floor-is-pattern $a #Pattern ( \kore-floor ph0 ph1 ph2 ) $.
kore-floor-is-sugar $a #Notation ( \kore-floor ph0 ph1 ph2 ) ( \kore-not ph1 ( \kore-ceil ph0 ph1 ( \kore-not ph0 ph2 ) ) ) $.

Why in this case have 2 arguments been added and not one as for the other existing symbols in the Matching Logic? Is it a tricky detail?

More generally, I don't understand what is the usefulness of the additional argument?

zhengyao-lin commented 2 years ago

The first argument is used to denote the output sort of the pattern (which is also a pattern itself). In particular, for any kore construct, one should be able to prove some kind of typing lemma like this (e.g. https://github.com/kframework/matching-logic-proof-checker/blob/main/theory/kore-sorting.mm)

ph1 in [ph0]          ph2 in [ph0]
-----------------------------------
( \kore-and ph0 ph1 ph2 ) in [ph0]

where [ph0] denotes the domain of sort ph0.

In the case of \kore-not, we couldn't use the native \not, because semantically it takes the complement with respect to the entire domain, but instead we want to take the complement with respect to only [ph0]. Thus we are taking an extra intersection with [ph0] (which is equal to \kore-top ph0)

In the case of \kore-ceil and \kore-floor, we actually need two sorts ph0 and ph1, where ph0 denotes the output sort as before, and ph1 denotes the input sort. These sorts are used to make sure that the result stays in [ph0].