Formal variable-width family refinement gate

.github/actions/checkout-dev-siblings/action.yml

@@ -66,7 +66,38 @@ runs:
                 "$remote" "$event_ref" >/dev/null 2>&1
             then
               selected_ref="$event_ref"
-            else
+            elif [ "$repo" = "vinary-tree-interop" ]; then
+              # Prefer the exact public version declared by this checkout's
+              # path dependency when no coordinated development branch exists.
+              # This keeps development branches flexible while preventing a
+              # stale sibling default (for example RC4) from satisfying an
+              # exact RC6 requirement.
+              required_version="$(
+                sed -nE \
+                  '/^[[:space:]]*vinary-tree-interop[[:space:]]*=/{s/.*version[[:space:]]*=[[:space:]]*"=([^" ]+)".*/\1/p;}' \
+                  "$GITHUB_WORKSPACE/Cargo.toml" | head -n 1
+              )"
+              tagged_ref="v$required_version"
+              if [ -n "$required_version" ] && \
+                git ls-remote --exit-code \
+                  "$remote" "refs/tags/$tagged_ref" >/dev/null 2>&1
+              then
+                selected_ref="$tagged_ref"
+              elif [ -n "$required_version" ] && \
+                git ls-remote --exit-code --heads \
+                  "$remote" master >/dev/null 2>&1
+              then
+                # The release branch may publish an exact version on master
+                # before creating a version tag.  Select master only as an
+                # explicit fallback; the post-checkout package-version audit
+                # below remains authoritative and rejects mismatches.
+                selected_ref=master
+              elif [ -n "$required_version" ]; then
+                echo "ERROR: $repo requires $tagged_ref from Cargo.toml, but that upstream ref is unavailable" >&2
+                exit 1
+              fi
+            fi
+            if [ -z "$selected_ref" ]; then
               selected_ref="$development_ref"
             fi
           fi
@@ -83,6 +114,28 @@ runs:
               "https://github.com/vinary-tree/$repo.git" "$dest"
             echo "::endgroup::"
           fi
+          if [ "$repo" = "vinary-tree-interop" ]; then
+            required_version="$(
+              sed -nE \
+                '/^[[:space:]]*vinary-tree-interop[[:space:]]*=/{s/.*version[[:space:]]*=[[:space:]]*"=([^" ]+)".*/\1/p;}' \
+                "$GITHUB_WORKSPACE/Cargo.toml" | head -n 1
+            )"
+            if [ -n "$required_version" ]; then
+              actual_version="$(
+                awk '
+                  /^\[package\]$/ { in_package=1; next }
+                  /^\[/ { in_package=0 }
+                  in_package && /^[[:space:]]*version[[:space:]]*=/ {
+                    gsub(/[[:space:]]*"/, "", $3); print $3; exit
+                  }
+                ' "$dest/Cargo.toml"
+              )"
+              if [ "$actual_version" != "$required_version" ]; then
+                echo "ERROR: $repo ref $selected_ref declares $actual_version, but Cargo.toml requires $required_version" >&2
+                exit 1
+              fi
+            fi
+          fi
         done
         echo "Sibling crates available under $parent:"
         ls -1d \

.github/workflows/bindings-conformance.yml

@@ -76,14 +76,18 @@ jobs:
           mkdir -p target/julia-ci-env
           julia --project=target/julia-ci-env -e '
             using Pkg
-            Pkg.develop(path=ENV["GITHUB_WORKSPACE"] * "/../vinary-tree-interop/bindings/julia/VinaryTreeInterop")
-            Pkg.develop(path=ENV["GITHUB_WORKSPACE"] * "/bindings/julia/Libdictenstein")
+            Pkg.develop([
+              PackageSpec(path=ENV["GITHUB_WORKSPACE"] * "/../vinary-tree-interop/bindings/julia/VinaryTreeInterop"),
+              PackageSpec(path=ENV["GITHUB_WORKSPACE"] * "/bindings/julia/Libdictenstein")
+            ])
             Pkg.test("Libdictenstein")
           '
           julia --project=bindings/julia/Libdictenstein/docs -e '
             using Pkg
-            Pkg.develop(path=ENV["GITHUB_WORKSPACE"] * "/../vinary-tree-interop/bindings/julia/VinaryTreeInterop")
-            Pkg.develop(path=ENV["GITHUB_WORKSPACE"] * "/bindings/julia/Libdictenstein")
+            Pkg.develop([
+              PackageSpec(path=ENV["GITHUB_WORKSPACE"] * "/../vinary-tree-interop/bindings/julia/VinaryTreeInterop"),
+              PackageSpec(path=ENV["GITHUB_WORKSPACE"] * "/bindings/julia/Libdictenstein")
+            ])
             Pkg.instantiate()
             include("bindings/julia/Libdictenstein/docs/make.jl")
           '

.github/workflows/ci.yml

@@ -199,9 +199,9 @@ jobs:
       - uses: taiki-e/install-action@cargo-llvm-cov
       - name: Run coverage
         run: |
-          cargo llvm-cov --all-features --branch \
+          cargo +nightly llvm-cov --all-features --branch \
             --lcov --output-path lcov.info
-          cargo llvm-cov report --branch \
+          cargo +nightly llvm-cov report --branch \
             --cobertura --output-path cobertura.xml
       - name: Upload coverage to Codecov
         uses: codecov/codecov-action@v4
@@ -355,6 +355,59 @@ jobs:
           TLA_JAVA_HEAP: "3g"
         run: prlimit --as="$FORMAL_MEM_LIMIT_BYTES" --rss="$FORMAL_MEM_LIMIT_BYTES" -- bash scripts/verify-formal-correspondence.sh
 
+  # -----------------------------------------------------------------
+  # Variable-width family/profile gate. This is the exact preimplementation
+  # gate for the committed Rocq/TLA+ family-refinement source tuple, including
+  # safe models and every required negative control. GitHub-hosted runners do
+  # not expose a user systemd bus, so the verifier uses prlimit here while
+  # retaining systemd-run caps for local execution.
+  # -----------------------------------------------------------------
+  variable-width-formal:
+    name: Variable-width formal gate
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - uses: ./.github/actions/checkout-dev-siblings
+      - uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: "5.2"
+      - uses: actions/setup-java@v5
+        with:
+          distribution: temurin
+          java-version: "21"
+      - name: Install Rocq and TLA+ tools
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y curl ripgrep util-linux
+          # Rocq 9.1.1 is distributed in opam through the compatibility
+          # package name [coq]; pinning the version still selects the Rocq
+          # toolchain and avoids Ubuntu's older apt package.
+          opam install --yes coq.9.1.1
+          eval "$(opam env)"
+          echo "$(opam var bin)" >> "$GITHUB_PATH"
+          curl -L \
+            https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar \
+            -o tla2tools.jar
+          sudo mkdir -p /opt/tla
+          sudo mv tla2tools.jar /opt/tla/tla2tools.jar
+          sudo tee /usr/local/bin/tla2sany >/dev/null <<'EOF'
+          #!/usr/bin/env bash
+          exec java -Xmx"${TLA_JAVA_HEAP:-512m}" -cp /opt/tla/tla2tools.jar tla2sany.SANY "$@"
+          EOF
+          sudo tee /usr/local/bin/tlc >/dev/null <<'EOF'
+          #!/usr/bin/env bash
+          exec java -Xmx"${TLA_JAVA_HEAP:-512m}" -cp /opt/tla/tla2tools.jar tlc2.TLC "$@"
+          EOF
+          sudo chmod +x /usr/local/bin/tla2sany /usr/local/bin/tlc
+      - name: Run capped variable-width formal gate
+        env:
+          VARIABLE_WIDTH_FORMAL_RESOURCE_CONTROL: external
+          VARIABLE_WIDTH_FORMAL_TIMEOUT_SECONDS: "7200"
+          VARIABLE_WIDTH_TLC_JAVA_OPTIONS: "-Xms64m -Xmx512m -XX:+UseParallelGC"
+        run: bash scripts/verify-variable-width-formal.sh
+      - name: Run invariant-derived reference harness
+        run: prlimit --rss=2147483648 -- cargo test --manifest-path formal-verification/Cargo.toml --test variable_width_formal_harness
+
   # -----------------------------------------------------------------
   # Miri unsafe-boundary checks. Runs on nightly because `cargo miri`
   # is a nightly component.
@@ -394,12 +447,13 @@ jobs:
         env:
           CARGO_BUILD_JOBS: "2"
           FORMAL_MEM_LIMIT_BYTES: "8589934592"
-        run: prlimit --as="$FORMAL_MEM_LIMIT_BYTES" --rss="$FORMAL_MEM_LIMIT_BYTES" -- cargo miri setup
+        run: prlimit --as="$FORMAL_MEM_LIMIT_BYTES" --rss="$FORMAL_MEM_LIMIT_BYTES" -- cargo +nightly miri setup
       - name: Run Miri-gated correspondence harness
         env:
           CARGO_BUILD_JOBS: "2"
           FORMAL_MEM_LIMIT_BYTES: "8589934592"
           FORMAL_RESOURCE_CONTROL: external
+          FORMAL_MIRI_TOOLCHAIN: nightly
           RUN_MIRI: "1"
           TLA_JAVA_HEAP: "3g"
         run: prlimit --as="$FORMAL_MEM_LIMIT_BYTES" --rss="$FORMAL_MEM_LIMIT_BYTES" -- bash scripts/verify-formal-correspondence.sh

bindings/julia/Libdictenstein/docs/make.jl

@@ -7,7 +7,11 @@ DocMeta.setdocmeta!(Libdictenstein, :DocTestSetup,
 makedocs(
     modules=[Libdictenstein],
     sitename="Libdictenstein.jl",
-    strict=true,
+    # Documenter 1.x removed the legacy `strict` keyword.  An empty
+    # `warnonly` list preserves fail-closed documentation diagnostics, while
+    # `checkdocs=:all` retains strict API coverage checking.
+    warnonly=Symbol[],
+    checkdocs=:all,
     doctest=true,
     pages=[
         "Guide" => "index.md",

docs/algorithms/README.md

@@ -8,6 +8,9 @@ The Dictionary Layer is the family of dictionary backends provided by **libdicte
 
 This layer abstracts over different data structures (tries, DAWGs, double-array tries) through common traits, allowing you to choose the best backend for your specific use case while maintaining a consistent API.
 
+For the topology/profile split, canonical UTF-8 and ULEB128 boundaries, and
+interned-ID identity rules, see [variable-width logical profiles](variable-width-profiles.md).
+
 ## Architecture
 
 <img src="../diagrams/algorithms-backend-family.svg" alt="The Dictionary Layer trait API (Dictionary, MappedDictionary, DictionaryNode) sits above three in-memory backend families - Trie, DAWG, and Suffix Automaton; the Trie family holds DoubleArrayTrie (the recommended default) and DAT-Char (UTF-8), and the DAWG family holds DynamicDawg." width="70%"/>
@@ -559,7 +562,7 @@ For concurrent writes, dictionaries have different strategies:
 |-----------|----------|--------|-------|
 | DoubleArrayTrie | `Persistent` | Rebuild + atomic swap | Append-only via builder |
 | DynamicDawg | `InternalSync` | Direct mutation | Internal RwLock |
-| PathMapDictionary | `InternalSync` | Direct mutation | Internal RwLock |
+| PathMapDictionary | `ArcSwap` copy-on-write | Clone, transform, and CAS-publish an immutable root | Readers take one snapshot and never block; competing writers retry from the winning root |
 
 ## Advanced Topics