Benchmark/vendor examples specs

NOTICE

@@ -10,6 +10,11 @@ applicable upstream license; the protocols and proof obligations are unchanged.
 
 Benchmark groups live under benchmark/proof-completion/ (proof completion) and
 benchmark/proof-from-scratch/ (proof from scratch).
+Where a benchmark copy names an upstream module-level assumption, the statement
+is upstream's and only the name is added. A proof has to cite an assumption to
+use it -- tlapm puts none of them in the context of an obligation -- and a name
+is the legible way to do so; repeating the statement verbatim in a BY clause
+works too.
 Full license texts for Apache-2.0 and BSD-2-Clause material are provided in
 LICENSES/Apache-2.0.txt and LICENSES/BSD-2-Clause.txt, respectively.
 
@@ -72,6 +77,109 @@ tlaplus/Examples  —  MIT, except where noted below  —  https://github.com/tl
         -- as proof-from-scratch targets graded by tlapm. The upstream example
         asks redistributors to review the external artifact's licensing and
         attribution requirements.
+      - tlaplus_examples_bosco — MIT: the benchmark model corresponds to
+        bosco.tla at commit 1ef5f158cc1743975441dd94c280e56c8fd06766:
+        https://github.com/tlaplus/Examples/tree/1ef5f158cc1743975441dd94c280e56c8fd06766/specifications/bosco
+        A TLA+ encoding by Igor Konnov, Thanh Hai Tran, and Josef Widder (2016)
+        of the one-step Byzantine asynchronous consensus algorithm from Yee Jiun
+        Song and Robbert van Renesse, "Bosco: One-Step Byzantine Asynchronous
+        Consensus" (DISC 2008). The upstream module states no theorems, so the
+        benchmark copy adds five: `Spec => []P` for each invariant P that the
+        upstream TLC configuration (bosco.cfg) checks -- TypeOK and the
+        agreement lemmas Lemma3_0, Lemma3_1, Lemma4_0, Lemma4_1. The upstream
+        OneStep0 and OneStep1 properties are not benchmark targets: they hold
+        only for more than 7*T processes, which the module's assumptions do not
+        state.
+      - tlaplus_examples_Disruptor — MIT: the benchmark models correspond to
+        Disruptor_MPMC.tla, Disruptor_SPMC.tla and RingBuffer.tla at commit
+        45c1cfd7ed40d9287b1c2ac51a05a7cb750e0521:
+        https://github.com/tlaplus/Examples/tree/45c1cfd7ed40d9287b1c2ac51a05a7cb750e0521/specifications/Disruptor
+        By Nicholas Schultz-Møller, modelling the Rust Disruptor implementation
+        in https://github.com/nicholassm/disruptor-rs; the Disruptor ring-buffer
+        data structure originates from LMAX Exchange. The upstream modules state
+        no theorems, so the benchmark copies add two per variant: `Spec => []P`
+        for each invariant P that the upstream TLC configurations check --
+        TypeOk and NoDataRaces. Upstream names the assumptions of all three
+        modules, states that Writers and Readers are disjoint, and EXTENDs
+        Naturals and FiniteSets in RingBuffer rather than instantiating them
+        LOCALly, and assumes in Disruptor_SPMC that Writers is a finite set of
+        cardinality one, without which two writers claim the same slot and both
+        of that module's goals are false. The benchmark copies therefore
+        deviate from upstream in the theorems alone. The upstream Liveliness property
+        is not a benchmark target: it lives in MCDisruptor_MPMC and
+        MCDisruptor_SPMC, where TLC checks it under the state constraint that
+        bounds the model, which is not sound evidence for a liveness property.
+      - tlaplus_examples_braf — MIT: the benchmark models correspond to
+        BufferedRandomAccessFile.tla at commit
+        0e018bcffe93c775c5c8ec30989065d9d4eabfc1:
+        https://github.com/tlaplus/Examples/tree/0e018bcffe93c775c5c8ec30989065d9d4eabfc1/specifications/braf
+        Copyright (c) 2024, Oracle and/or its affiliates; by Calvin Loncaric. A
+        specification of tlc2.util.BufferedRandomAccessFile, the caching layer
+        TLC uses for filesystem access, copied from
+        https://github.com/tlaplus/tlaplus. Upstream holds all three modules
+        (BufferedRandomAccessFile, RandomAccessFile, Common) in one file, which
+        tlapm cannot load, so the benchmark copies split them into one file per
+        module -- a mechanical split with no change to the text. The upstream
+        modules state no theorems and no assumptions, so the benchmark copies
+        add fourteen theorems -- one per invariant and property that the
+        upstream TLC configuration checks, including the refinement of
+        RandomAccessFile -- and the three assumptions that the constants'
+        upstream comments describe (MaxOffset \in Nat, BuffSz \in Nat \ {0},
+        ArbitrarySymbol \notin Symbols), without which the theorems do not hold
+        for arbitrary constant values. Inv2 is not a benchmark target: upstream
+        excludes it from the invariants deliberately, treating it as an action
+        precondition, and states Inv2CanAlwaysBeRestored instead.
+      - tlaplus_examples_btree — MIT: the benchmark models correspond to
+        btree.tla and kvstore.tla at commit
+        f2f1f982a5c8c17dfbbd44c5b84032aeb021bb10:
+        https://github.com/tlaplus/Examples/tree/f2f1f982a5c8c17dfbbd44c5b84032aeb021bb10/specifications/btree
+        By Lorin Hochstein, from https://github.com/lorin/btree-tla. The
+        benchmark copy rewrites the recursive operator FindLeafNode as a
+        recursive function, which TLAPS supports and recursive operators are
+        not; TLC explores the same 2,820,091 states (374,727 distinct) under the
+        upstream MCbtree configuration before and after the rewrite. Upstream
+        states the assumptions the algorithm needs -- the control states are
+        ten distinct values, the keys are strictly totally ordered under <, the
+        branching factor is at least two, and the node pool is non-empty -- so
+        btree.tla deviates in five theorems alone, one per invariant the
+        upstream configuration checks except FreeNodesRemain, which is a
+        statement about the model's MaxNode rather than about the tree.
+        kvstore.tla additionally carries names for its two assumptions, which
+        are still anonymous upstream. The upstream Refinement property is
+        commented out of the configuration and is therefore not a target.
+      - tlaplus_examples_NanoBlockchain — MIT: the benchmark model corresponds
+        to Nano.tla at commit 0e018bcffe93c775c5c8ec30989065d9d4eabfc1:
+        https://github.com/tlaplus/Examples/tree/0e018bcffe93c775c5c8ec30989065d9d4eabfc1/specifications/NanoBlockchain
+        By Andrew Helwer, a specification of the Nano cryptocurrency protocol.
+        The benchmark copy rewrites the recursive operators PublicKeyOf,
+        BalanceAt, ValueOfSendBlock and SumBag as recursive functions, which
+        TLAPS supports and recursive operators are not; ValueOfSendBlock is
+        inlined so that the mutual recursion becomes a single function, and
+        SumBag sums each distinct element times its multiplicity rather than
+        removing one copy at a time. TLC explores the same state spaces under
+        the upstream configurations before and after the rewrite (6,083 states /
+        3,003 distinct for MCNanoSmall; 1,120,079 / 530,587 for MCNanoMedium).
+        The upstream Safety theorem is kept as the benchmark target.
+      - tlaplus_examples_dag-consensus — MIT: the benchmark models correspond to
+        Sailfish.tla, BlockDag.tla, Digraph.tla and Utils.tla at commit
+        47b0e2cc0268836b89f5ce451f38e5df5f1cf773:
+        https://github.com/tlaplus/Examples/tree/47b0e2cc0268836b89f5ce451f38e5df5f1cf773/specifications/dag-consensus
+        By Giuliano Losa, from https://github.com/nano-o/dag-consensus; a
+        specification of the Sailfish and Sailfish++ DAG-based consensus
+        algorithms. The benchmark copies rewrite the recursive operators
+        OrderSet, Linearize and Descendants as recursive functions, which TLAPS
+        supports and recursive operators are not; TLC explores the same 314,144
+        states (109,604 distinct) under TLCSailfish1 before and after the
+        rewrite. The upstream module states no theorems, so the copy adds three
+        -- one per invariant the upstream TLC configurations check (TypeOK,
+        Agreement, Liveness) -- together with the quorum-system assumptions that
+        TLCSailfish1 and TLCSailfish2 describe for their concrete choices (two
+        quorums share a correct node; a blocking set contains a correct node and
+        meets every quorum), which upstream leaves to the instantiating module.
+        Both harnesses instantiate Sailfish rather than extending it, and TLC
+        checks the assumptions of a module it extends but not of one it
+        instantiates, so the four assumptions were checked by evaluating them
+        against each harness's constants in a module of their own.
 
 OpenAddressing  —  MIT  —  benchmark group OpenAddressing
     By Markus A. Kuppe, from the mku-OA branch of https://github.com/lemmy/Examples