Towards nominals

[4ever2]

PR tracks progress towards nominal SSProve integration.

• Base Locations and Interfaces on finite maps. #65
• Remove ordType instance on choice_type #69
• Remove trim and internalize locations #72

[MarkusKL]

Merge checklist:

• Update user docs.
• Write header for fmap_extra.v
• Investigate how this affects the Hax backend. (I would be happy to receive help with this)
• Merge Remove ordType instance on choice_type #69
• Merge Remove trim and internalize locations #72

[spitters]

Do you depend on solving the universe issue, or can that be done in a separate PR?

[4ever2]

Do you depend on solving the universe issue, or can that be done in a separate PR?

The universe issue is not a problem here. We don't plan on removing choice_type in this PR.

[4ever2]

@MarkusKL
There are some minor conflicts with the changes from #73.

Disregard the MC-dev CI failure, they are unrelated to these changes. I'll fix it in another PR.

[4ever2]

@MarkusKL
CI issue is now fixed.

Feel free to add a reference to the nominal paper in the readme, either in this PR or in the PR integrating nominal.

[spitters]

@cmester0 will this require any modifications for the hax backend? Could you check that all our examples still compile?

[spitters]

LGTM

[MarkusKL]

I will add a reference to the paper in a week or two when it has been finalized for CSF and is online. Thanks for all of the comments, reviews and fixes.

[MarkusKL]

I have rebased this branch on current main in my own repository: MarkusKL#7
I would suggest to override this branch with the rebased branch wait for builds to succeed and then merge as soon as possible to put these changes into main. Or is there something else that needs to be done before this can be merged? I will then make a new PR for nominal definitions, theorems and examples.

[cmester0]

The changes required by Hax are removing trimmed and Parable proofs, or some renaming/updating to use fmaps. There should be nothing blocking from Hax, I will just fix everything once this is merged.