Stage-3 REQ-6: review surface — semantic forks + towers (the F-F tripwire) (#348) (#89)

* Stage-3 REQ-6: review surface — semantic forks and definition towers (#348)

Add the additive "semantic forks and definition towers" section to
`forge audit` / `forge review` (`.design/stage3-bv-reconstruction.md`
REQ-6 / AC-7): bv-shadow density per module + every burned lemma's
definition-tower depth, carrying the post-ship F-F density tripwire.

- new forge/src/forks.rs: SemanticForks { bv_density (per contract-bearing
  item, denominated by ens clauses), burned_lemma_towers (via the meaning.rs
  spec-fn tower rooted at the lemma's req∪ens), tripwire }. The F-F tripwire
  fires when project-wide bv-shadow density reaches 500‰ (majority of the
  postcondition surface) — a named, informational warning that gates nothing.
- meaning.rs: add tower_metrics (depth-only, no src) + factor the shared
  spec-fn graph helpers; build_tower behavior unchanged.
- additive Option<SemanticForks> on AuditManifest + ReviewArtifact
  (#[serde(skip_serializing_if = Option::is_none)] → v1 goldens byte-identical);
  cli render_audit/render_review append the human section.
- fixtures: bv_density_normal.th (250‰, no trip) + bv_density_spike.th
  (666‰, trips); 6 forks unit tests + 3 bv_lowering conformance tests.

A pure read-only projection: no verdict changes, no exit-code changes; the
@bv per-item overlay (program_has_bv_tag) and REQ-3/4/5 locks stay green.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* chore(doc-drift): re-pin 6 docs for the #348 semantic-forks section ripple

REQ-6 adds forge/src/forks.rs + the additive semantic_forks section across
audit.rs/cli.rs/review.rs/meaning.rs/main.rs, drifting the docs governing
them. Content-sha refresh (squash-stable). Governed REQs unchanged.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: maxine-at-forecast

.design/basis/09-option-result.md

@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 0be0416df846c149e4d5b6feaf22596d7ab912906bd992184cb63eec8d0e9723 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 0e9ce0aee57c30c48e74a37c8c492afafe9545ade899c965e842b98bbf72b12e (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: thermite-syntax/src/ast.rs
 governs: thermite-syntax/src/parser.rs
 governs: thermite-spec/src/validator.rs

.design/basis/11-ergonomics.md

@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 0be0416df846c149e4d5b6feaf22596d7ab912906bd992184cb63eec8d0e9723 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 0e9ce0aee57c30c48e74a37c8c492afafe9545ade899c965e842b98bbf72b12e (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: thermite-syntax/src/parser.rs
 governs: thermite-syntax/src/ast.rs
 governs: thermite-lower/src/lower.rs

.design/forge/audit-manifest.md

@@ -3,7 +3,7 @@
 tier: 3-component
 status: draft
 audited-sha: 1cc9d97c6c5d7eab6109561834db77f2ef4b57ab (re-pinned 2026-06-16: forge workflow status rows now render from canonical registry IDs; behavior unchanged; RFC #17)  (prior: 488103d4382815b85141d17bc01b60917ba744e7 (#274 — lean_fragment membership report; REQ-7..10 SHIPPED, audit.rs verified-current))
-audited-content-sha256: adf1e73cdae4923311fc2bdac210e295850a490f0edacdc1055a810195dc2458
+audited-content-sha256: 11d046491b2627236d2a81608698435e965743ef0c746746e13ec1e6c2cba0af
 governs: forge/src/audit.rs
 thesis-refs:
   - thermite-design.md §6

.design/forge/cli.md

@@ -4,7 +4,7 @@
 tier: 3-component
 status: shipped
 audited-sha: 5ae0816c042debb01c70eb9b89c775837f0c0f24 (content-sha256 re-pinned 2026-06-21 for stage-2 REQ-8 / AC-8 (#330), faithfulness + two-phase TV + the trust flip: the change to this doc's governed file (cli.rs) is the additive `forge strat-faithful-tv [--generated N] [--seed <u64>] [--json]` subcommand (`Command::StratFaithfulTv` → `run_strat_faithful_tv`, the two-phase TV sweep reporting the phase split + the gated trust profile); every other subcommand + flag parse is unchanged. The legacy commit pin stays at the 5ae0816c stable-main ancestor; only the active content-sha256 digest moves. prior: 2026-06-20 stage-2 REQ-4 / AC-4 (#326) `forge strat-tv` + `ForgeError::StratDifferential`; 2026-06-18 umbrella REQ-2c / AC-4 rotating-seed `--seed` flag on `forge tv`; §6 metrics dashboard `--metrics` value)
-audited-content-sha256: fefedbf24bbda305680c8fb5947123fd1190ce32279fca0fc21b9f6bb8c86b42
+audited-content-sha256: fdf790121bf8dc4fa50c43b0b476a3a390d114cac27709240a111b11f126dcab
 governs: forge/src/cli.rs
 thesis-refs:
   - thermite-design.md §5

.design/forge/spec-review.md

@@ -3,7 +3,7 @@
 tier: 3-component
 status: draft
 audited-sha: 8b4d2580b472d04fca2b14de5b6be52533a2d258 (re-pinned 2026-06-17 for stage-1 increment 3, REQ-9 lemma library: the only change to this doc's governed file (review.rs) is the additive REQ-9 burned_lemmas partition + BurnedLemma projection (a certified lemma surfaces like any certified item); the v1 intent-reviewable / battery-failing partitions are unchanged (REQ-S1-9). prior: 92396428567edc6940a9e2845217f5ff4c2ea3c6)
-audited-content-sha256: 835a51237e78d06896155aff194ef58091b658ed34a04ea32f7b9e13f4de1c3c
+audited-content-sha256: dadde2fd2a0e6b248e4d843a120be92e1e69537780b0c531bb2aab2864c1f213
 governs: forge/src/review.rs
 thesis-refs:
   - thermite-design.md §7

.design/scaffold/workspace.md

@@ -3,7 +3,7 @@
 tier: 3-component
 status: draft
 audited-sha: 5ae0816c042debb01c70eb9b89c775837f0c0f24 (content-sha256 re-pinned 2026-06-20 for stage-2 REQ-4 / AC-4 (#326), the classifier ops half: the changes to this doc's governed lib roots are additive — `pub mod classifier;` + the classifier re-exports in thermite-spec/src/lib.rs (the new Rust admission classifier), and `mod strat_tv;` in forge/src/main.rs (the differential battery module); the workspace/crate structure is otherwise unchanged. The legacy commit pin stays at the 5ae0816c stable-main ancestor; only the active content-sha256 digest moves. prior: 2026-06-17 umbrella REQ-7 / AC-12 §6 metrics dashboard `mod metrics;`; stage-1 REQ-10/AC-14 G1 gate seven-verdict test module)
-audited-content-sha256: 8028435bfe4a6bedcdd68c639756f7097944430a118435134982131b19527154
+audited-content-sha256: bb5fae7f5c33ec049c7e9cd730c1038c02e29e9fce73a6a1a93f42c5e8c7164f
 governs:
   - Cargo.toml (virtual workspace manifest)
   - rust-toolchain.toml

conformance/forge/bv_density_normal.th

@@ -0,0 +1,40 @@
+// bv_density_normal.th — a project whose bv-shadow density is BELOW the F-F retreat
+// threshold (`.design/stage3-bv-reconstruction.md` REQ-6 / AC-7, the "normal" case).
+//
+// `forge audit` / `forge review` auto-route this through the bit-vector engine (it carries
+// a `@bv` tag), so the "semantic forks and definition towers" section reports the
+// per-module bv-shadow density and the project-wide F-F tripwire. Here ONE @bv-tagged ens
+// clause sits among FOUR contract-bearing ens clauses: a project density of 1/4 = 250‰,
+// well within the 500‰ retreat threshold — the tripwire does NOT fire (the healthy
+// baseline: a small, deliberate machine-semantics fork in an otherwise-unbounded codebase).
+//
+// Per-module known counts (a pure parse-level projection):
+//   * wrap_add  — 1/1 ens machine-semantics (1000‰)
+//   * plain_add — 0/1 (0‰)
+//   * plain_inc — 0/1 (0‰)
+//   * plain_id  — 0/1 (0‰)
+//   project     — 1/4 ens machine-semantics (250‰) → WITHIN the 500‰ threshold.
+
+fn wrap_add(a: u64, b: u64) -> u64
+    req true
+    ens@bv64 a + b == b + a
+    fx pure
+{ a + b }
+
+fn plain_add(a: u64, b: u64) -> u64
+    req a < 100 && b < 100
+    ens result >= a
+    fx pure
+{ a + b }
+
+fn plain_inc(x: u32) -> u32
+    req x < 100
+    ens result == x + 1
+    fx pure
+{ x + 1 }
+
+fn plain_id(x: u32) -> u32
+    req true
+    ens result == x
+    fx pure
+{ x }

conformance/forge/bv_density_spike.th

@@ -0,0 +1,33 @@
+// bv_density_spike.th — a SYNTHETIC density spike that trips the named F-F warning
+// (`.design/stage3-bv-reconstruction.md` REQ-6 / AC-7, the "spike" case).
+//
+// The post-ship F-F tripwire: when machine-semantics forks become the MAJORITY of the
+// contract-bearing postcondition surface, the program has drifted far enough toward the
+// fork that the @bv retreat ladder (full → nowrap-only → lemma-only → drop) should be
+// weighed. Here TWO @bv-tagged ens clauses sit among THREE contract-bearing ens clauses:
+// a project density of 2/3 = 666‰, at or above the 500‰ retreat threshold — the F-F
+// tripwire FIRES (a loud, informational warning; it gates nothing, changes no verdict).
+//
+// Per-module known counts (a pure parse-level projection):
+//   * wrap_comm  — 1/1 ens machine-semantics (1000‰)
+//   * wrap_xor   — 1/1 ens machine-semantics (1000‰)
+//   * plain_add  — 0/1 (0‰)
+//   project      — 2/3 ens machine-semantics (666‰) → REACHES the 500‰ threshold (TRIP).
+
+fn wrap_comm(a: u64, b: u64) -> u64
+    req true
+    ens@bv64 a + b == b + a
+    fx pure
+{ a + b }
+
+fn wrap_xor(a: u64, b: u64) -> u64
+    req true
+    ens@bv64 a ^ b ^ b == a
+    fx pure
+{ a ^ b }
+
+fn plain_add(a: u64, b: u64) -> u64
+    req a < 100 && b < 100
+    ens result >= a
+    fx pure
+{ a + b }

forge/src/audit.rs

@@ -97,6 +97,17 @@ pub struct AuditManifest {
     /// discipline). The section gates nothing — informational, like `lean_fragment`.
     #[serde(default, skip_serializing_if = "Vec::is_empty")]
     pub bv_shadows: Vec<BvShadowRow>,
+    /// The "semantic forks and definition towers" section
+    /// (`.design/stage3-bv-reconstruction.md` REQ-6 / AC-7): the AGGREGATE legibility
+    /// surface over the per-clause `bv_shadows` above + the burned-lemma towers — bv-shadow
+    /// density per module, every burned lemma's definition-tower depth, and the post-ship
+    /// **F-F density tripwire**. A pure projection ([`crate::forks::SemanticForks::build`]);
+    /// `None` (and omitted) for a tag-free, lemma-free project, so the v1 corpus serializes
+    /// BYTE-IDENTICALLY (the additive `bv_shadows`/`lean_fragment` discipline;
+    /// `manifest_version` stays `"v1"`). The section gates nothing — informational, like
+    /// `bv_shadows`.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub semantic_forks: Option<crate::forks::SemanticForks>,
 }
 
 /// One `@bv`-tagged clause's shadow-flag row in the audit manifest
@@ -605,13 +616,18 @@ impl AuditManifest {
         // Lock 1 (stage-3 REQ-3 / AC-4): the project's `@bv` shadow flags, one row per
         // tagged clause — a pure projection of the certs' obligations.
         let bv_shadows = BvShadowRow::from_certificates(certs);
+        // REQ-6 / AC-7: the aggregate "semantic forks and definition towers" section — the
+        // bv-shadow density per module, the burned-lemma tower depths, and the F-F density
+        // tripwire. `None` (omitted) for a tag-free, lemma-free project (the v1 corpus).
+        let semantic_forks = crate::forks::SemanticForks::build(certs, program);
         AuditManifest {
             manifest_version: MANIFEST_VERSION.to_string(),
             functions,
             project_assurance,
             tcb,
             lean_fragment,
             bv_shadows,
+            semantic_forks,
         }
     }
 }

forge/src/cli.rs

@@ -2761,6 +2761,12 @@ fn render_review(artifact: &ReviewArtifact) -> String {
             ));
         }
     }
+    // REQ-6 / AC-7: the aggregate "semantic forks and definition towers" section — the
+    // bv-shadow density per module + burned-lemma tower depths + the F-F density tripwire.
+    if let Some(forks) = &artifact.semantic_forks {
+        out.push('\n');
+        out.push_str(&forks.render());
+    }
     out
 }
 
@@ -3007,6 +3013,11 @@ fn render_audit(manifest: &AuditManifest) -> String {
             ));
         }
     }
+    // REQ-6 / AC-7: the aggregate "semantic forks and definition towers" section — the
+    // bv-shadow density per module + burned-lemma tower depths + the F-F density tripwire.
+    if let Some(forks) = &manifest.semantic_forks {
+        out.push_str(&forks.render());
+    }
     out
 }