More parallelism + better understandability for snapshot tests (#96)

This PR builds on #95, separating out the various snapshot tests that
were previously merged via
[`inline-crate`](https://crates.io/crates/inline-crate).

examples/_get_latest.sh

@@ -0,0 +1,63 @@
+#! /bin/bash
+
+# This script exposes the `get_latest` function that reads the following
+# variables:
+#
+#    GITHUB_ORG
+#    GITHUB_REPO
+#    GITHUB_BRANCH
+#    MOVE_PATHS
+#    FORCE_REFORMAT_PATHS
+#
+# It then downloads the project, moves all the paths from `MOVE_PATHS` into the
+# directory, and if `FORCE_REFORMAT_PATHS` is set, then forcefully reformats the
+# files in those paths.
+
+function get_latest() {
+    echo "[INFO] Cleaning any existing files"
+    rm -rf "${GITHUB_REPO}.zip" "${GITHUB_REPO}-${GITHUB_BRANCH}"
+    # shellcheck disable=SC2086
+    rm -rf $MOVE_PATHS
+
+    echo "[INFO] Downloading latest version of ${GITHUB_ORG}/${GITHUB_REPO}"
+    wget --quiet -O "${GITHUB_REPO}.zip" "https://github.com/${GITHUB_ORG}/${GITHUB_REPO}/archive/refs/heads/${GITHUB_BRANCH}.zip"
+
+    echo "[INFO] Unzipping ${GITHUB_REPO}"
+    unzip -q "${GITHUB_REPO}.zip"
+
+    echo "[INFO] Moving files"
+    for path in $MOVE_PATHS; do
+        echo "       ... $path"
+        if [ -d "${GITHUB_REPO}-${GITHUB_BRANCH}/$path" ]; then
+            # Directory, move all the .rs files, including those in subdirectories, creating the necessary directories
+            mkdir -p "$path"
+            find "${GITHUB_REPO}-${GITHUB_BRANCH}/$path" -name '*.rs' -print0 | while IFS= read -r -d '' file; do
+                relative_path=$(realpath --relative-to="${GITHUB_REPO}-${GITHUB_BRANCH}" "$file")
+                dirname=$(dirname "$relative_path")
+                mkdir -p "$dirname"
+                mv "$file" "$relative_path"
+            done
+        else
+            # File
+            mkdir -p "$(dirname "$path")"
+            mv "${GITHUB_REPO}-${GITHUB_BRANCH}/$path" "$path"
+        fi
+    done
+
+    # Until these files are formatted on the branch, we want to just manually
+    # reformat it locally, to minimize the diff for the snapshots
+    if [ "$FORCE_REFORMAT_PATHS" != "" ]; then
+        echo "[INFO] Reformatting paths not yet already formatted within ${GITHUB_REPO} '${GITHUB_BRANCH}'"
+        for path in $FORCE_REFORMAT_PATHS; do
+            echo "       ... $path"
+            if [ -d "$path" ]; then
+                find "$path" -name '*.rs' -exec verusfmt {} \;
+            else
+                verusfmt "$path"
+            fi
+        done
+    fi
+
+    echo "[INFO] Cleaning up"
+    rm -rf "${GITHUB_REPO}-${GITHUB_BRANCH}" "${GITHUB_REPO}.zip"
+}

examples/ironfleet-snapshot/get_latest.sh

@@ -0,0 +1,16 @@
+#! /bin/bash
+
+set -e
+set -o pipefail
+
+SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )"
+cd "$SCRIPT_DIR"
+source ../_get_latest.sh
+
+GITHUB_ORG=verus-lang
+GITHUB_REPO=verified-ironkv
+GITHUB_BRANCH=main
+MOVE_PATHS="ironsht/src"
+FORCE_REFORMAT_PATHS="ironsht/src"
+
+get_latest

examples/ironfleet-snapshot/ironsht/src/abstract_end_point_t.rs

@@ -0,0 +1,25 @@
+#![verus::trusted]
+
+use builtin::*;
+use builtin_macros::*;
+use vstd::prelude::*;
+
+verus! {
+
+// This translates ironfleet's NodeIdentity type.
+pub struct AbstractEndPoint {
+    pub id: Seq<u8>,
+}
+
+impl AbstractEndPoint {
+    // Translates Common/Native/Io.s.dfy0
+    pub open spec fn valid_physical_address(self) -> bool {
+        self.id.len() < 0x100000
+    }
+
+    pub open spec fn abstractable(self) -> bool {
+        self.valid_physical_address()
+    }
+}
+
+} // verus!

examples/ironfleet-snapshot/ironsht/src/abstract_parameters_t.rs

@@ -0,0 +1,24 @@
+#![verus::trusted]
+
+use builtin::*;
+use builtin_macros::*;
+use vstd::prelude::*;
+
+verus! {
+
+pub struct AbstractParameters {
+    pub max_seqno: nat,
+    pub max_delegations: nat,
+}
+
+impl AbstractParameters {
+    // Translates Impl/SHT/Parameters::StaticParams
+    pub open spec fn static_params() -> AbstractParameters {
+        AbstractParameters {
+            max_seqno: 0xffff_ffff_ffff_ffff as nat,
+            max_delegations: 0x7FFF_FFFF_FFFF_FFFF as nat,
+        }
+    }
+}
+
+} // verus!

examples/ironfleet-snapshot/ironsht/src/abstract_service_t.rs

@@ -0,0 +1,30 @@
+#![verus::trusted]
+
+use vstd::map::*;
+use vstd::modes::*;
+use vstd::multiset::*;
+use vstd::seq::*;
+use vstd::set::*;
+
+use builtin::*;
+use builtin_macros::*;
+use vstd::pervasive::*;
+
+use crate::app_interface_t::*;
+use crate::keys_t::*;
+use crate::message_t::*;
+use crate::single_message_t::*;
+
+verus! {
+
+pub enum AppRequest {
+    AppGetRequest { seqno: nat, key: AbstractKey },
+    AppSetRequest { seqno: nat, key: AbstractKey, ov: Option<AbstractValue> },
+}
+
+pub enum AppReply {
+    AppReply { g_seqno: nat, key: AbstractKey, ov: Option<AbstractValue> },
+}
+
+} // verus!
+// verus

examples/ironfleet-snapshot/ironsht/src/app_interface_t.rs

@@ -0,0 +1,43 @@
+#![verus::trusted]
+
+use crate::keys_t::*;
+use vstd::map::*;
+use vstd::modes::*;
+use vstd::multiset::*;
+use vstd::seq::*;
+use vstd::set::*;
+
+use builtin::*;
+use builtin_macros::*;
+use vstd::pervasive::*;
+
+verus! {
+
+pub type AbstractValue = Seq<u8>;
+
+pub type Hashtable = Map<AbstractKey, AbstractValue>;
+
+// Translates Services/SHT/AppInterface.i.dfy :: max_val_len
+pub open spec fn max_val_len() -> int {
+    1024
+}
+
+// Translates Services/SHT/AppInterface.i.dfy :: ValidKey
+pub open spec fn valid_key(key: AbstractKey) -> bool {
+    true
+}
+
+// Translates Services/SHT/AppInterface.i.dfy :: ValidValue
+pub open spec fn valid_value(value: AbstractValue) -> bool {
+    value.len() < max_val_len()
+}
+
+// Protocol/SHT/Delegations.i.dfy ExtractRange
+pub open spec fn extract_range(h: Hashtable, kr: KeyRange<AbstractKey>) -> Hashtable {
+    Map::<AbstractKey, AbstractValue>::new(
+        |k: AbstractKey| h.dom().contains(k) && kr.contains(k),
+        |k: AbstractKey| h[k],
+    )
+}
+
+} // verus!

examples/ironfleet-snapshot/ironsht/src/args_t.rs

@@ -0,0 +1,56 @@
+#![verus::trusted]
+
+use vstd::prelude::*;
+use vstd::seq::*;
+use vstd::seq_lib::*;
+
+verus! {
+
+pub type AbstractArg = Seq<u8>;
+
+pub type AbstractArgs = Seq<AbstractArg>;
+
+pub type Arg = Vec<u8>;
+
+pub type Args = Vec<Arg>;
+
+/// Clone a Vec<u8>.
+///
+/// Implemented as a loop, so might not be as efficient as the
+/// `std::vec::Vec::clone` method.
+// TODO: implemented to avoid depending on (and waiting for) Vec::clone,
+// which is made complicated by how it should treat its generic type
+// parameter. Here the elements are u8 which are easy to deal with.
+pub fn clone_vec_u8(v: &Vec<u8>) -> (out: Vec<u8>)
+    ensures
+        out@ == v@,
+{
+    let mut out: Arg = Vec::with_capacity(v.len());
+    let mut i = 0;
+    while i < v.len()
+        invariant
+            i <= v.len(),
+            i == out.len(),
+            forall|j| #![auto] 0 <= j < i ==> out@[j] == v@[j],
+    {
+        out.push(v[i]);
+        i = i + 1;
+    }
+    proof {
+        assert_seqs_equal!(out@, v@);
+    }
+    out
+}
+
+pub fn clone_arg(arg: &Arg) -> (out: Arg)
+    ensures
+        out@ == arg@,
+{
+    clone_vec_u8(arg)
+}
+
+pub open spec fn abstractify_args(args: Args) -> AbstractArgs {
+    args@.map(|i, arg: Arg| arg@)
+}
+
+} // verus!