From 53d6d0df88917b74b36ad8095f171d48283ff84e Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Mon, 11 May 2026 22:08:10 -0500 Subject: [PATCH] Stage stack solidification source slice --- 0-Core-Formalism/lean/Semantics/AGENTS.md | 38 + .../Semantics/BeaverMaskFreshness.lean | 94 ++ .../Semantics/WhitespaceFreeGrammar.lean | 78 + 4-Infrastructure/AGENTS.md | 40 + .../hardware/build_uart_beacon.sh | 44 + .../hardware/tangnano9k_uart_beacon.v | 84 + .../hardware/tangnano9k_uart_swapped.cst | 27 + ...beaver_mask_freshness_negative_controls.py | 183 +++ .../custom_equation_awareness_manifest.py | 390 +++++ .../shim/desi_epoviz_population_cell_join.py | 398 +++++ .../shim/desi_epoviz_row_eigenmass_probe.py | 445 +++++ .../shim/external_sem_entity_diff_probe.py | 170 ++ .../shim/hutter_eigenmass_transfer_plan.py | 276 ++++ .../shim/hutter_transfer_readiness_fixture.py | 263 +++ .../shim/network_topology_hold_manifests.py | 174 ++ .../shim/rrc_hold_closure_checklist.py | 148 ++ 4-Infrastructure/shim/rrc_tri_cycle_audit.py | 495 ++++++ .../shim/smn_tool_awareness_registry.py | 205 +++ .../shim/stack_fail_closure_register.py | 346 ++++ .../shim/stack_solidification_audit.py | 500 ++++++ .../stellar_gas_abelian_sandpile_probe.py | 324 ++++ .../stellar_gas_eigenvector_mass_probe.py | 409 +++++ ...ellar_gas_full_cell_eigenmass_stability.py | 586 +++++++ ...llar_gas_multiscale_eigenmass_alignment.py | 291 ++++ .../stellar_gas_population_grouping_study.py | 620 +++++++ .../shim/stellar_gas_sandpile_fine_zoom.py | 281 ++++ .../shim/stellar_gas_sandpile_graph_replay.py | 444 +++++ .../tang9k_rrc_q16_virtual_serial_probe.py | 246 +++ .../shim/tang9k_uart_beacon_probe.py | 87 + .../shim/tang9k_uart_transport_router.py | 196 +++ .../shim/whitespace_zero_grammar_probe.py | 191 +++ 5-Applications/compression-core/src/oisc.rs | 406 +++++ ..._freshness_negative_controls_2026-05-09.md | 37 + ...z_manga_population_cell_join_2026-05-09.md | 84 + ...i_epoviz_row_eigenmass_probe_2026-05-09.md | 76 + ...noirlab2610_calibration_note_2026-05-09.md | 78 + ...ellar_gas_distribution_prior_2026-05-09.md | 86 + ...ternal_sem_entity_diff_probe_2026-05-09.md | 79 + .../fpga_direct_probe_report_2026-05-09.md | 206 +++ .../fpga_rrc_q16_accel_setup_2026-05-09.md | 171 ++ .../fpga_uart_route_analysis_2026-05-09.md | 173 ++ ...ion_topological_soliton_lane_2026-05-09.md | 207 +++ ...tter_eigenmass_transfer_plan_2026-05-09.md | 127 ++ ...r_readiness_fixture_manifest_2026-05-09.md | 32 + ..._reference_genomics_logogram_2026-05-09.md | 164 ++ ...work_topology_hold_manifests_2026-05-09.md | 51 + ...indrome_hex_symmetry_markers_2026-05-09.md | 151 ++ ...ive_harmony_social_synchrony_2026-05-09.md | 181 +++ .../rrc_hold_closure_checklist_2026-05-09.md | 88 + .../docs/rrc_tri_cycle_audit_2026-05-09.md | 107 ++ ...ckwave_eigenvalue_comparison_2026-05-09.md | 175 ++ .../LAW_GATED_RECONSTRUCTION_CORE_SHIFT.md | 249 +++ ...NDIRECTION_LOGOGRAM_DESIGN_AND_COMPILER.md | 1427 +++++++++++++++++ .../docs/specs/SMN_SEMANTIC_MASS_NUMBERS.md | 150 ++ .../stack_fail_closure_register_2026-05-09.md | 129 ++ .../stack_solidification_kanban_2026-05-09.md | 89 + ...idification_staging_manifest_2026-05-09.md | 226 +++ .../stack_solidification_status_2026-05-09.md | 81 + ...r_gas_abelian_sandpile_probe_2026-05-09.md | 69 + ...r_gas_eigenvector_mass_probe_2026-05-09.md | 69 + ...ull_cell_eigenmass_stability_2026-05-09.md | 85 + ...ltiscale_eigenmass_alignment_2026-05-09.md | 62 + ...as_population_grouping_study_2026-05-09.md | 100 ++ ...ellar_gas_sandpile_fine_zoom_2026-05-09.md | 43 + ...ar_gas_sandpile_graph_replay_2026-05-09.md | 157 ++ ...rrc_q16_virtual_serial_probe_2026-05-09.md | 21 + ...tang9k_uart_transport_routes_2026-05-09.md | 31 + ...ogical_soliton_equation_pack_2026-05-09.md | 371 +++++ ...water_shock_public_benchmark_2026-05-09.md | 233 +++ .../whitespace_zero_grammar_2026-05-09.md | 34 + 70 files changed, 14378 insertions(+) create mode 100644 0-Core-Formalism/lean/Semantics/AGENTS.md create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/BeaverMaskFreshness.lean create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/WhitespaceFreeGrammar.lean create mode 100644 4-Infrastructure/AGENTS.md create mode 100755 4-Infrastructure/hardware/build_uart_beacon.sh create mode 100644 4-Infrastructure/hardware/tangnano9k_uart_beacon.v create mode 100644 4-Infrastructure/hardware/tangnano9k_uart_swapped.cst create mode 100644 4-Infrastructure/shim/beaver_mask_freshness_negative_controls.py create mode 100644 4-Infrastructure/shim/custom_equation_awareness_manifest.py create mode 100644 4-Infrastructure/shim/desi_epoviz_population_cell_join.py create mode 100644 4-Infrastructure/shim/desi_epoviz_row_eigenmass_probe.py create mode 100644 4-Infrastructure/shim/external_sem_entity_diff_probe.py create mode 100644 4-Infrastructure/shim/hutter_eigenmass_transfer_plan.py create mode 100644 4-Infrastructure/shim/hutter_transfer_readiness_fixture.py create mode 100644 4-Infrastructure/shim/network_topology_hold_manifests.py create mode 100644 4-Infrastructure/shim/rrc_hold_closure_checklist.py create mode 100755 4-Infrastructure/shim/rrc_tri_cycle_audit.py create mode 100644 4-Infrastructure/shim/smn_tool_awareness_registry.py create mode 100644 4-Infrastructure/shim/stack_fail_closure_register.py create mode 100644 4-Infrastructure/shim/stack_solidification_audit.py create mode 100644 4-Infrastructure/shim/stellar_gas_abelian_sandpile_probe.py create mode 100644 4-Infrastructure/shim/stellar_gas_eigenvector_mass_probe.py create mode 100644 4-Infrastructure/shim/stellar_gas_full_cell_eigenmass_stability.py create mode 100644 4-Infrastructure/shim/stellar_gas_multiscale_eigenmass_alignment.py create mode 100644 4-Infrastructure/shim/stellar_gas_population_grouping_study.py create mode 100644 4-Infrastructure/shim/stellar_gas_sandpile_fine_zoom.py create mode 100644 4-Infrastructure/shim/stellar_gas_sandpile_graph_replay.py create mode 100644 4-Infrastructure/shim/tang9k_rrc_q16_virtual_serial_probe.py create mode 100644 4-Infrastructure/shim/tang9k_uart_beacon_probe.py create mode 100644 4-Infrastructure/shim/tang9k_uart_transport_router.py create mode 100644 4-Infrastructure/shim/whitespace_zero_grammar_probe.py create mode 100644 5-Applications/compression-core/src/oisc.rs create mode 100644 6-Documentation/docs/beaver_mask_freshness_negative_controls_2026-05-09.md create mode 100644 6-Documentation/docs/desi_epoviz_manga_population_cell_join_2026-05-09.md create mode 100644 6-Documentation/docs/desi_epoviz_row_eigenmass_probe_2026-05-09.md create mode 100644 6-Documentation/docs/desi_noirlab2610_calibration_note_2026-05-09.md create mode 100644 6-Documentation/docs/desi_stellar_gas_distribution_prior_2026-05-09.md create mode 100644 6-Documentation/docs/external_sem_entity_diff_probe_2026-05-09.md create mode 100644 6-Documentation/docs/fpga_direct_probe_report_2026-05-09.md create mode 100644 6-Documentation/docs/fpga_rrc_q16_accel_setup_2026-05-09.md create mode 100644 6-Documentation/docs/fpga_uart_route_analysis_2026-05-09.md create mode 100644 6-Documentation/docs/hopfion_topological_soliton_lane_2026-05-09.md create mode 100644 6-Documentation/docs/hutter_eigenmass_transfer_plan_2026-05-09.md create mode 100644 6-Documentation/docs/hutter_transfer_readiness_fixture_manifest_2026-05-09.md create mode 100644 6-Documentation/docs/matched_reference_genomics_logogram_2026-05-09.md create mode 100644 6-Documentation/docs/network_topology_hold_manifests_2026-05-09.md create mode 100644 6-Documentation/docs/palindrome_hex_symmetry_markers_2026-05-09.md create mode 100644 6-Documentation/docs/predictive_harmony_social_synchrony_2026-05-09.md create mode 100644 6-Documentation/docs/rrc_hold_closure_checklist_2026-05-09.md create mode 100644 6-Documentation/docs/rrc_tri_cycle_audit_2026-05-09.md create mode 100644 6-Documentation/docs/shockwave_eigenvalue_comparison_2026-05-09.md create mode 100644 6-Documentation/docs/specs/LAW_GATED_RECONSTRUCTION_CORE_SHIFT.md create mode 100644 6-Documentation/docs/specs/OMINDIRECTION_LOGOGRAM_DESIGN_AND_COMPILER.md create mode 100644 6-Documentation/docs/specs/SMN_SEMANTIC_MASS_NUMBERS.md create mode 100644 6-Documentation/docs/stack_fail_closure_register_2026-05-09.md create mode 100644 6-Documentation/docs/stack_solidification_kanban_2026-05-09.md create mode 100644 6-Documentation/docs/stack_solidification_staging_manifest_2026-05-09.md create mode 100644 6-Documentation/docs/stack_solidification_status_2026-05-09.md create mode 100644 6-Documentation/docs/stellar_gas_abelian_sandpile_probe_2026-05-09.md create mode 100644 6-Documentation/docs/stellar_gas_eigenvector_mass_probe_2026-05-09.md create mode 100644 6-Documentation/docs/stellar_gas_full_cell_eigenmass_stability_2026-05-09.md create mode 100644 6-Documentation/docs/stellar_gas_multiscale_eigenmass_alignment_2026-05-09.md create mode 100644 6-Documentation/docs/stellar_gas_population_grouping_study_2026-05-09.md create mode 100644 6-Documentation/docs/stellar_gas_sandpile_fine_zoom_2026-05-09.md create mode 100644 6-Documentation/docs/stellar_gas_sandpile_graph_replay_2026-05-09.md create mode 100644 6-Documentation/docs/tang9k_rrc_q16_virtual_serial_probe_2026-05-09.md create mode 100644 6-Documentation/docs/tang9k_uart_transport_routes_2026-05-09.md create mode 100644 6-Documentation/docs/topological_soliton_equation_pack_2026-05-09.md create mode 100644 6-Documentation/docs/underwater_shock_public_benchmark_2026-05-09.md create mode 100644 6-Documentation/docs/whitespace_zero_grammar_2026-05-09.md 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/