!MfVXcmpKuyudZHcqil:matrix.org

The K Framework User Group

261 Members
The K Framework (kframework.org) and its applications to smart contracts.  EVM: github.com/kframework/evm-semantics Viper: github.com/kframework/viper-semantics45 Servers

Load older messages


SenderMessageTime
6 Oct 2021
@apache8080:matrix.orgapache8080Where does the IELE group discuss things? Looks like their matrix is dead16:15:39
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Here should be fine actually. 16:29:07
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt If you have questions about the language itself and the semantics. 16:29:20
@apache8080:matrix.orgapache8080Does IELE get used by any production blockchains?16:43:21
@javbit:matrix.orgjavbit joined the room.16:44:48
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Not at the moment. 17:19:18
9 Oct 2021
@ammkrn:matrix.org@ammkrn:matrix.org left the room.21:02:36
14 Oct 2021
@sashmit1:matrix.orgSashmit Bhaduri joined the room.21:11:09
15 Oct 2021
@jesse.sigal:matrix.orgjesse.sigal joined the room.20:41:59
19 Oct 2021
@koding:matrix.orgkoding joined the room.06:35:08
@koding:matrix.orgkoding Hi all! Is Jello Paper website being updated?
(I had difficulties to get beyond Installation as it is the only item after Homepage in the left-hand menu. It took me a while to understand that the content of Repository Structure section is the main content of the Jello Paper -- only thanks to the Web Archive versions of the website from 2019.)
06:49:01
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Yes, it is updated automatically whenever KEVM is updated (https://github.com/kframework/evm-semantics). The left navigation menu gives you high-level navigation, and the right one gives you low-level navigation. 16:25:34
20 Oct 2021
@jesse.sigal:matrix.orgjesse.sigal Hi all, is it possible to have alpha equivalnce taken into account when using kprove? I.e., in my language I want claim (\x -> x) => (\y -> y) to work (where x and y are program variables). 14:25:07
@jesse.sigal:matrix.orgjesse.sigal (and (\x -> x) is lambda syntax) 14:29:37
21 Oct 2021
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Not like this (without writing your own manual pattern matching), because from K's perspective these are just terms that look like \->(x, x) and \->(y, y) where \-> is the symbol defined in your language. 12:29:50
@jesse.sigal:matrix.orgjesse.sigalIs there a common idiom in K for acheiving this? (Based on or not with KVars)12:30:33
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt But if you put symbolic variables in for x and y then at least this case will work:
claim (\X:Var -> X) => (\?Y:Var -> ?Y)
for example.
12:30:36
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt But from K's perspective in your original, x and y are "domain values" (which means they are distinct elements in the carrier sort in the model). 12:31:40
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Whereas X:Var is a symbolic universally quantified variable, and ?Y:Var is an existentially quantified variable. 12:32:09
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt But weird things happen at the 0-step proof boundary, so i fyou want to do a functional equality proof like this, you may want to force it to take one step, I usually do this:
syntax Step ::= run ( MySort ) , done ( MySort )

rule  k  run(X) => done(X) ...  /k 

claim  k  run(\X:Var -> X) => done(\?Y:Var -> Y) ...  /k 
to force it to do a single step of execution before checking the equality.
12:33:44
@jesse.sigal:matrix.orgjesse.sigalAh I believe I ran into this issue yesterday experimenting where it complained no rewrites were applicable :)12:34:42
@jesse.sigal:matrix.orgjesse.sigalThanks!12:35:22
@jesse.sigal:matrix.orgjesse.sigalI guess it's also possible to write a K function to replace all bound (w.r.t. the defined language) variables with existential/fresh K variables as a preparation step.12:36:23
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt Yes, it's definitely possible, but it's maybe not as straightforward as you may think. 12:38:12
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt You can have a rule that looks like this:
rule  k  makeFresh() => ?X:Int ...  /k 
for example.
12:38:31
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt But you can't have a functional rule like that, because the semantics of having a fresh existential variable on the RHS of a functional rule ends up being unsound. 12:39:00
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt So you need to manually unfold your whole term on the top of the k cell, and replace variables using top-level semantic rules like above, and then re-fold it back up. 12:39:36
@jesse.sigal:matrix.orgjesse.sigalHmmm, makes sense that that would cause problems. I'll have to sit and think about the last point you made as well. As a plus, the calculus I implemented as a test has a reduction relation which is functional, so I might be able to get away with a simpler approach.12:41:43
@_slack_runtimeverification_U8T2RJ802:matrix.orgeverett.hildenbrandt eg. (sketch):
rule  k  (\X:Var -> TERM) => #applySubst(X, ?XFRESH, TERM) ~> (\?XFRESH -> [HOLE]) ...  /k 
rule  k  TERM ~> (\X -> [HOLE]) => (\X -> TERM) ...  /k 

syntax MySort ::= #applySubst(Var, Var, MySort) [function]
rule #applySubst(X, ?XFRESH, X) => ?XFRESH
... OTHER CASES FORE #applySubst
12:42:24
@jesse.sigal:matrix.orgjesse.sigalAh I think I see, cheers!12:47:40

There are no newer messages yet.


Back to Room List