Constant time release evidence

* ci: bind equality evidence to exact release binaries

Inspect production comparison paths after final linking and bind call closure, timing, formal results, provenance, and artifacts to the exact release identity. Reject ancestor evidence for a different release commit.

* build: migrate to cargo-rail 0.18

Replace removed config synchronization with semantic migration checks while preserving disabled MSRV policy, push-only release effects, and the tagged v5.1 action contract.

Author: loadingalias

.changes/constant-time-release-evidence-1e18.md

@@ -0,0 +1,7 @@
+---
+"rscrypto" = "patch"
+---
+
+Constant-time release evidence now inspects production equality paths in final
+linked binaries and binds disassembly, symbols, timing, formal results,
+provenance, and hashes to the exact release commit and build configuration.

.config/rail.toml

@@ -28,42 +28,24 @@ targets = [
 include_paths = true
 include_renamed = true
 
-pin_transitives = false
-transitive_host = "root"
-
 strict_version_compat = true
 exact_pin_handling = "warn"
 major_version_conflict = "warn"
-
-msrv = false # Root package MSRV is authoritative; this single-crate workspace does not inherit workspace.package.
-msrv_source = "max"
-
-detect_unused = true
-compiler_diag_cache = true
-remove_unused = true
-
-prune_dead_features = true
 preserve_features = []
-
-detect_undeclared_features = true
-fix_undeclared_features = true
 skip_undeclared_patterns = []
 
 exclude = []
 include = []
 max_backups = 2
-sort_dependencies = true
-enforce_msrv_inheritance = false
 consumer_scope = "open" # Published library: preserve dormant public feature and dependency APIs.
+msrv_policy = { mode = "disabled" } # Root package MSRV remains authoritative in this single-crate workspace.
 
 
 [release]
 tag_prefix = "v"
 tag_format = "{prefix}{version}" # Single crate: vX.Y.Z
 
 require_clean = true
-push = true
-create_github_release = false
 sign_tags = true
 publish_delay = 5
 
@@ -75,7 +57,7 @@ unconventional_commits = "allow"  # Required .changes files own bumps and user-f
 semver_check = "warn"
 change_dir = ".changes"
 require_change_files = ["rscrypto"]
-forge = "auto"  # Release creation provider: auto, github, gitlab
+remote_effects = "push" # Release automation pushes commits/tags; the repository workflow owns forge releases.
 
 [release.changelog]
 path = "CHANGELOG.md"
@@ -107,7 +89,6 @@ infrastructure = [
 ]
 unknown_file_policy = "strict" # Unknown crate files build/test; unknown workspace files run infrastructure checks.
 confidence_profile = "balanced" # Planner confidence profile: strict, balanced, fast
-bot_pr_confidence_profile = "strict" # Optional planner profile override for bot-authored PRs
 
 [change-detection.custom]
 cargo_graph = [

.github/actions/setup/action.yaml

@@ -62,7 +62,7 @@ runs:
       if: inputs.tools-mode != 'none'
       shell: bash
       env:
-        CARGO_RAIL_VERSION: "0.17.3"
+        CARGO_RAIL_VERSION: "0.18.0"
         CARGO_SEMVER_CHECKS_VERSION: "0.48.0"
         TOOLS_MODE: ${{ inputs.tools-mode }}
       run: scripts/ci/install-tools.sh "$TOOLS_MODE"

.github/workflows/_ci-suite.yaml

@@ -77,7 +77,7 @@ jobs:
       run_script: |
         mkdir -p target/cargo-rail
         cargo rail config validate --strict
-        cargo rail config sync --check
+        cargo rail config migrate --check
         cargo rail unify --check --explain --format json \
           --output target/cargo-rail/unify-result.json
       artifact_name: cargo-graph-${{ inputs.cache_key_prefix }}

.github/workflows/ci.yaml

@@ -41,7 +41,7 @@ jobs:
         id: rail
         uses: loadingalias/cargo-rail-action@90f7f739028887508c6e8d8b7cc510dc612eb653  # v5.1.0
         with:
-          version: "0.17.3"
+          version: "0.18.0"
 
       - name: Check Release Intent Coverage
         if: github.event_name == 'pull_request'

.github/workflows/ct.yaml

@@ -170,7 +170,7 @@ jobs:
         if [[ "$raw_artifacts" == "true" ]]; then
           package_args+=(--raw)
         fi
-        python3 scripts/ct/package_evidence.py "${package_args[@]}"
+        scripts/ct/python.sh scripts/ct/package_evidence.py "${package_args[@]}"
 
         exit "$status"
       artifact_name: ct-${{ matrix.artifact_suffix }}

ct.toml

@@ -8,6 +8,61 @@ release_report = "ct-report.json"
 harness = "tools/ct-harness"
 artifact_script = "scripts/ct/artifacts.sh"
 
+[equality_evidence.release_binary]
+name = "rscrypto-ct-evidence"
+kind = "executable"
+profile = "release"
+backend = "llvm"
+features = ["std", "full", "parallel", "diag"]
+default_features = false
+owner_widths = [16, 28, 32, 48, 64, 1632, 2400, 3168]
+owner_symbols = [
+  "ct_entry_owner_eq_16",
+  "ct_entry_owner_eq_28",
+  "ct_entry_owner_eq_32",
+  "ct_entry_owner_eq_48",
+  "ct_entry_owner_eq_64",
+  "ct_entry_owner_eq_1632",
+  "ct_entry_owner_eq_2400",
+  "ct_entry_owner_eq_3168",
+]
+public_len_symbols = [
+  "ct_entry_kmac256_verify",
+  "ct_entry_mlkem512_decapsulate",
+  "ct_entry_mlkem768_decapsulate",
+  "ct_entry_mlkem1024_decapsulate",
+  "ct_entry_argon2i_verify",
+  "ct_entry_argon2d_verify",
+  "ct_entry_argon2id_verify",
+  "ct_entry_scrypt_verify",
+  "ct_entry_rsa_pkcs1v15_sign_fixed_blinding",
+  "ct_entry_rsa_pss_sign_fixed_blinding",
+  "ct_entry_rsa_oaep_decrypt_fixed_blinding",
+  "ct_entry_rsa_pkcs1v15_decrypt_fixed_blinding",
+  "ct_entry_rsa_private_key_pkcs8_roundtrip",
+]
+formal_owner_widths = [16, 32, 48, 64]
+formal_limitation = "BINSEC owner kernels cover the representative 16-, 32-, 48-, and 64-byte production monomorphizations. The 28- and ML-KEM-sized owner monomorphizations require linked-binary disassembly/closure and heuristics on every release lane; BINSEC proof kernels are deferred because they add no caller-selectable shape and the large copies exceed the present proof budget."
+downstream_limitation = "Evidence binds this final linked harness executable and its exact compiler/linker configuration. It does not claim constant-time behavior for arbitrary downstream binaries that rebuild or inline rscrypto differently. Returning bool remains the T3.4 declassification limitation."
+
+[[asm_public_operand]]
+primitive = "password.argon2i"
+root = "ct_entry_argon2i_verify"
+symbol = "rscrypto::auth::argon2::argon2_hash_with_kernel_inner"
+kind = "variable_latency_division"
+max_count = 2
+source = "src/auth/argon2/mod.rs:1751"
+rationale = "The divisions derive matrix dimensions and iteration bounds from validated public Argon2Params and the caller-visible output length. Password and salt contents do not feed the divisors."
+
+[[asm_public_operand]]
+primitive = "password.argon2i"
+root = "ct_entry_argon2i_verify"
+symbol = "rscrypto::auth::argon2::fill_segment_inner"
+kind = "variable_latency_division"
+max_count = 2
+source = "src/auth/argon2/mod.rs:1434"
+rationale = "For the Argon2i retained root, address generation and segment positions are data-independent; these divisions use public lane, segment, and matrix dimensions rather than password-derived contents."
+
 [operation_inventory]
 schema_version = 1
 authority = "ct.toml"
@@ -33,6 +88,9 @@ operations = ["kmac.variable_output_and_verify"]
 public_length = "The caller selects KMAC output length and supplies an expected buffer of that public length."
 secret_contents = "The computed KMAC output and expected bytes are traversed fully for each public-length chunk."
 tests = "KMAC NIST/Wycheproof/differential tests plus kmac256_valid_vs_invalid_tag DudeCT."
+evidence_symbols = ["ct_entry_kmac256_verify"]
+evidenced_call_count = 1
+limited_call_count = 0
 
 [[public_len_comparison]]
 id = "rsa.public_modulus_and_profile_shapes"
@@ -42,6 +100,16 @@ operations = ["rsa.private_key_import_export_and_generation", "rsa.private_sign_
 public_length = "Widths derive from the public modulus, digest algorithm, DER/padding profile, or caller-visible encoded length."
 secret_contents = "Private representatives, decoded plaintext/hash fields, or validation intermediates are compared without content-dependent exits after public shape checks."
 tests = "RSA official/Wycheproof/differential/private-operation tests and RSA CT harness/DudeCT cases."
+evidence_symbols = [
+  "ct_entry_rsa_pkcs1v15_sign_fixed_blinding",
+  "ct_entry_rsa_pss_sign_fixed_blinding",
+  "ct_entry_rsa_oaep_decrypt_fixed_blinding",
+  "ct_entry_rsa_pkcs1v15_decrypt_fixed_blinding",
+  "ct_entry_rsa_private_key_pkcs8_roundtrip",
+]
+evidenced_call_count = 7
+limited_call_count = 5
+limitation = "The two Miller-Rabin key-generation comparisons and three public verification comparisons are not reachable from the retained release equality roots. Their lengths remain public and their source traversal is audited, but T3.3 does not convert that source review into linked-binary evidence."
 
 [[public_len_comparison]]
 id = "mlkem.parameter_set_shapes"
@@ -51,6 +119,13 @@ operations = ["kem.mlkem512", "kem.mlkem768", "kem.mlkem1024"]
 public_length = "Encoded key/ciphertext widths are fixed by the public ML-KEM parameter set and validated before comparison."
 secret_contents = "Decapsulation implicit-rejection ciphertext/key material is traversed fully at that public parameter-set width."
 tests = "ML-KEM ACVP, differential, property, operation, CT harness, and DudeCT cases for all parameter sets."
+evidence_symbols = [
+  "ct_entry_mlkem512_decapsulate",
+  "ct_entry_mlkem768_decapsulate",
+  "ct_entry_mlkem1024_decapsulate",
+]
+evidenced_call_count = 1
+limited_call_count = 0
 
 [[public_len_comparison]]
 id = "argon2.caller_selected_output"
@@ -60,6 +135,9 @@ operations = ["password.argon2i", "password.argon2d_and_argon2id"]
 public_length = "Primitive verification derives exactly the caller-supplied expected output length after public bounds checks."
 secret_contents = "The freshly derived password verifier and expected bytes are traversed fully before the temporary is cleared."
 tests = "Argon2 vectors/differentials/parallel tests and variant CT harness/DudeCT cases."
+evidence_symbols = ["ct_entry_argon2i_verify", "ct_entry_argon2d_verify", "ct_entry_argon2id_verify"]
+evidenced_call_count = 1
+limited_call_count = 0
 
 [[public_len_comparison]]
 id = "scrypt.caller_selected_output"
@@ -69,6 +147,9 @@ operations = ["password.scrypt"]
 public_length = "Primitive verification derives exactly the caller-supplied expected output length after public minimum-length checks."
 secret_contents = "The freshly derived password verifier and expected bytes are traversed fully before the temporary is cleared."
 tests = "scrypt vectors/differentials and verification CT harness/DudeCT cases."
+evidence_symbols = ["ct_entry_scrypt_verify"]
+evidenced_call_count = 1
+limited_call_count = 0
 
 [status]
 ct_claimed = "all required evidence has passed for the exact primitive/configuration pair"
@@ -113,9 +194,13 @@ kind = "staticlib"
 status = "covered"
 symbols = [
   "ct_entry_owner_eq_16",
+  "ct_entry_owner_eq_28",
   "ct_entry_owner_eq_32",
   "ct_entry_owner_eq_48",
   "ct_entry_owner_eq_64",
+  "ct_entry_owner_eq_1632",
+  "ct_entry_owner_eq_2400",
+  "ct_entry_owner_eq_3168",
   "ct_entry_secret_bytes32_debug_masked",
   "ct_entry_hmac_sha256_verify",
   "ct_entry_hmac_sha384_verify",
@@ -3110,6 +3195,7 @@ tier = "A"
 claim = "ct-intended"
 features = ["always"]
 variants = ["Owner16", "Owner32", "Owner48", "Owner64"]
+release_owner_widths = [16, 28, 32, 48, 64, 1632, 2400, 3168]
 entrypoints = [
   "Aes128GcmKey::eq",
   "X25519SecretKey::eq",
@@ -3125,7 +3211,16 @@ required = ["tier_a"]
 notes = "Public callers select a semantic owner, never a raw secret length. Source structure and black_box are not machine-code proofs; T3.3 owns exact release-binary evidence. Returning bool remains an explicit T3.4 limitation."
 [primitive.harness]
 status = "covered"
-symbols = ["ct_entry_owner_eq_16", "ct_entry_owner_eq_32", "ct_entry_owner_eq_48", "ct_entry_owner_eq_64"]
+symbols = [
+  "ct_entry_owner_eq_16",
+  "ct_entry_owner_eq_28",
+  "ct_entry_owner_eq_32",
+  "ct_entry_owner_eq_48",
+  "ct_entry_owner_eq_64",
+  "ct_entry_owner_eq_1632",
+  "ct_entry_owner_eq_2400",
+  "ct_entry_owner_eq_3168",
+]
 
 [[primitive]]
 id = "secret_wrappers.exposure_and_display"

docs/constant-time.md

@@ -146,9 +146,12 @@ evidence set includes:
 
 - Stable harness entrypoints.
 - Build and host provenance.
-- LLVM IR, assembly, object, and symbol artifacts.
+- LLVM IR, assembly, pre-link objects, and symbol artifacts.
+- A fat-LTO final linked equality evidence executable, its exact linker
+  command and linker identity, and post-link disassembly, symbols, and size.
 - Automated checks for suspicious generated-code patterns.
-- Empirical timing tests on native executable targets.
+- Empirical timing tests on native executable targets, bound to the hashed
+  timing executable, disassembly, symbol map, and linker command.
 - ML-KEM DudeCT cases for key generation secret noise, encapsulation coins,
   decapsulation secret keys, implicit rejection, NTT, inverse NTT,
   product-domain conversion, basemul/dot products, and compress/decompress
@@ -157,6 +160,20 @@ evidence set includes:
   paths.
 - Miri and unsafe-code validation where the CT path uses unsafe Rust.
 
+The linked equality executable retains production owner comparisons at the
+distinct 16-, 28-, 32-, 48-, 64-, 1632-, 2400-, and 3168-byte owner widths.
+The required owner timing cases remain the manifest-declared 16-, 32-, 48-,
+and 64-byte cases. Public-length internal comparisons are mapped in `ct.toml`
+to retained production entrypoints or to an explicit limitation; an uncovered
+call is not silently treated as binary evidence.
+
+This executable is an unpublished evidence surface. It proves only its exact
+source, toolchain, backend, target, target features, feature set, profile, and
+linker configuration. It is not the crate's public API, it is not a sealed
+decision type, and it does not generalize to arbitrary downstream binaries.
+Equality still returns `bool`; that declassification limitation remains until
+T3.4.
+
 Assembly triage is grouped by primitive, reachable symbol, finding kind, and
 artifact. Register-indexed memory is presented first, then conditional control
 flow, then indirect calls. `needs-binsec` means operand provenance remains
@@ -168,7 +185,8 @@ date. Source or disassembly movement invalidates it.
 BINSEC is required on the GNU Linux targets supported by the workflow. Every
 manifest-required kernel must report `secure`. Other target reports record
 BINSEC as `not_applicable` with the target policy reason; that status is not
-binary proof.
+binary proof. Each formal result is bound to its hashed proof driver,
+disassembly, configuration, solver log, candidate identity, and toolchain.
 
 Statistical timing checks must be described precisely:
 

docs/release.md

@@ -167,7 +167,7 @@ receive anything, the workflow:
 2. Revalidates configuration, the unified Cargo graph, dependency policy,
    audit results, SemVer, and successful CI for the exact commit.
 3. Requires complete Weekly CT/RSA and RISC-V native/CT evidence from that
-   commit or a mechanically proven release-tooling-only ancestor.
+   exact commit and crate version.
 4. Builds the `.crate` once, reproduces the source archive from the tag, and
    rejects dirty, private, local-only, or mismatched package contents.
 5. Captures repository controls and writes provenance attestations, an identity
@@ -176,11 +176,10 @@ receive anything, the workflow:
    crates.io token through OIDC, publishes the same crate, then downloads it
    from crates.io and verifies its SHA-256.
 
-A release-tooling-only repair may reuse the newest successful ancestor with
-paired Weekly and RISC-V evidence. The checker permits only changelog,
-release/CT tooling, root-package version, and normalized local CT lockfile
-version changes. Runtime, dependency, feature, build, or test changes invalidate
-that exception.
+Any change after the evidence run—including a version-only or release-tooling
+change—creates a new release candidate and requires fresh paired Weekly and
+RISC-V evidence. Ancestor binaries are never promoted into an exact-commit
+constant-time claim.
 
 ## Recovery
 

justfile

@@ -112,7 +112,7 @@ check-zeroize-evidence:
 
 check-unify:
     cargo rail config validate --strict
-    cargo rail config sync --check
+    cargo rail config migrate --check
     cargo rail unify --check --explain
 
 ci-check: