Module architecture and verification

Module Architecture and Verification Model

Overview

Use this model to enforce strict scope boundaries for specialized authors (by node role), reduce manual traceability work, and support highly deterministic verification.

ValidKeep maps architectural concepts directly to atomic files and physical code artifacts. This mapping strictly separates:

• Obligations (Demand / Problem Space)
• Capabilities (Supply / Interface)
• Implementations (Design / White-Box Logic / Code)
• Execution Evidence (Verification / Test Plans / Test Scripts)

During authoring, certain monolithic documents (like Requirement or Functional Specifications) are generated as "virtual views" dynamically rendered from the underlying atomic files, while testing assets exist purely as native module components.

1. Contract Algebra (Problem Space)

The problem space establishes the absolute demand placed upon the module.

• Module index (x): Module position in the hierarchy (for example, 0.2 in module M_{0.2}).
• Child index (i): Index of an immediate child module (for example, 0.2.1).
• Directive (D_x): Parent-defined objectives and constraints delegated to this module. Stored as *.dx.md.
• Requirements (R_x): Module-local domain constraints injected by stakeholders directly into this specific module. Stored as *.rx.md.
• Rule (r): A specific, scalar obligation where r \in O_x. In the files, each rule is documented under its own markdown subheading, allowing the AST parser to identify it as a discrete traceability fragment.

Root dx bootstrap and the mandate / requirement split

The very first top-level module root .dx.md in a workspace is created ex nihilo*: it is manually placed at the repository boundary, not delegated from any parent module. That root dx has no parent and no upstream D_x; it is the DAG origin for obligation traceability. It should stay deliberately thin, little more than the essential mandate needed to start the DAG (scope, boundary intent, and delegation posture for the tree below). Few if any detailed stakeholder rules belong in that file.

For every module, D_x conveys the mandate (what the parent, or, at the root, the workspace author, charges this module to accomplish). R_x carries stakeholder requirements authored at the level where they apply. At the root module, the rx requirements author (and human reviewers) populate R_x with the product's substantive obligations; the root dx does not duplicate that work. Deeper in the tree, each module's .rx.md captures user and domain requirements at the appropriate depth, while each child still inherits its charge and parent specific requirements through its own .dx.md.

There is no dedicated dx author role. For nested modules, delegated child directives (D_i, materialized as child *.dx.md files) are authored from the parent side by the lx logic author as part of L_{parent} decomposition and stubout, not as a separate role. Only the repository's first root dx is placed "by hand", i.e. from an external source; all subsequent dx files are downstream artifacts of parent design.

Obligation Equation (O_x)

O_x is the complete obligation set for the module.

Interpretation: the module must satisfy every inherited directive and every locally defined requirement. Because this set contains all contract rules, it acts as the primary driver for defining the module's interface and mandatory OQ test coverage. Functional risk (business-process impact on obligations) is recorded per obligation fragment on dx and rx via sidecar fragment_attributes (functional_risk, optional functional_risk_note, functional_risk_scope); verify requires it when enforce_risk_based_testing is enabled and the fragment matches the profile's obligation trace source selectors.

2. Solution Algebra (Implementation Space)

To satisfy its obligations, the module defines a Black-Box interface and a White-Box physical implementation.

• Borrowed tools (B_x): Parent-authorized external services, databases, or resources allocated to this module. Stored as *.bx.md.
• Capability (C_x): The black-box public interface promised by the module. Stored as *.cx.md.
• Capability element (c): A scalar interface endpoint or promised feature where c \in C_x.
• Local logic (L_x): Internal white-box algorithmic design and architecture. Stored as *.lx.md.
• Delegated child directives (\bigcup_i D_i): Objectives delegated to children when decomposition is required.
• Physical Code (CODE): The actual application source code files written to implement L_x.

Capability Equation (C_x)

The realization of a module's capability occurs in a two-way vector loop between parent and child.

1. The Delegation Vector (Top-Down Design):

When internal logic (L_x) becomes too complex, it delegates by spawning children. It establishes the "ironclad stipulations" by authoring child directives (D_i) and handing down borrowed tools (B_i).

2. The Subsumption Guarantee (Child Resolution):

The child resolves its local obligations (O_i = D_i \cup R_i) and forms its public-facing interface (C_i = O_i). Because C_i contains D_i, the interface mathematically guarantees the parent's mandate is met (\therefore D_i \subseteq C_i).

3. The Integration Vector (Bottom-Up Execution):

At runtime, the parent logic cannot execute a demand (D_i); it must consume a definitive interface. Therefore, the true Capability Equation evaluates L_x parameterized by external tools and the established capabilities of its children:

Mathematically, local logic (L_x) acts as an operator parameterized by borrowed tools and child capabilities to produce the boundary capability.

Balance Law & Implementation Risk

Demand and supply must match exactly. A rule r is satisfied by a capability c, which is designed in logic l, and physically realized in CODE. Therefore, the upstream trace flows: CODE \to L_x \to C_x \to O_x.

Note on Risk: While C_x satisfies the functional contract (O_x), the physical realization of that contract (L_x) inevitably introduces implementation-induced risk (e.g., race conditions, bottlenecks, memory overhead). Therefore, while OQ verifies the C_x balance law, PQ explicitly monitors the L_x implementation risk.

3. Demand Verification: Operational Qualification (OQ)

In ValidKeep, Qualification (IQ, OQ, PQ) refers to types of testing strategies applied to specific mathematical nodes, rather than sequential lifecycle phases.

Operational Qualification (OQ) is the process of verifying the Demand (O_x). OQ tests are static, pre-computed validations executed in a controlled environment. OQ testing strictly treats the module as a Black Box, interacting only with the exposed Capability (C_x) using an active test driver script to prove that a specific Obligation (O_x) has been met.

• OQ Test Strategy (OQTS): The black-box laboratory plan. Stored as *.oqts.md. It designs shared test functions, outlines mock environments for borrowed tools (B_x), and specifies testing orchestration against C_x.
• OQ Test Definition (OQTEST): A discrete, isolated file representing the verification of a single rule (r \in O_x). Stored as *.oqtest.md. Every individual rule fragment in D_x and R_x MUST trace directly to the root of its own OQTEST file.
• OQ Test Infrastructure Code (OQTSCODE): The physical code files containing shared test harnesses and database mockers designed by the OQTS.
• OQ Executable Code (OQTESTCODE): The physical, automated active test driver scripts that inject inputs into C_x to verify the expected results defined in the OQTEST.

The OQ Verification Loop

Every demand rule r \in O_x \to OQTEST_r. The OQTEST_r translates into an active OQTESTCODE_r script, leveraging OQTSCODE to poke the boundary of C_x.

4. Supply Verification: Performance Qualification (PQ) & Observability

Performance Qualification (PQ) is the process of verifying Implementation Resilience (L_x). While OQ proves the module behaves correctly under controlled test data, PQ proves that the internal algorithms, mitigations, and constraints designed in L_x survive under unpredictable real-world payloads.

Because you cannot understand chaotic system failure by only looking at the black-box front door, PQ relies on White-Box observability. It uses internal telemetry probes explicitly designed into the module logic and evaluated passively by the Hub.

• PQ Test Strategy (PQTS): The white-box laboratory plan. Stored as *.pqts.md. It designs the load-generation profiles and the ValidKeep SDK telemetry routing pipeline required to observe L_x.
• PQ Test Definition (PQTEST): An isolated file defining the expected invariants and telemetry thresholds for a single logic step or identified risk (l \in L_x). Stored as *.pqtest.md.
• PQ Evaluation Code (PQTESTCODE): The script that queries the ValidKeep Hub for live ValidKeep SDK telemetry emitted by CODE, asserting it against the invariants defined in the PQTEST.

Embedded Telemetry & The PQ Verification Loop

1. 1. Design Mandate & Risk (L_x): During the white-box design phase, the architect identifies implementation-induced risks (e.g., a mutex lock) and dictates the placement of telemetry probes to monitor them.
2. 2. Physical Probes (CODE): The developer embeds physical ValidKeep SDK probes in CODE at the exact locations designated by L_x.
3. 3. Execution & Evaluation: The module is subjected to load (driven by PQTS load-profiles). The CODE probes emit state telemetry tagged with the AST path of the L_x fragment. The Hub catches this emission.
4. 4. The Trace Validation: The PQTESTCODE script queries the Hub for telemetry tied to that exact L_x fragment. It evaluates the data (CODE \to L_x \to PQTEST) to ensure the internal logic survived the load.

5. Submodule Extraction (Resolving the Complexity Problem)

If internal white-box logic (L_x) becomes too complex or requires its own deep state management, it must be extracted out of the current module:

1. 1. Re-scoping: The complex logic is removed from L_x and redefined as a delegated child directive (D_i) alongside allocated tools (B_i).
2. 2. New Boundary: This establishes a new submodule (i) with its own interface boundary (C_i) and obligation set (O_i).
3. 3. Local Assurances: The new submodule becomes fully responsible for authoring its own OQTEST suite, PQTEST suite, and internal CODE probes.

1. 4. Integration loop: Parent L_x authors D_i and B_i, then reads child C_i targets recorded in [lx_children_cx.vk.yaml](../../validkeep-core/.validkeep/lx_children_cx.vk.yaml) when trace_link_author: upstream on the lx → cx children edge. External workflows may notify the parent when a child C_i stabilizes; ValidKeep verify only enforces the sidecar DAG and right_join back-traces (downstream child cx and code must justify existence against parent lx when linked).

All lx outbound trace edges (lx → dx, lx → bx, lx → cx, lx → code, lx → pqtest) use right_join in the assurance profile: parent lx has discretion; delegated or realized downstream fragments must justify existence.

6. Role isolation and blind-scoped authoring

Because architectural variables are segregated by file, each specialized author receives a rigidly constrained context window. Each role only sees the information required for its task, supporting double-blind verification and scope isolation.

Compatible authoring workflows may use optional context assembly rules (for example peer:cx, parent:lx). ValidKeep verify does not require them. The assurance profile may set trace_link_author: upstream on a scope: children trace row (today: lx → cx only); tools that honor the flag may treat targets listed in lx_children_cx.vk.yaml as read-only integration inputs for the parent lx author , not a DAG reversal. Delegation edges (lx → dx, lx → bx) do not set this flag; child dx and bx are authored by child-module roles. Multi-kind fragment scopes can be profile-driven as a YAML list (for example obligations spanning dx and rx). Peer resolves co-located files in the module directory; parent applies where child genesis roles read parent lx. Tree-wide reads apply where the profile allows repository-wide obligation alignment.

• rx , Requirements author
• Writes: Local Requirements (R_x) only.
• Reads (mandatory): Peer directive (D_x) , the mandate delegated to this module.
• May read (optional, requirements fence): Any D or R in the repository, read-only. Use mandates and existing requirements across parent, child, and distant modules to align obligations and decide where each rule belongs. Stakeholder rules belong in R at the lowest module that can accommodate them; writes only local R_x. When another module is the better home, request that module's requirements author (for example via a coordination ledger or workflow notification) to author the rule there instead of mis-placing it here. Never crosses into B_x, L_x, C_x, tests, or code.
• Does not read: Borrowed tools (B_x) , delegated by the parent lx author and consumed by the child lx author. Also blind to parent logic (L_{parent}) and any white-box, interface, or verification artifacts.
• cx , Interface author
• Writes: Capability (C_x).
• Reads: Obligations (D_x, R_x) only. Blind to implementation, borrowed tools, tests, and code.
• lx , Logic author
• Writes: Local Logic (L_x), Delegated Child Directives (D_i / child *.dx.md), Delegated Tools (B_i).
• Reads: Capability (C_x), Borrowed Tools (B_x), and child C_i listed in lx_children_cx.vk.yaml when trace_link_author: upstream.
• Context logic: Authors D_i to demand what the child must do, links child C_i in lx_children_cx, then reads those interfaces to write parent integration logic. Child dx/bx are authored by child-module roles , parent lx does not treat all immediate child dx/bx as mandatory read scope.
• Note: Determines where embedded PQ probes are required.
• oqts , OQ Lab Builder
• Writes: OQ Test Strategy (OQTS) and $OQTSCODE. Defines mock setups and black-box fixtures.
• Reads: Capability (C_x) and Borrowed Tools (B_x). Blind to L_x to preserve the purity of the black-box environment. Obligation context reaches OQ via oqtest (dx/rx → oqtest); OQTS traces only from cx and bx.
• pqts , PQ Lab Builder
• Writes: PQ Test Strategy (PQTS) and $PQTSCODE. Defines load profiles and SDK telemetry pipelines.
• Reads: Local Logic (L_x).
• oqtest , OQ trace planner & per-fragment authoring
• Writes: dx/rx_children_oqtest.vk.yaml and discrete OQTEST files per rule (r \in O_x).
• Reads: A specific rule fragment, Capability (C_x), and OQTS fixtures. Strictly blind to Borrowed Tools (B_x) and Logic (L_x) to prevent writing implementation-coupled tests.
• pqtest , PQ trace planner & per-fragment authoring
• Writes: lx_children_pqtest.vk.yaml and discrete PQTEST files per logic risk (l \in L_x).
• Reads: A specific logic fragment (L_x) and PQTS. They read the architectural design to understand the documented risks and the expected schemas of the ValidKeep SDK probes.
• code , trace planner (review_fragments, lx_tree_code)
• Writes: Tracecar lx_tree_code.vk.yaml only in planner mode.
• Reads: Peer L_x. Per-file single mode authors application source from one assigned code file.
• oqtscode , OQ harness author (planner + per-file single)
• Planner: oqts_tree_oqtscode.vk.yaml. Single: shared OQ harness/fixture code per assigned file.
• pqtscode , PQ harness author (planner + per-file single)
• Planner: pqts_tree_pqtscode.vk.yaml. Single: shared PQ load/telemetry infrastructure per assigned file.
• oqtestcode , runner author (planner + per-file single)
• Planner: oqtest_peer_oqtestcode.vk.yaml. Single: executable drivers per assigned runner file; reads paired OQTEST only (Execution Steps embed harness calls).
• pqtestcode , PQ run author (planner + per-file single)
• Planner: pqtest_peer_pqtestcode.vk.yaml. Single: Hub-orchestrated PQ run scripts per assigned file , open recording, retrieve probe results on closure, and evaluate pass/fail against paired PQTEST criteria; reads paired PQTEST and PQTS.

Tracecars and scope (file-level verify)

Child-module delegation (lx → dx / lx → bx): downstream child genesis roles edit lx_children_{dx,bx} in the parent shadow directory (back-link from child mandate to parent logic).

Tree sidecars are downstream-maintained pairing ledgers: one sidecar per module may contain many source: rows (one per upstream spec file). Verify does not require every upstream markdown file to list every downstream artifact in tree scope.

Formal :tree spatial scope: from the module anchor directory through the module tree, excluding nested child-module subtrees (same rule for lx→code, oqts→oqtscode, pqts→pqtscode).

7. Rendered Document Views

Traditional software lifecycle documents are generated dynamically by the ValidKeep compiler by joining atomic files into unified views. Testing assets are preserved and displayed natively.

• Requirement Specification (RS): Fleshes out the Problem Space.

• Functional Specification (FS): Defines the Black-Box Interface.

• Design Specification (DS): Details White-Box Logic and Submodule extraction.

• Test Documentation: The native strategies (OQTS, PQTS) and the collections of discrete cases (\bigcup OQTEST_r and \bigcup PQTEST_l) are displayed as standalone native assets rather than compiled into a monolithic view.
• Verification Report (VR): Assembled dynamically from the Hub, demonstrating that all OQTEST active drivers passed and all PQTEST runs completed with probe telemetry that satisfied their criteria under load.