Base Locations and Interfaces on finite maps.

[MarkusKL]

Locations and Inerfaces are based on fset from extructures. This PR changes it so that they are now based on fmap like packages already are.

Improvements made by this PR:

• Better automation for deciding disjointness, compatability and submaps.
• Remove flat predicate.
• Remove lemmas that were previously left inline.
• choice_type is not required to itself have choiceType strcture (except for in packages/heap_type.v).
• Improvement in build time of the project (6 min. around -30%).
• Removes many ad-hoc proofs done in the examples
• All fset/fmap automation has been isolated in fmap_extra.v, which provides fmap_solve
• Towards future work: removing inductive choiceType universe, integrating nominal sets.

Breaking changes:

• Custom reasoning about fset needs to be redone, but almost all of it should be automatic.
• Removes loc_rel invariant
• Simple replacements
  • {fset Location} -> Locations
  • ('nat; 5)%N -> (5, 'nat) (when defining locations)
  • fset [:: l1; l2 ... ] -> [fmap l1; l2 ... ]
  • L1 :|: L2 -> unionm L1 L2 (when taking union of locations and interfaces)
  • fset0 -> emptym

TODO:

• [x] ~~Replace dependency on extructures with mathcomp-finmap.~~ (Missing operations. See #66 )
• [x] Fix Sigma protocol example.
• [ ] Update documentation

The file fmap_extra could be of interest upstream.

[MarkusKL]

I created a draft PR here to track the progress of replacing the inductively defined choice_type with the extensible set of countType. https://github.com/MarkusKL/ssprove/pull/1

[MarkusKL]

This PR is ready for review.

• I would suggest merging this into a new branch e.g. towards-nominals, so that all breaking changes can be introduced at once.
• Does the loc_rel invariant need to be fixed? The idea is cool, but it is not used anywhere in this codebase and the current automation/lemmas for it looks to be insufficient. It would be nice to pursue some other time.
• The MC-dev build is failing, but I do not think it is due to changes that I introduced. Is it possible to rebuild main and see if it also fails currently?

[4ever2]

• The MC-dev build is failing, but I do not think it is due to changes that I introduced. Is it possible to rebuild main and see if it also fails currently?

It's not currently possible to trigger a run manually, but I agree that it isn't due to these changes. Looks like its due to https://github.com/math-comp/math-comp/pull/1354

[4ever2]

The problem with mathcomp master is now fixed.

• I would suggest merging this into a new branch e.g. towards-nominals, so that all breaking changes can be introduced at once.

I created the towards-nominals branch so that you can target that branch in this PR if you want to merge it that way.

[MarkusKL]

Thanks. I changed the base branch. Feel free to merge. I will make a thorough update of the documentation after more changes.

[spitters]

This is a great contribution. @4ever2 has reviewed it, so feel free to move ahead, but please add documentation first :-)

Could you elaborate on this:

Custom reasoning about fset needs to be redone, but almost all of it should be automatic.

[4ever2]

• Does the loc_rel invariant need to be fixed? The idea is cool, but it is not used anywhere in this codebase and the current automation/lemmas for it looks to be insufficient. It would be nice to pursue some other time.

Could you perhaps open an issue so we don't forget this?

[4ever2]

We are not merging into main yet, and many other breaking changes are coming in the next PRs, so let's wait with the documentation.

Lasse also approved the changes, so let's merge it.