[Formalization] Remediation of Lean formal model semantic gaps, subtyping incompleteness, and scope relations

[bordumb]

A security audit of the Lean formal specifications in formal/Auths/ identified several semantic modeling discrepancies, subtyping incompleteness, and representation boundary gaps between the formal model and security expectations.

While the Lean theorems are verified within the current framework, resolving these modeling issues will improve formal specification accuracy, prevent misunderstandings regarding security guarantees, and eliminate unnecessary delegation rejection cases.

---

Identified Findings

1. Stateless Budget Ceiling Semantics

• Location: formal/Auths/Rich/Semantics.lean
• Issue: budgetCovers checks only whether an individual action request satisfies requested.value <= ceiling.value. The formal model maintains no cumulative spend state or ledger tracking across multiple actions.
• Risk: Terms like "Budget Ceiling" can be misconstrued as cumulative spend limits rather than per-action stateless bounds.
• Action: Clarify naming and document in the formal specification that BudgetCeiling represents a stateless per-action ceiling. If cumulative balance tracking is required, define explicit stateful ledger semantics in a follow-up specification.

2. Incomplete ActionConstraint Subtyping

• Location: formal/Auths/Rich/Semantics.lean
• Issue: actionConstraintLe returns False when comparing child = allowedBodyDigests {D} against parent = exactBodyDigest D, despite {D} containing only D.
• Risk: Valid, safe delegation tightenings are rejected due to syntactic constructor mismatch rather than semantic containment failure.
• Action: Update actionConstraintLe to recognize singleton set equivalence:
  • .allowedBodyDigests child <= .exactBodyDigest parent iff child = {parent}.
  • Prove transitivity and antisymmetry for the updated relation in formal/Auths/Rich/Theorems.lean.

3. Rigid Assurance Policy Equality Constraint

• Location: formal/Auths/Rich/Semantics.lean
• Issue: structuralScopeLe requires child.assurance = parent.assurance (exact identity).
• Risk: Delegated grants cannot tighten assurance policy requirements (e.g. upgrading from baseline to hardware MFA assurance).
• Action: Introduce an assuranceLe partial order or lattice to allow valid policy tightening, or explicitly document the exact-equality invariant requirement in formal/assurance-manifest-v1.toml.

4. Representation Assumptions (Time Boundaries & Vocabulary Equality)

• Location: formal/Auths/Rich/Types.lean, formal/Auths/Refinement/Production.lean
• Issue:
  • Validity windows use unbounded Nat values instead of bounded fixed-width integer types.
  • Vocabulary matching relies on literal byte-list equality (stringBytes), assuming pre-normalized input strings.
• Action: Document residual assumptions regarding canonical serialization, string normalization, and integer range bounds in the assurance manifest TCB section.

5. Failure Order Side-Channel Classification

• Location: formal/Auths/Rich/Semantics.lean
• Issue: evaluateCoverage short-circuits diagnostic reasons in a fixed precedence order (e.g., checking permissions before validity windows).
• Action: Add documentation clarifying that diagnostic return codes are deterministic failure reports and do not guarantee side-channel non-interference.

---

Proposed Implementation Plan

1. Update actionConstraintLe in formal/Auths/Rich/Semantics.lean to support singleton set subtyping against exactBodyDigest.
2. Update corresponding proofs in formal/Auths/Rich/Theorems.lean (action_constraint_trans, action_constraint_antisymm, action_constraint_allows_monotone).
3. Refactor assurance comparison in structuralScopeLe if policy tightening is intended.
4. Update formal/assurance-manifest-v1.toml to accurately reflect residual representation assumptions.
5. Re-run formal qualification gates to ensure Lean compilation and proof qualification pass cleanly.

---

Acceptance Criteria

• Lake builds without errors or warnings (lake build).
• Lean formal qualification passes (cargo xtask formal qualify aeneas).
• Transitive axiom audit remains free of unapproved axioms (cargo xtask formal).