search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
452 stars 150 forks source link

Make `module_name` rewriting injective #4201

Open palinatolmach opened 9 months ago

palinatolmach commented 9 months ago

At the moment, module name for a proof is generated based on its uppercase proof.id with escaped illegal characters:

 @staticmethod
    def _make_module_name(proof_id: str) -> str:
        return 'M-' + re.sub(
            r'[\[\]]|[_%().:,]+', lambda match: 'bkt' if match.group(0) in ['[', ']'] else '-', proof_id.upper()
        )

However, as @tothtamas28 noted, mapping should be injective, otherwise name clashes might occur. We might be able to achieve reasonable injectivity by making escaping more symbol-specific as we do in Kontrol with contract names (e.g., rewriting each of _%().:, to its own counterpart and not just a -).

palinatolmach commented 8 months ago

Moving to Backlog since it's not urgent.