New structure for specification tests

[gtrepta]

Issue

Our current testing framework for proofs is doing everything under a single subfolder with a single verification module:

simple-proofs
├── verification.md
├── list-free.md
├── list-length.md
├── ...
├── verification
    ├── haskell
        ├── <kompiled verification module>

For uplc-to-k to generate specifications for contracts, it will need to kompile its own VERIFICATION module for them where things like the global environment and scott encoding summaries can live

Solution

We can mirror what KEVM is doing and break down proofs into subtrees with their own verification modules:

tests
├── specs
    ├── verification-common.md
    ├── simple
        ├── verification.md
        ├── list-free.md
        ├── list-length.md
        ├── ...
    ├── uplc-to-k
        ├── true.uplc
        ├── genv.uplc
        ├── freeTruePolicy.uplc
        ├── ...
    ├── ...

tests/specs/simple can be handled the same way it's being handled for simple-proofs/.

Note the tests/specs/verification-common.md file, which holds simplification rules that are common to all proofs which they can import.

But the testing framework can use uplc-to-k on the contracts in tests/specs/uplc-to-k to generate their own subfolders and kompile/run their respective verification/claim modules. So tests/specs/uplc-to-k/freeTruePolicy.uplc will make for example:

tests
├── specs
    ├── uplc-to-k
        ├── freeTruePolicy
            ├── verification.k
            ├── freeTruePolicy-spec.k
            ├── haskell
                ├── <kompiled verification module>

[ChristianoBraga]

For binsearch I was experimenting with a directory structure that would allow each contract/uplc to have its own directory, with its own verification.k, and verification sub dir. Also, the possibility of common files to be imported, not only one, to allow inclusion of global environment instances for different sources such as Plutus, DJed and other things that may appear. Maybe:

tests/specs/
  Plutus-global-environment-instance.k
  DJed-global-environment-instance.k
  /free-true-policy/
   free-true-policy.md
   verification.md
   verification/
  /stablecoin/
   ... 
  /nft/
   ... 

Maybe Djed would deserve a directory of its own, with sub dir for its constracts but maybe we should start simple.