Annotating rules that preserve definedness

[PetarMax]

This PR aims to annotate all of the Kontrol rules for which we know that they preserve definedness, but the backend is not able to prove this on its own.

[PetarMax]

Related question.

[palinatolmach]

The Docker test is failing in solc_to_k with

  File "/home/user/.local/lib/python3.10/site-packages/kontrol/solc_to_k.py", line 580, in __init__
    self.contract_path = self.contract_json['ast']['absolutePath']
KeyError: 'ast' 

which means that it can’t find the ast field in the compilation artifact file generated by forge build — that doesn't seem related to the changes made in the PR, I'll look into why that might be happening.

Update: it's not PR-specific, the same issue appears in other PRs and (seemingly) on different runners:

• https://github.com/runtimeverification/kontrol/actions/runs/8035018079/job/21959536108?pr=394
• https://github.com/runtimeverification/kontrol/actions/runs/8044703786/job/21968793500?pr=369

Trying to reproduce this locally now.