Lemmas imported in one module are applied in others

For further investigation.

While working on https://github.com/runtimeverification/kontrol/pull/369, @PetarMax and I noticed that Optimism-specific lemmas that are imported in the PortalTest contract via

kontrol build --require lemmas.k --module-import PortalTest:PAUSABILITY-LEMMAS

are only being imported into PortalTest-VERIFICATION module:

module S2KtestZModPortalTest-VERIFICATION
    imports public S2KtestZModPortalTest-CONTRACT
    imports public PAUSABILITY-LEMMAS
endmodule

but it looks like they’re being used across all tests in Kontrol test suite. For example, AssumeTest.test_assume_false(uint256,uint256) is affected, with

<k>
   ( #addr [ ISZERO ]
   ~> #exec [ ISZERO ]
   ~> #pc [ ISZERO ] => CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0
   ~> #pc [ CALL ] )
   ~> #execute
   ~> _CONTINUATION
</k>

getting rewritten to

<k>
   ( .K => CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0
   ~> #pc [ CALL ] )
   ~> #execute
   ~> _CONTINUATION
</k>

Reproduce the issue with kontrol build --require lemmas.k --module-import PortalTest:PAUSABILITY-LEMMAS and inspect the generated S2KtestZModPortalTest-VERIFICATION module. Compare lemma application in PortalTest with AssumeTest.test_assume_false(uint256,uint256), then determine why the imported rules rewrite unrelated tests and define a testable isolation boundary.