sail-to-lean: annotate data type annotations (including quantifiers)

[tobiasgrosser]

Look over all files in https://github.com/rems-project/sail/tree/sail2/lib, e.g., https://github.com/rems-project/sail/blob/sail2/lib/flow.sail.

Here an example PR: https://github.com/rems-project/sail/pull/754/files

We may want to use HAdd.add instead of Int.add

[jprider63]

@benjaminselfridge is actually working on this, but I don't seem to be able to assign it to him. @Alasdair would you please add him to the repository?

[jprider63]

From @javra:

New Lean defs go here: src/sail_lean_backend/Sail/Sail.lean

[benjaminselfridge]

We're starting a branch here: https://github.com/GaloisInc/sail/blob/feature/lean_external_arith/lib/arith.sail

Does the initial commit I made look sane to you?

[javra]

Looks good! There's a better abs in Mathlib, but since we don't want to depend on it, that's not an option.

You could also, in Sail.lean, add intAbs, define it as the composition you used, and thant refer to that in the annotation.

[benjaminselfridge]

Hi @javra,

I'm finished with annotations for arith.sail and flow.sail. I'm working on the rest of the files, but I wanted to check in and make sure what I just committed seems reasonable to you.

[javra]

Feel free to already open a (draft) PR, that's easier for me to review 👍

[javra]

Some annotations are still missing in arith.sail, shr_int for example. But we already merge the ones that you added

[tobiasgrosser]

@benjaminselfridge, feel invited to work with small patches that add complete annotations for a given area. We can merge these and then step-by-step add the others.