Remove trim and internalize locations

[MarkusKL]

(This builds upon #69, so until it is merged the diff also includes those changes - A representative diff can be seen here for now MarkusKL#5).
This is the final PR with breaking changes to the main codebase, so afterwards the focus is to merge #70.
In parallel, I will add the nominal operators as an optional import.

This PR makes the following improvements:

• ValidPackage is strengthened to subsume the concept of trimmed i.e.
  ValidPackage (old) + trimmed (old) <-> ValidPackage (new)
  This has minimal impact on the examples except for the fact that it may have revealed an adequacy bug in Fiat-Shamir construction (see comment and changes in code). Changes to e.g. KEMDEM are strict simplifications of the code.
• The locations parameter has been internalized, so that package is parameterized only by imports and exports. To reduce the amount of definitions about packages (avoiding the package vs. loc_package dichotomy). Games for interface I are now captured by the notation game I := package [interface] I and adversaries for I are captured by the notation adversary I := package I A_export. This makes if easy to define a game pair for I as bool -> game I even if the two game use different locations.

Breaking changes:

• trim is removed. Trim a package using link by changing trim E p to ID E o p.
• trimmed is removed. Every ValidPackage is trimmed, so trimmed side conditions are gone from lemmas.
• package takes only two parameters I and E making it more like the old loc_package.
• [package ... ] notation takes the locations of the defined package as first parameter.
• User proofs about package validity need to be updated, but most can probably be remove due to automation from Base Locations and Interfaces on finite maps. #65 .

[MarkusKL]

This example shows why I think the current definition of ValidPackage is flawed:

Module Danger.
  Definition innocent_package b :
    package fset0 [interface] [interface #val #[ 1 ] : 'unit → 'bool ]
  := [package #def #[ 1 ] (_ : 'unit) : 'bool { ret b } ].

  Instance bad_instance {p} : ValidPackage fset0 [interface] fset0 p.
  Proof.
    apply prove_valid_package => o.
    rewrite in_fset0 //.
  Qed.

  (* This is provable because bad_instance gets derived as the instance for ValidPackage,
      which determines the imports of the adversary *)
  Lemma bad_lemma : innocent_package true ≈₀ innocent_package false.
  Proof.
    apply eq_rel_perf_ind_eq.
    intros n S T x. rewrite in_fset0 //.
  Qed.
End Danger.

This code is validated currently on main.

[Copilot]

Pull Request Overview

This PR removes the old trimming mechanism and internalizes package locations while simplifying the package interface and composition operations.

• Eliminates the trim/trimmed operations, making every ValidPackage trimmed by construction.
• Updates package composition operations (link, par) to rely on new conditions (fseparate, fcompat) and union operations (unionm).
• Revises documentation in both README.md and DOC.md to reflect the new API changes.

Reviewed Changes

Copilot reviewed 30 out of 48 changed files in this pull request and generated 1 comment.

File	Description
README.md	Updated package type signature and linking lemmas to remove the location parameter and use new compatibility and separation functions.
DOC.md	Revised documentation examples and explanations to match the new API definitions and syntax changes.

Files not reviewed (18)

• _CoqProject: Language not supported
• theories/Crypt/Casts.v: Language not supported
• theories/Crypt/Package.v: Language not supported
• theories/Crypt/Prelude.v: Language not supported
• theories/Crypt/examples/AsymScheme.v: Language not supported
• theories/Crypt/examples/DDH.v: Language not supported
• theories/Crypt/examples/ElGamal.v: Language not supported
• theories/Crypt/examples/Executor.v: Language not supported
• theories/Crypt/examples/KEMDEM.v: Language not supported
• theories/Crypt/examples/MACCCA.v: Language not supported
• theories/Crypt/examples/OTP.v: Language not supported
• theories/Crypt/examples/OVN.v: Language not supported
• theories/Crypt/examples/PRF.v: Language not supported
• theories/Crypt/examples/PRFMAC.v: Language not supported
• theories/Crypt/examples/PRFPRG.v: Language not supported
• theories/Crypt/examples/PRPCCA.v: Language not supported
• theories/Crypt/examples/RandomOracle.v: Language not supported
• theories/Crypt/examples/Schnorr.v: Language not supported

Comments suppressed due to low confidence (1)

DOC.md:519

• The keyword 'raw_pacakge' appears to be misspelled; it should be 'raw_package'.

Advantage (G : bool → raw_pacakge) (A : raw_package) : R

[4ever2]

Looks good. Let's merge once rebased and the typos have been fixed.

[MarkusKL]

Fixed typos. Wrote header for fmap_solve. Rebased on towards-nominals. I am ready to merge and move on to make final review in #70.