[K-Bug] kompile - simplification rule involving cell maps not compiled correctly

virgil-serbanuta commented 1 year ago

What component is the issue in?

Front-End

Which command

[X] kompile
[ ] kast
[ ] krun
[ ] kprove
[ ] kprovex
[ ] ksearch

What K Version?

K version: v5.5.40-0-g98574f12a2-dirty

Operating System

Linux

K Definitions (If Possible)

module A
  imports INT

  configuration
    <a>
      <k>.K</k>
      <shards>
        <shard multiplicity="*" type="Map">
          <shard-id> 0:Int </shard-id>
          <shard-value> 0:Int </shard-value>
        </shard>
      </shards>
    </a>

  syntax KItem ::= "start"
  syntax Int ::= f(ShardsCell)  [function, total]

  rule <k> start => f(Shards) </k>
      Shards:ShardsCell

  rule f(<shards>.Bag</shards>) => 0
  rule f(<shards>_:ShardCell Remainder</shards>) => 1 +Int f(<shards>Remainder</shards>)  [simplification]

endmodule

If needed, here's a spec using this:

module SPEC
  imports A

  claim <k> start => 2 </k>
        <shards>
          <shard>
            <shard-id> 0:Int </shard-id>
            <shard-value> 0:Int </shard-value>
          </shard>
          <shard>
            <shard-id> 1:Int </shard-id>
            <shard-value> 1:Int </shard-value>
          </shard>
        </shards>
endmodule

Steps to Reproduce

kompile a.k --backend haskell && kprove spec.k

kompile will produce this translation for rule f(<shards>_:ShardCell Remainder</shards>) => 1 +Int f(<shards>Remainder</shards>) [simplification] (indented to make it easier to read):

// rule `f(_)_A_Int_ShardsCell`(`<shards>`(inj{ShardCell,ShardCellMap}(_Gen0)))=>`_+Int_`(#token("1","Int"),`f(_)_A_Int_ShardsCell`(`<shards>`(`.ShardCellMap`(.KList)))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(7e4f664e55f0c88c055d9f2d2ef43b63a866fb51f0e3e8b6c51164c672d74f9f), org.kframework.attributes.Location(Location(22,8,22,89)), org.kframework.attributes.Source(Source(/mnt/data/runtime-verification/elrond-esdt/tmp/a.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification]

axiom{R} \implies{R} (
    \top{R}(),
    \equals{SortInt{},R} (
      Lblf'LParUndsRParUnds'A'Unds'Int'Unds'ShardsCell{}(
        Lbl'-LT-'shards'-GT-'{}(
          inj{SortShardCell{}, SortShardCellMap{}}(Var'Unds'Gen0:SortShardCell{})
        )
      ),
      \and{SortInt{}} (
        Lbl'UndsPlus'Int'Unds'{}(
          \dv{SortInt{}}("1"),
          Lblf'LParUndsRParUnds'A'Unds'Int'Unds'ShardsCell{}(
            Lbl'-LT-'shards'-GT-'{}(Lbl'Stop'ShardCellMap{}())
          )
        ),
        \top{SortInt{}}()
      )
    )
  )
  [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/mnt/data/runtime-verification/elrond-esdt/tmp/a.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(22,8,22,89)"), simplification{}(""), UNIQUE'Unds'ID{}("7e4f664e55f0c88c055d9f2d2ef43b63a866fb51f0e3e8b6c51164c672d74f9f")]

Expected Results

The translation for rule f(<shards>_:ShardCell Remainder</shards>) => 1 +Int f(<shards>Remainder</shards>) [simplification] should use the Remainder variable.

To be specific, the LHS of this rule should be translated to f(<shards>_:ShardCell Remainder</shards>), not to f(<shards>_:ShardCell</shards>) and the RHS of this rule should be translated to 1 +Int f(<shards>Remainder</shards>), not to 1 +Int f(<shards>.ShardCellMap</shards>).

radumereuta commented 1 year ago

@virgil-serbanuta we somehow missed this issue. Is this something you are still interested in us looking at?

virgil-serbanuta commented 1 year ago

I don't need this, IIRC, I was helping someone debug.

On the other hand, also IIRC and sorry if I'm wrong, this may make some broken proofs pass. If that's the case, then shouldn't this be fixed anyway? Or shouldn't this syntax be disabled if it's not fixed?

ehildenb commented 1 year ago

Some things to investigate:

Does teh rule compile correctly without the simplification attribute? If so, then we have narrowed down teh potential failure to the changes in how we do configuration completion for normal vs. simplification rules.

Robertorosmaninho commented 1 year ago

With [simplification] I got a similar result:

// rule `f(_)_A_Int_ShardsCell`(`<shards>`(`.ShardCellMap`(.KList)))=>#token("0","Int") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(d582175fe383b724b31e5bed5e852b6d05f85a93a86c658acc7bff9da059b003), org.kframework.attributes.Location(Location(21,8,21,37)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/tests/issue_3087/a.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
  axiom{R} \implies{R} (
    \and{R}(
      \top{R}(),
      \and{R} (
          \in{SortShardsCell{}, R} (
            X0:SortShardsCell{},
            Lbl'-LT-'shards'-GT-'{}(Lbl'Stop'ShardCellMap{}())
          ),
          \top{R} ()
        )),
    \equals{SortInt{},R} (
      Lblf'LParUndsRParUnds'A'Unds'Int'Unds'ShardsCell{}(X0:SortShardsCell{}),
     \and{SortInt{}} (
       \dv{SortInt{}}("0"),
        \top{SortInt{}}())))
  [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(21,8,21,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/tests/issue_3087/a.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), UNIQUE'Unds'ID{}("d582175fe383b724b31e5bed5e852b6d05f85a93a86c658acc7bff9da059b003")]

The behavior is the same with and without [simplification].

Just for the sake of providing more information, the output of the mentioned command is:

$ kompile a.k --backend haskell && kprove spec.k

[Warning] Compiler: Could not find main syntax module with name A-SYNTAX in
definition.  Use --syntax-module to specify one. Using A as default.
kore-exec: [148026] Warning (WarnStuckClaimState):
    The configuration's term unifies with the destination's term, but the implication check between the conditions has failed. Location: /home/robertorosmaninho/rv/tests/issue_3087/spec.k:4:9-14:18
Context:
    (InfoReachability) while checking the implication
  #Not ( {
    2
  #Equals
    f ( <shards>
      <shard>
        <shard-id>
          0
        </shard-id>
        <shard-value>
          0
        </shard-value>
      </shard> <shard>
        <shard-id>
          1
        </shard-id>
        <shard-value>
          1
        </shard-value>
      </shard>
    </shards> )
  } )
#And
  <a>
    <k>
      f ( <shards>
        <shard>
          <shard-id>
            0
          </shard-id>
          <shard-value>
            0
          </shard-value>
        </shard> <shard>
          <shard-id>
            1
          </shard-id>
          <shard-value>
            1
          </shard-value>
        </shard>
      </shards> ) ~> .
    </k>
    <shards>
      <shard>
        <shard-id>
          0
        </shard-id>
        <shard-value>
          0
        </shard-value>
      </shard> <shard>
        <shard-id>
          1
        </shard-id>
        <shard-value>
          1
        </shard-value>
      </shard>
    </shards>
  </a>
[Error] Prover: backend terminated because the configuration cannot be
rewritten further. See output for more details.

ehildenb commented 1 year ago

@Robertorosmaninho in the above output, it looks like you grabbed the Kore of the wrong rule (the base case, instead of the recursive case).

Robertorosmaninho commented 1 year ago

I'll check it again.

Robertorosmaninho commented 1 year ago

You're right. My bad @ehildenb! Here is the correct KORE rule With [simplification]:

// rule `f(_)_A_Int_ShardsCell`(`<shards>`(inj{ShardCell,ShardCellMap}(_Gen0)))=>`_+Int_`(#token("1","Int"),`f(_)_A_Int_ShardsCell`(`<shards>`(`.ShardCellMap`(.KList)))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(7e4f664e55f0c88c055d9f2d2ef43b63a866fb51f0e3e8b6c51164c672d74f9f), org.kframework.attributes.Location(Location(22,8,22,89)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/tests/issue_3087/a.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification]
  axiom{R} \implies{R} (
    \top{R}(),
    \equals{SortInt{},R} (
      Lblf'LParUndsRParUnds'A'Unds'Int'Unds'ShardsCell{}(Lbl'-LT-'shards'-GT-'{}(inj{SortShardCell{}, SortShardCellMap{}}(Var'Unds'Gen0:SortShardCell{}))),
     \and{SortInt{}} (
       Lbl'UndsPlus'Int'Unds'{}(\dv{SortInt{}}("1"),Lblf'LParUndsRParUnds'A'Unds'Int'Unds'ShardsCell{}(Lbl'-LT-'shards'-GT-'{}(Lbl'Stop'ShardCellMap{}()))),
        \top{SortInt{}}())))
  [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/tests/issue_3087/a.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(22,8,22,89)"), simplification{}(""), UNIQUE'Unds'ID{}("7e4f664e55f0c88c055d9f2d2ef43b63a866fb51f0e3e8b6c51164c672d74f9f")]

Although the resulting error still is the same.

runtimeverification / k