 | The K Framework User Group | 189 Members |
| The K Framework (kframework.org) and its applications to smart contracts. EVM: github.com/kframework/evm-semantics Viper: github.com/kframework/viper-semantics | 43 Servers |
| The K Framework User Group | 189 Members |
| The K Framework (kframework.org) and its applications to smart contracts. EVM: github.com/kframework/evm-semantics Viper: github.com/kframework/viper-semantics | 43 Servers |
| Timestamp | Message | |
|---|---|---|
| 17 Jan 2020 | ||
| 15:36:47 |  rikard.hjort | This is a crude approximation, because obviously some configuration that unifies two rules may not be reachable, and it ignores confluence. But a design goal I have is that the semantics are deterministic, and making sure all LHSs are is something I try to do anyway. |
| 15:37:57 | rikard.hjort | This is obviously ignoring the side conditions. But if they were written as requires X and requires notBool X it may be more feasible. |
| 15:42:04 |  traian.serbanuta | So, I think it might work like this: • Take each pair of rules • Unify their LHS • If they unify, check that the conjunction of the require conditions is satisfiable • If so, then report (maybe including a model generated by the SMT) Is this what you had in mind? |
| 15:43:27 | rikard.hjort | Yes, precisely |
| 15:46:09 | traian.serbanuta | It's doable, but the SMT solver might not be able to solve all instances; in that case, would you prefer false positives or false negatives? :-) |
| 15:54:30 |  everett.hildenbrandt | This is basically how the Maude confluence checker works. |
| 16:00:40 | rikard.hjort | False positives (reporting two rules possibly overlap, when in fact they don't) |
| 20:46:21 |  mrchico | If I have a spec whose RHS contains a variable that does not appear on the LHS, what are the semantics? Implicit existential quantifier? If this was a rewrite rule it would be an error, so I was expecting this to be the case for specs as well, but some anecdotal evidence suggests otherwise |
| 20:49:41 | everett.hildenbrandt | I believe it's existentially quantified, and bound by whatever constraints show up for that variable in the requires clause. 7M49CGSD can confirm for Java backend, BJL91LBZ for haskell backend. |
| 20:50:18 | everett.hildenbrandt | But one way to check would be to compile the spec to Kore (kprove --dry-run on Haskell backend), then just inspect the generated .kprove-*/spec.kore file for the quantifier it uses. |
| 20:54:50 |  tom.tuegel | Unless some change was made to the frontend, it's universal; all implicitly-quantified variables in Kore are universally quantified. |
| 20:57:05 | mrchico | In reply to @_slack_runtimeverification_UBJL91LBZ:matrix.orgThat's what I wrote initially, but a universal quantification on the RHS doesn't make much sense though? Then the matching would need to check that current expression can match any value? |
| 20:57:34 | tom.tuegel | @train |
| 20:57:50 | tom.tuegel | 5FRLGXJ9 will know more about what the frontend does here. |
| 21:00:36 | mrchico | This makes sense, but is a little dangerous, imo. We've had at least one instance where a misspelled variable on the RHS led to an accepted proof (for wrong reasons). Maybe a warning would be nice |
| 21:00:53 | mrchico | In reply to @_slack_runtimeverification_U8T2RJ802:matrix.org* This makes sense, but is a little dangerous, imo. We've had at least one instance where a misspelled variable on the RHS led to an accepted proof (for wrong reasons). Maybe a warning would be nice |
| 21:03:03 | everett.hildenbrandt | Well we are in the process of re-vamping the semantics of ? variables for the Haskell backend, so maybe we could impose a similar restriction on proofs that new variables which show up on the RHS must be prefixed with a ?, otherwise it's an error. |
| 21:03:36 | mrchico | I think that would be a good idea |
| 21:05:14 | mrchico | especially if the variable is present in the requires but only on the RHS, I'm not even sure there is a meaningful interpretation of the current behaviour. If you wanted to restrict a RHS variable, wouldn't you use ensures? |
| 21:05:35 | mrchico | * especially if the variable is present in the requires but only on the RHS, I'm not even sure there is a meaningful interpretation of the current behaviour. If you wanted to restrict a RHS variable, wouldn't you use ensures? |
| 21:07:03 | everett.hildenbrandt | Well sure, but operationally I think it ends up meaning largely the same thing. If you have it in the requires, it's like you're carrying around a variable which hasn't been used but is constrained until you reach the RHS, if you have it in ensures, it's like it shows up once you reach the RHS and then you check the additional constraint on it. At least for proving I think it won't matter. |
| 21:08:12 | mrchico | ah, I see what you mean |
| 23:53:02 |  daejun.park joined the room. | |
| 23:53:03 | daejun.park | FTTNE71Q In Matching logic, it is universally quantified, and I know it is counter-intuitive, but that's what it means locally. But that's not what you would need. I think we need to force users to use ? variables for RHS-only variables, and generate a warning message when non-?-variables appear only in RHS. Indeed, this is the behavior of some old version of K, but at some point, it was gone. So we will need to put it back. |
| 20 Jan 2020 | ||
| 08:00:38 | traian.serbanuta | Well, I would refer to this document that 7QGKQWE4 and myself put together, and has been reviewed by several other parties as well: https://github.com/kframework/kore/blob/master/docs/2019-12-16-Question-Mark-Variables-With-Ensures.md |
| 08:06:11 | traian.serbanuta | Although I agree that in general you don't want unbound universally quantified variables in the RHS, and as you pointed out, this is most often a misspelling mistake, you do sometimes need them, such as when expressing the rules involving randomness. Nevertheless, I totally agree with 7M49CGSD that we should report an error when variables unbound in the LHS are found in the RHS (and I think we already do), but we should have a special attribute for rules where we intentionally want unbound free variables in the RHS. That attribute would also instruct the execution engine that a random value of the given type is solicited upon applying that rule in concrete execution. |
| 08:10:14 | traian.serbanuta | Also, 7M49CGSD, the same document makes a distinction between the semantics of using ? (which would require existential quantification) and that of using universally quantified (unbound) variables. And it makes the case that both are useful, depending on the situation. |
| 12:34:36 | mrchico | Ok. It seems to be a general agreement that there should be an error if unbound variables appear only on the RHS. @traian.serbanuta this is the case for rules, but not for specs. I'll make an issue out of this. Regarding the universal vs. existential quantification, my reasoning was that given the way that the proof was constructed; i.e. by reaching a state which matched all other cells, and with particular expression in the cell where my (free) RHS variable sat, this was an existential quantification: the existential variable could be instantiated with the given expression. If there had been a universal quantification, it seems to me that the proof would need to consist of a set of states, which match all other cells, and where the cell in question can be instantiated to any value. In other words, such a claim would be equivalent to a set of claims, one for every possible value of the RHS variable. This interpretation appears to be consistent with the documentation for |
| 12:40:03 | traian.serbanuta | I think you're right that the current implementation does indeed treat unbound variables in the RHS of specs as existential. I think that was a choice made because it does not really make sense to have unbound universal variables in the RHS, so we decided to handle them as being existentially quantified at the time. But that is not correct, and since now we have the ? proposal, it makes more sense to throw an error. |
| 23 Jan 2020 | ||
| 04:22:15 |  Wei Tang (back on 31 Jan!) changed their display name from Wei Tang to Wei Tang (back on 31 Jan!). | |