Restructure configuration to support referencing multiple contracts

Jenkinsfile

@@ -21,7 +21,7 @@ pipeline {
       }
     }
     stage('Test') {
-      options { timeout(time: 15, unit: 'MINUTES') }
+      options { timeout(time: 30, unit: 'MINUTES') }
       parallel {
         stage('Unit')             { steps { sh 'make test-unit     -j8' } }
         stage('Symbolic')         { steps { sh 'make test-symbolic -j2' } }
@@ -31,7 +31,7 @@ pipeline {
     stage('Integration Proofs') { 
       options { timeout(time: 180, unit: 'MINUTES') }
       stages {
-        stage('Audit Proofs') { steps { sh 'make dexter-prove lqt-prove lb-prove -j4' } }
+        stage('Audit Proofs') { steps { sh 'make dexter-prove lb-prove -j4' } }
       }
     }
     stage('Cross Test') {

Makefile

@@ -143,7 +143,7 @@ defn-k:      defn-llvm defn-prove defn-symbolic
 defn-compat: defn-contract-expander defn-extractor defn-input-creator defn-output-compare
 
 build:        build-k build-compat
-build-k:      build-llvm build-prove build-symbolic build-dexter build-lqt
+build-k:      build-llvm build-prove build-symbolic build-dexter build-lb build-lqt
 build-compat: build-contract-expander build-extractor build-input-creator build-output-compare
 
 # LLVM

common.md

@@ -334,29 +334,7 @@ eleven 'anywhere' rules here.
 Michelson Internal Representation Conversion
 --------------------------------------------
 
-This function converts the `other_contracts` field into its internal
-represetation.
-
-```k
-  syntax Map ::= #OtherContractsMapToKMap(OtherContractsMapEntryList)              [function]
-               | #OtherContractsMapToKMap(String, Map, OtherContractsMapEntryList) [function]
-  // ----------------------------------------------------------------------------------------
-  rule #OtherContractsMapToKMap( .OtherContractsMapEntryList ) => .Map
-  rule #OtherContractsMapToKMap( Contract A T ; Rs )
-    => #OtherContractsMapToKMap(A, #BuildAnnotationMap(.FieldAnnotation, T), Rs)
-
-  rule #OtherContractsMapToKMap(A, TypeMap, Rs) =>
-       #BuildOtherContractsMap(#Address(A), TypeMap) #OtherContractsMapToKMap(Rs)
-
-  syntax Map ::= #BuildOtherContractsMap(Address, Map) [function]
-  // ------------------------------------------------------------
-  rule #BuildOtherContractsMap(A, FA:FieldAnnotation |-> T:TypeName TypeMap:Map)
-    => A . FA |-> T #BuildOtherContractsMap(A, TypeMap)
-
-  rule #BuildOtherContractsMap(_, .Map) => .Map
-```
-
-This function converts all other datatypes into their internal represenations.
+This function converts datatypes into their internal represenations.
 
 ```k
   syntax DataOrSeq ::= Data | DataList | MapEntryList // Can't subsort DataList to Data, as that would form a cycle.
@@ -597,16 +575,21 @@ a contract lookup.
           => Transfer_tokens
               #MichelineToNative(
                   P,
-                  #Type({KnownAddrs [ #ParseEntrypoint(A) ]}:>TypeName),
+                  #Type(#LookupEntrypoint(KnownAddrs, #ParseEntrypoint(A))),
                   KnownAddrs,
                   BigMaps
               )
               #Mutez(M)
               #ParseEntrypoint(A)
               N
        requires (isWildcard(N) orBool isInt(N))
-        andBool #ParseEntrypoint(A) in_keys(KnownAddrs)
         andBool #IsLegalMutezValue(M)
+
+  syntax TypeName ::= #LookupEntrypoint(Map, Entrypoint) [function]
+  // --------------------------------------------------------------
+  rule #LookupEntrypoint(Entrypoints, A . FA) => { { Entrypoints [ A ] }:>Map [ FA ] }:>TypeName
+    requires A in_keys(Entrypoints)
+     andBool FA in_keys( { Entrypoints [ A ] }:>Map )
 ```
 
 We extract a `big_map` by index from the bigmaps map. Note that these have

compat.md

@@ -820,5 +820,12 @@ module OUTPUT-COMPARE
        <knownaddrs> _ => #OtherContractsMapToKMap(M) </knownaddrs>
 
   rule <k> real_output AOS ; output EOS => #CheckOutput(EOS, AOS) ... </k>
+
+  syntax Map ::= #OtherContractsMapToKMap(OtherContractsMapEntryList)              [function]
+               | #OtherContractsMapToKMap(String, Map, OtherContractsMapEntryList) [function]
+  // ----------------------------------------------------------------------------------------
+  rule #OtherContractsMapToKMap( .OtherContractsMapEntryList ) => .Map
+  rule #OtherContractsMapToKMap( Contract A T ; Rs )
+    => #Address(A) |-> #BuildAnnotationMap(.FieldAnnotation, T) #OtherContractsMapToKMap(Rs)
 endmodule
 ```