diff --git a/0-Core-Formalism/lean/Semantics/AGENTS.md b/0-Core-Formalism/lean/Semantics/AGENTS.md new file mode 100644 index 00000000..0d579c78 --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/AGENTS.md @@ -0,0 +1,38 @@ +# AGENTS.md - Lean/Semantics + +Scope: `0-Core-Formalism/lean/Semantics/` + +The strict operating rules live in `../../../6-Documentation/docs/AGENTS.md`. +Follow those rules for all Lean, proof, fixed-point, hardware-extraction, and +shim-boundary work. + +## Local Rules + +- Keep module names aligned with file names and namespaces. +- Prefer small domain modules over utility files. +- Every new computational gate needs an executable witness: theorem, `#eval`, + or native-decision proof. +- Run the narrow build target first, for example: + +```bash +lake build Semantics.BeaverMaskFreshness +``` + +- Run the broader build before claiming a stable Lean surface: + +```bash +lake build +``` + +- Do not delete difficult theorems to make builds pass. Fix proofs or quarantine + with an explicit `TODO(lean-port): ...` boundary. +- Treat generated Python, Rust, Verilog, and JSON as shims or receipts, not as + the formal source of truth. + +## Current Stack-Solidification Anchors + +- `Semantics.BeaverMaskFreshness` is a finite admission gate for Beaver-mask + freshness negative controls. +- Stack status receipts live under `shared-data/data/stack_solidification/`. +- The current staged slice is documented in + `../../../6-Documentation/docs/stack_solidification_staging_manifest_2026-05-09.md`. diff --git a/0-Core-Formalism/lean/Semantics/Semantics/BeaverMaskFreshness.lean b/0-Core-Formalism/lean/Semantics/Semantics/BeaverMaskFreshness.lean new file mode 100644 index 00000000..a9472d7e --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/Semantics/BeaverMaskFreshness.lean @@ -0,0 +1,94 @@ +namespace Semantics.BeaverMaskFreshness + +/-- Source class for a Beaver-style mask coefficient. Only `freshRandom` + is admissible for privacy-equivalent Beaver masking in this gate model. -/ +inductive MaskSource where + | freshRandom + | reused + | topologyDerived + | adversarialChosen + deriving Repr, DecidableEq, BEq + +/-- A finite audit event for one mask coefficient. -/ +structure MaskEvent where + epoch : Nat + party : Nat + maskId : Nat + source : MaskSource + deriving Repr, DecidableEq, BEq + +def sourceFreshIndependent (source : MaskSource) : Bool := + source == MaskSource.freshRandom + +def eventFreshIndependent (event : MaskEvent) : Bool := + sourceFreshIndependent event.source + +def maskIdUsedBefore (maskId : Nat) : List MaskEvent → Bool + | [] => false + | event :: rest => (event.maskId == maskId) || maskIdUsedBefore maskId rest + +/-- Admission gate for treating a coefficient as a privacy-equivalent mask. + It must be fresh/independent and its mask id must not already occur in the + receipt history. -/ +def admissibleMaskEvent (history : List MaskEvent) (event : MaskEvent) : Bool := + eventFreshIndependent event && !maskIdUsedBefore event.maskId history + +def admitMaskEvent (history : List MaskEvent) (event : MaskEvent) : Option (List MaskEvent) := + if admissibleMaskEvent history event then + some (event :: history) + else + none + +def freshA : MaskEvent := + { epoch := 0, party := 0, maskId := 1001, source := MaskSource.freshRandom } + +def freshB : MaskEvent := + { epoch := 0, party := 1, maskId := 1002, source := MaskSource.freshRandom } + +def reusedA : MaskEvent := + { epoch := 1, party := 0, maskId := 1001, source := MaskSource.reused } + +def topologyA : MaskEvent := + { epoch := 1, party := 0, maskId := 2001, source := MaskSource.topologyDerived } + +def adversarialA : MaskEvent := + { epoch := 1, party := 0, maskId := 3001, source := MaskSource.adversarialChosen } + +/-- Positive control: a fresh random mask with an unused id admits. -/ +theorem freshUnusedAdmits : + admissibleMaskEvent [] freshA = true := by + native_decide + +/-- Positive control: distinct fresh random mask ids may both admit. -/ +theorem distinctFreshSequenceAdmits : + admitMaskEvent [freshA] freshB = some [freshB, freshA] := by + native_decide + +/-- Negative control: an explicit reused-source coefficient is rejected. -/ +theorem reusedSourceRejected : + admissibleMaskEvent [freshA] reusedA = false := by + native_decide + +/-- Negative control: even if source were mislabeled fresh, mask-id reuse is rejected. -/ +theorem reusedMaskIdRejected : + admissibleMaskEvent [freshA] { reusedA with source := MaskSource.freshRandom } = false := by + native_decide + +/-- Negative control: topology-derived adaptive coefficients are not treated as + privacy-equivalent random masks by this gate. -/ +theorem topologyDerivedRejected : + admissibleMaskEvent [] topologyA = false := by + native_decide + +/-- Negative control: adversarially chosen coefficients are rejected. -/ +theorem adversarialChosenRejected : + admissibleMaskEvent [] adversarialA = false := by + native_decide + +#eval admissibleMaskEvent [] freshA +#eval admissibleMaskEvent [freshA] reusedA +#eval admissibleMaskEvent [freshA] { reusedA with source := MaskSource.freshRandom } +#eval admissibleMaskEvent [] topologyA +#eval admissibleMaskEvent [] adversarialA + +end Semantics.BeaverMaskFreshness diff --git a/0-Core-Formalism/lean/Semantics/Semantics/WhitespaceFreeGrammar.lean b/0-Core-Formalism/lean/Semantics/Semantics/WhitespaceFreeGrammar.lean new file mode 100644 index 00000000..54057b51 --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/Semantics/WhitespaceFreeGrammar.lean @@ -0,0 +1,78 @@ +namespace Semantics.WhitespaceFreeGrammar + +/-! +Whitespace-free grammar gate. + +The intended compression rule is narrow: + +* symbol payloads are stored; +* ordinary inter-symbol whitespace is derived from symbol count/order; +* no whitespace symbol is admitted into the payload stream; +* non-canonical spacing needs a residual and therefore remains outside this + zero-whitespace gate. +-/ + +/-- A finite grammar atom represented by its payload byte count. -/ +structure GrammarAtom where + payloadBytes : Nat + deriving Repr, DecidableEq, BEq + +/-- Payload cost counts symbols only. Whitespace is not a symbol. -/ +def payloadBytes : List GrammarAtom -> Nat + | [] => 0 + | atom :: rest => atom.payloadBytes + payloadBytes rest + +/-- Number of derivable inter-symbol boundaries. -/ +def derivedBoundaryCount : List GrammarAtom -> Nat + | [] => 0 + | [_] => 0 + | _ :: rest => 1 + derivedBoundaryCount rest + +/-- Stored whitespace codes are always zero in this gate. -/ +def storedWhitespaceCodes (_atoms : List GrammarAtom) : Nat := 0 + +/-- Stored cost under the zero-whitespace grammar. -/ +def storedBytes (atoms : List GrammarAtom) : Nat := + payloadBytes atoms + storedWhitespaceCodes atoms + +/-- Decoded display bytes if every derived boundary replays as one ASCII space. + This is a replay cost, not a stored cost. -/ +def canonicalDisplayBytes (atoms : List GrammarAtom) : Nat := + payloadBytes atoms + derivedBoundaryCount atoms + +def atomA : GrammarAtom := { payloadBytes := 5 } +def atomB : GrammarAtom := { payloadBytes := 4 } +def atomC : GrammarAtom := { payloadBytes := 7 } +def exampleAtoms : List GrammarAtom := [atomA, atomB, atomC] + +theorem exampleStoredWhitespaceZero : + storedWhitespaceCodes exampleAtoms = 0 := by + native_decide + +theorem exampleStoredCostDropsDerivedSpaces : + storedBytes exampleAtoms = payloadBytes exampleAtoms := by + native_decide + +theorem exampleDerivedBoundaryCount : + derivedBoundaryCount exampleAtoms = 2 := by + native_decide + +theorem exampleCanonicalDisplayCost : + canonicalDisplayBytes exampleAtoms = storedBytes exampleAtoms + 2 := by + native_decide + +theorem emptyHasNoWhitespaceCodes : + storedWhitespaceCodes [] = 0 ∧ derivedBoundaryCount [] = 0 := by + native_decide + +theorem singletonHasNoDerivedBoundary : + storedWhitespaceCodes [atomA] = 0 ∧ derivedBoundaryCount [atomA] = 0 := by + native_decide + +#eval storedWhitespaceCodes exampleAtoms +#eval payloadBytes exampleAtoms +#eval storedBytes exampleAtoms +#eval derivedBoundaryCount exampleAtoms +#eval canonicalDisplayBytes exampleAtoms + +end Semantics.WhitespaceFreeGrammar diff --git a/4-Infrastructure/AGENTS.md b/4-Infrastructure/AGENTS.md new file mode 100644 index 00000000..6e8f0a84 --- /dev/null +++ b/4-Infrastructure/AGENTS.md @@ -0,0 +1,40 @@ +# AGENTS.md - Infrastructure And Hardware + +Scope: `4-Infrastructure/` + +## Rules + +- Keep infrastructure scripts receipt-bearing: every probe should have a + machine-readable output or update an existing receipt. +- Separate software witnesses from live hardware witnesses. +- Do not claim FPGA acceleration from bitstream generation alone. +- Do not claim UART/fabric success without observed bytes or a matching hardware + receipt. +- Treat `/usr/bin/sem` as GNU Parallel on this machine unless proven otherwise; + use the isolated `sem` binary documented in stack solidification receipts when + needed. + +## Preferred Checks + +```bash +python3 -m py_compile 4-Infrastructure/shim/