Verification Results

Layer-by-Layer Results

Detailed breakdown of the three verification layers (Syntactic, Structural, Behavioral), failure codes, transition criteria, and implementation metrics. All results reflect Phase I at v0.2.0-implementation.

Summary

✅

Phase I Complete: 118/118 tests passing · flake8 = 0 errors · all 3 invariant layers implemented and verified.

Layer I_s — Syntactic Invariants (S1–S6)

Formal validity of the transformed program representation. Verified via LibCST parser and signature comparison.

Code	Condition	Check	Tests	Status
S1	P₁ parses as valid Module	`cst.parse_module`	2	PASS
S2	Exactly one top-level FunctionDef	node count	3	PASS
S3	Function name unchanged	name compare	2	PASS
S4	Signature unchanged	params compare	3	PASS
S5	No new decorators	decorator set	3	PASS
S6	No new imports inside function	Import scan	3	PASS
Composite verdict			5	PASS

Layer I_t — Structural Invariants (T1–T5)

Relational integrity of the transformed program. Verified via dependency graph analysis and scope resolution.

Code	Condition	Check	Tests	Status
T1	Every used Name has a binding	scope analysis	5	PASS
T2	No invalid dependency cycles	DFS cycle detection	3	PASS
T3	No orphan variables	liveness diff	3	PASS
T4	No new global statements	AST scan	3	PASS
T5	Local call targets resolve	symbol table	4	PASS
Composite verdict			5	PASS

Layer I_b — Behavioral Invariants (B1–B4)

Observable behavior over a defined corpus. B1–B3 use differential testing; B4 uses runtime enforcement.

Code	Condition	Check	Tests	Status
B1	Return values match	differential test	2	PASS
B2	Exceptions match	differential test	2	PASS
B3	stdout traces match	differential test	2	PASS
B4	No new side effects	runtime enforcement	7	PASS
Composite verdict			5	PASS

      ⚠ B4 scope: Monkeypatching is not a security sandbox. It detects
      accidental side effects introduced by transformations,
      not hostile code.
    

Decision Policy

The admissibility condition for any candidate P₁.

# Acceptance
Accept(P₁)     ⟺  I_s(P₁) ∧ I_t(P₁) ∧ I_b(P₁)

# Rejection
Reject(P₁)     ⟺  ¬I_s ∨ ¬I_t ∨ ¬I_b

# Golden rule
Inconclusive   ≠  Accepted   # default to rejection when in doubt
    

Failure Codes

Each rejection returns a specific failure code for debugging.

syntactic:parse

P₁ does not parse as valid Python.

syntactic:signature

Function signature changed.

structural:undefined_name

A name is used without a binding.

structural:cycle

An invalid dependency cycle was detected.

behavioral:return_mismatch

Return value differs from P₀.

behavioral:exception_mismatch

Exception differs from P₀.

behavioral:timeout

Timeout exceeded during differential test.

behavioral:side_effect

A blocked side effect was triggered (B4).

Transition Criteria — Function to Module Level

Extending to module-level rewriting is conditional. All four criteria must be met during the pilot study.

Mechanism Stability

TSR ≥ 90%

on valid transformations

Unsafe Detection

UDR ≥ 95%

on injected failures

Computational Cost

OH ≤ 2×

overhead vs baseline

Recovery Fidelity

SRF = 100%

in controlled tests

      ℹ These are proposed engineering gates for this research,
      not established scientific laws. They will be revised based on
      baseline calibration.
    

Hypotheses

Four hypotheses are defined for empirical evaluation.

ID	Statement	Status
H1	Isolated candidate execution reduces failure propagation compared to non-isolated execution.	Not yet tested
H2	Structural validation combined with differential testing detects more injected behavioral regressions than structural validation alone.	Not yet tested
H3	Controlled activation and rollback reduce deployment disruption compared to conventional replacement.	Not yet tested
H4	Successful rollback does not necessarily imply complete restoration of required execution state.	Not yet tested

      ⚠ Numerical thresholds will be established after baseline measurements
      and pilot calibration, not assumed before.
    

Metrics (Defined, Not Yet Measured)

The pilot will collect the following metrics.

Metric	Definition	Measurement
TSR	Transformation Success Rate	decision count
UDR	Unsafe-change Detection Rate	failure injection
FPR	False Positive Rate	ground-truth compare
FNR	False Negative Rate	ground-truth compare
OH	Runtime Overhead	`time.perf_counter`
MTTR	Mean Time to Recovery	rollback timing
SRF	State Restoration Fidelity	deferred (Phase III)

Threats to Validity

Explicit limitations of the current scope.

Type	Concern	Mitigation
Construct	Observation model determines what differential testing can detect	Explicit corpus + documented observables
Internal	Results may reflect implementation details	Fixed hardware, versions, workloads
External	Python-only results may not generalize	Scope explicitly restricted
Statistical	Pilot too small for general claims	Feasibility only; variance for future study
Security	Multiprocessing is not a hardened sandbox	Documented; not claimed