!MfVXcmpKuyudZHcqil:matrix.org

The K Framework User Group

253 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
26 Jul 2021
@metaweta:matrix.orgMike StayWhat's the current syntax for bags? (Or are they supported?)18:29:38
@metaweta:matrix.orgMike StayCan we declare an operator to be associative and commutative?18:31:04
@_slack_runtimeverification_U99TYNSG3:matrix.orgnishantjr Ah, the attribute may be a tag for the now depricated --transition parameter to kompile:
    --transition
      [DEPRECATED: java backend only]  string  is a whitespace-separated list 
      of tags designating rules to become transitions.
      Default: [transition]
18:32:03
@cbwilliams:matrix.orgcbwilliamsI think I remember seeing that we can add the tag [associative] to an operator, but I don't know where I saw this.18:33:26
@_slack_runtimeverification_U99TYNSG3:matrix.orgnishantjr I'm not sure if that was in a really old version on K based on maude, but that's no longer supported unfortunately. I think in this situation, you move to create a rule to move each subterm to its own cell within a cell marked multiplicity="*" type="Set", as in the thread cell here : https://github.com/kframework/k/blob/master/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md#configuration 18:39:21
@_slack_runtimeverification_U99TYNSG3:matrix.orgnishantjr You'd need a rule similar to https://github.com/kframework/k/blob/master/k-distribution/pl-tutorial/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md#spawn 18:40:06
@_slack_runtimeverification_U99TYNSG3:matrix.orgnishantjr Another way of getting commutativity is to use the builtin SET module (though I don't think its appropriate in this case). https://github.com/kframework/k/blob/master/k-distribution/include/kframework/builtin/domains.md#sets 18:41:06
@cbwilliams:matrix.orgcbwilliamsokay, thanks, this seems to be working so far.18:49:28
@cbwilliams:matrix.orgcbwilliamsRedacted or Malformed Event18:49:36
@cbwilliams:matrix.orgcbwilliamsRedacted or Malformed Event18:49:46
@cbwilliams:matrix.orgcbwilliamsRedacted or Malformed Event18:50:03
@cbwilliams:matrix.orgcbwilliamsRedacted or Malformed Event18:50:13
@cbwilliams:matrix.orgcbwilliamsRedacted or Malformed Event18:50:24
@cbwilliams:matrix.orgcbwilliamsRedacted or Malformed Event18:50:49
@cbwilliams:matrix.orgcbwilliamsRedacted or Malformed Event18:50:53
@cbwilliams:matrix.orgcbwilliamsRedacted or Malformed Event18:51:17
@metaweta:matrix.orgMike StayRedacted or Malformed Event18:54:32
@metaweta:matrix.orgMike StayRedacted or Malformed Event18:55:53
@metaweta:matrix.orgMike Stay * If we just have an in(...), we see it in the <in> cell. Ditto for out(...). But if we put both in, they react with each other using the final rule but we don't see the result in the <k> cell. 18:56:15
@cbwilliams:matrix.orgcbwilliams *

module RHO-SYNTAX
    imports DOMAINS-SYNTAX
    imports KVAR-SYNTAX

    syntax N ::= "&" Terms
               | KVar

  syntax Zero ::= "Z"
  syntax In ::= "in" "(" KVar "<-" N "." Terms ")" [binder]
  syntax Out ::= "out" "(" N "," Terms ")"
  syntax Term ::= Zero
                | In
                | Out
  syntax Terms ::= List{Term, "|"}

endmodule

module RHO
  imports RHO-SYNTAX
  imports SUBSTITUTION

  syntax KResult ::= Terms

  configuration <T>
    <ins>
      <in multiplicity="*" type="Set"> . </in>
    </ins>
    <outs>
      <out multiplicity="*" type="Set"> . </out>
    </outs>
    <k> $PGM:Terms </k>
  </T>

  rule
    <k> _:Zero | Ts:Terms => Ts </k>

  rule
    <k> I:In | Ts:Terms => Ts </k>
    <ins> (Is) => (Is <in> I </in>) </ins>

  rule
    <k> O:Out | Ts:Terms => Ts </k>
    <outs> (Os) => (Os <out> O </out>) </outs>

  rule
      <in> in (Y <- X . Ts:Terms ) => . </in>
      <out> out(X , P:Terms) => . </out>
      <k> .Terms => Ts[&P / Y] </k>

endmodule```
19:01:14
@metaweta:matrix.orgMike StayIs there a way to concatenate lists?19:12:24
@metaweta:matrix.orgMike Stay For example, suppose we have a list of Xs separated by "|", where an X is either a Y or a list of Ys.
Something like rule <k> (ys:Ys) | xs:Xs => ys ++ xs </k>
19:15:14
@_slack_runtimeverification_U99TYNSG3:matrix.orgnishantjr Unfortunately you'd need to write a function, like "++DeclList" here https://github.com/kframework/boogie-semantics/blob/master/helpers.md . 19:22:26
@_slack_runtimeverification_U99TYNSG3:matrix.orgnishantjr Try using the --depth flag to krun to see what the state looks like at each step. 19:23:11
@metaweta:matrix.orgMike StayOK, thanks. When there are multiple rules that can apply to a configuration, how do we see all the possible outcomes?19:31:37
@metaweta:matrix.orgMike Stay BTW, why would we need to write concatenation for a built-in data structure? syntax Xs ::= List{X, "|"} 19:33:23
@_slack_runtimeverification_U99TYNSG3:matrix.orgnishantjr Use --search for the LLVM (default) backend. For haskell it is the default behaviour. 19:41:52
@_slack_runtimeverification_U99TYNSG3:matrix.orgnishantjr I'm not sure why exactly we dont have this yet. Currently this production desugars into ordinary rules, but no functions are generated. I think the plan is to replace these with parametric data types eventually. I think functions over parametric datatypes is on the TODO list though I'm not sure what the priority is exactly. 19:44:23
@cbwilliams:matrix.orgcbwilliamssorry, I don't understand. how do we write a term and display its graph of all future behaviors?21:25:02
@cbwilliams:matrix.orgcbwilliamssurely there is a way to do this; I believe that reasoning about these graphs is one of the main purposes of Matching Logic.21:26:59

There are no newer messages yet.


Back to Room List