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

Run kompile a.k --backend haskell && kprove spec.k using the definitions in a.k and claim in spec.k. Inspect the generated translation for the simplification rule involving Remainder; done means the translation preserves Remainder on both the left- and right-hand sides as described under Expected Results.

What component is the issue in?

Front-End

Which command

• 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>).