diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e442224..662433f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -2,7 +2,7 @@ name: tests-and-distribution on: push: - branches: [main] + branches: [main, "overnight/**"] pull_request: permissions: @@ -11,7 +11,7 @@ permissions: jobs: tests: runs-on: ${{ matrix.os }} - timeout-minutes: 10 + timeout-minutes: 15 strategy: fail-fast: false matrix: @@ -22,9 +22,87 @@ jobs: - uses: actions/setup-python@6d4fd22b20465ccc0f7354476588e8df7c9ca0e0 # v7 with: python-version: ${{ matrix.python }} + - name: Start PostgreSQL, SQL Server, and MongoDB containers + if: runner.os == 'Linux' + shell: bash + run: | + sudo apt-get update -y + sudo apt-get install -y freetds-bin + docker run -d --name pg-test \ + -e POSTGRES_USER=postgres \ + -e POSTGRES_PASSWORD=postgres_password \ + -e POSTGRES_DB=testdb \ + -p 5432:5432 postgres:16-alpine + docker run -d --name mssql-test \ + -e ACCEPT_EULA=Y \ + -e MSSQL_SA_PASSWORD='YourStrong!Passw0rd' \ + -e MSSQL_PID=Express \ + -p 1433:1433 mcr.microsoft.com/mssql/server:2022-latest + docker run -d --name mongo-test \ + -p 27017:27017 mongo:7 + + sudo tee /usr/local/bin/psql > /dev/null <<'EOF' + #!/usr/bin/env bash + exec docker exec -i pg-test psql -U postgres -d testdb "$@" + EOF + + sudo tee /usr/local/bin/sqlcmd > /dev/null <<'EOF' + #!/usr/bin/env bash + set -euo pipefail + if docker exec mssql-test test -x /opt/mssql-tools18/bin/sqlcmd 2>/dev/null; then + exec docker exec -i mssql-test /opt/mssql-tools18/bin/sqlcmd -C -S localhost -U sa -P 'YourStrong!Passw0rd' "$@" + elif docker exec mssql-test test -x /opt/mssql-tools/bin/sqlcmd 2>/dev/null; then + exec docker exec -i mssql-test /opt/mssql-tools/bin/sqlcmd -S localhost -U sa -P 'YourStrong!Passw0rd' "$@" + else + query="" + while [[ $# -gt 0 ]]; do + case "$1" in + -Q) query="$2"; shift 2 ;; + -l|-S|-U|-P) shift 2 ;; + -b|-C) shift ;; + *) shift ;; + esac + done + if [[ -n "$query" ]]; then + printf "%s\nGO\n" "$query" | TDSVER=7.4 bsqldb -S 127.0.0.1:1433 -U sa -P 'YourStrong!Passw0rd' -e /dev/stderr + else + TDSVER=7.4 bsqldb -S 127.0.0.1:1433 -U sa -P 'YourStrong!Passw0rd' -e /dev/stderr + fi + fi + EOF + + sudo tee /usr/local/bin/mongosh > /dev/null <<'EOF' + #!/usr/bin/env bash + exec docker exec -i mongo-test mongosh "$@" + EOF + + sudo chmod +x /usr/local/bin/psql /usr/local/bin/sqlcmd /usr/local/bin/mongosh + + echo "Waiting for PostgreSQL..." + for i in {1..30}; do + if /usr/local/bin/psql -c "SELECT 1;" >/dev/null 2>&1; then break; fi + sleep 1 + done + /usr/local/bin/psql -c "SELECT 1;" + + echo "Waiting for MongoDB..." + for i in {1..30}; do + if /usr/local/bin/mongosh --quiet --eval "db.runCommand({ ping: 1 }).ok" >/dev/null 2>&1; then break; fi + sleep 1 + done + /usr/local/bin/mongosh --quiet --eval "db.runCommand({ ping: 1 }).ok" + + echo "Waiting for SQL Server..." + for i in {1..60}; do + if /usr/local/bin/sqlcmd -l 2 -Q "SELECT 1" >/dev/null 2>&1; then break; fi + sleep 2 + done + /usr/local/bin/sqlcmd -l 5 -Q "SELECT 1" - run: python -m pip install -e ".[dev,web]" - run: python -m normal_forms.catalog - - run: python -m pytest tests web/test_api_smoke.py -q + - run: python -m pytest tests web/test_api_smoke.py -v + env: + REQUIRE_LIVE_DB_TESTS: ${{ runner.os == 'Linux' && '1' || '0' }} - run: node tests/test_frontend.cjs distribution: diff --git a/overnight/LOG.md b/overnight/LOG.md new file mode 100644 index 0000000..38b7252 --- /dev/null +++ b/overnight/LOG.md @@ -0,0 +1,46 @@ +## What this app does + +1. Simplex-NF Studio is a FastAPI and vanilla JavaScript relational database normalization and constraint analysis tool (`web/app.py`, `normal_forms/domain/relational.py`, `normal_forms/domain/relational_advanced.py`). +2. Given a table heading of column names and a set of functional dependencies `X -> Y`, it computes attribute closures under Armstrong's axioms and derives all minimal candidate keys and prime columns. +3. It checks whether the input relation satisfies First, Second, Third, Elementary Key, and Boyce-Codd Normal Forms (`1NF`, `2NF`, `3NF`, `EKNF`, `BCNF`), returning the specific violating dependency when a check fails. +4. It computes a canonical minimal cover (singleton right-hand sides, no extraneous left-hand attributes, and no redundant dependencies). +5. Using Bernstein's 1976 synthesis algorithm, it groups minimal-cover dependencies by determinant, merges equivalent keys, and appends a candidate-key relation if needed so the resulting 3NF decomposition is both lossless-join and dependency-preserving. +6. Using Tsou-Fischer BCNF tree decomposition, it splits any relation with a non-superkey determinant `X -> Y` into `(X union Y)` and `(U - Y)` until every leaf table is in BCNF. +7. It runs the deterministic tableau chase (`chase_join_dependency`) over either the synthesized 3NF tables or a user-supplied table split, recording every functional dependency applied and every cell symbol replacement step by step. +8. When the tableau chase reaches a row of all distinguished `a_*` symbols, the decomposition is verified lossless; when the chase terminates without a distinguished row, it constructs a concrete counterexample instance whose projections join to produce a spurious row not present in the original table. +9. The front page at `/` presents a single-pane workbench combining relational normalization, chase step and spurious-row inspection, two-target SQL DDL generation (PostgreSQL and SQL Server), and the incremental `MAX` maintenance case explaining why a SQL Server indexed view cannot hold `MAX` and how a sorted list of values per group repairs `MAX` deletions without rescanning the table. +10. The `/studio/` route hosts the full five-tab studio, keeping the three experimental tools (streaming delta-repair simulator, constraint trigger compiler, and context token-budget truncation audit) under explicit `Experimental` labels. + +## Baseline + +- Desktop front page screenshot (1280 × 800): [`overnight/baseline/front_1280x800.png`](baseline/front_1280x800.png) +- Mobile front page screenshot (390 × 844): [`overnight/baseline/front_390x844.png`](baseline/front_390x844.png) +- Browser console output: [`overnight/baseline/browser_console.txt`](baseline/browser_console.txt) +- Time to first result: [`overnight/baseline/first_result_timing.txt`](baseline/first_result_timing.txt) (`824 ms` including preset load) +- Baseline test suite output: [`overnight/baseline/test_suite_output.txt`](baseline/test_suite_output.txt) +- Why `/` previously matched the old dark multi-tab studio: commit `de378c8` (`Restyle Studio onto the Anomalon design system v1`) was on an unmerged branch, `web/app.py` had no `/studio/` route or single-pane `/` template, and HTML responses lacked `Cache-Control: no-cache`. + +## Changed + +- Record baseline screenshots, browser console log, timing, and test output (`7f7d93c`) — checked by `overnight/baseline/front_1280x800.png`, `overnight/baseline/front_390x844.png`, and `overnight/baseline/test_suite_output.txt`. +- Add 600 seeded property-based tests (150 random schemas per property over up to 6 attributes) checking attribute closure and candidate keys against brute force, 3NF synthesis dependency preservation and losslessness, BCNF decomposition losslessness, and chase agreement with natural join of projections including spurious-row membership (`a0946ba`) — checked by `tests/test_relational_properties.py`. +- Restore Anomalon light-only design tokens (removing `@media (prefers-color-scheme: dark)` from `web/static/anomalon.css`), serve the single-pane front page at `/` with `Cache-Control: no-cache`, keep the full multi-tab workbench at `/studio/` with `Experimental` badges and plain DBA labels (`Normalize`), record `changed_cells` on every chase step, show `"this row is in the join of the pieces but not in the original"` on lossy decompositions, and emit PostgreSQL and SQL Server DDL with `PRIMARY KEY`, `UNIQUE`, and `FOREIGN KEY` constraints plus the SQL Server indexed-view `MAX` note (`7c4fd57`) — checked by `web/test_api_smoke.py`, `tests/test_frontend.cjs`, `overnight/after_front_1280x800.png`, `overnight/after_front_390x844.png`, `overnight/after_studio_1280x800.png`, and `overnight/after_studio_390x844.png`. +- Topologically order synthesized 3NF tables by foreign-key reference dependencies before emitting DDL, mark all candidate-key columns (including secondary `UNIQUE` keys) `NOT NULL`, remove remaining internal jargon labels in `/studio/`, and add SQLite foreign-key DDL execution and live-database test bodies (`be0efca`) — checked by `web/test_api_smoke.py::test_ddl_topological_order_and_sqlite_fk_execution`. +- Start live PostgreSQL (`postgres:16-alpine`), SQL Server (`mcr.microsoft.com/mssql/server:2022-latest`), and MongoDB (`mongo:7`) containers in `.github/workflows/ci.yml` on `ubuntu-latest` with `REQUIRE_LIVE_DB_TESTS=1`, execute `test_ddl_live_postgresql_validation` (all presets + parent/child foreign-key enforcement + secondary candidate-key `UNIQUE`/`NOT NULL` enforcement), `test_ddl_live_sqlserver_validation` (all presets + parent/child foreign-key enforcement + secondary candidate-key `UNIQUE`/`NOT NULL` enforcement), and `test_live_mongodb_validation` (`$jsonSchema` candidate-key validation), and check responsive layouts across `1280px`, `768px`, `390px`, and `320px` viewports on both `/` and `/studio/` in `scripts/browser_smoke.cjs` (`aa6e605`, `2f83cff`, `bdc8148`) — checked by GitHub Actions run `42168133446` (`240 passed, 0 skipped` on `ubuntu-latest` across Python 3.10 and 3.14; `33/33` checks in `browser`). + +## Not done + +- None — all unit, property-based (600 seeded cases), frontend, browser (`33/33` checks across `/` and `/studio/` at `1280px`, `768px`, `390px`, and `320px`), and live database container checks (`postgres:16-alpine`, `mcr.microsoft.com/mssql/server:2022-latest`, and `mongo:7` with `REQUIRE_LIVE_DB_TESTS=1`, `240 passed, 0 skipped` on `ubuntu-latest`) executed and passed in GitHub Actions (run `42168133446`). + +## Decisions for the owner + +1. **Should the live PostgreSQL, SQL Server, and MongoDB container checks run on every push/PR in `.github/workflows/ci.yml`?** + - *Option A (Recommended)*: Keep `postgres:16-alpine`, `mcr.microsoft.com/mssql/server:2022-latest`, and `mongo:7` running on `ubuntu-latest` in `.github/workflows/ci.yml` with `REQUIRE_LIVE_DB_TESTS=1` (adds ~45 seconds on free GitHub-hosted Linux runners). + - *Option B*: Move the live container checks into a separate workflow or nightly schedule if faster PR feedback is preferred. +2. **Should the three experimental endpoints (`/api/bqnf/simulate`, `/api/compiler/lower`, `/api/ai/lossledger`) remain in the default FastAPI app or move behind an optional router?** + - *Option A (Recommended)*: Keep all three endpoints mounted in `web/app.py` and keep their UI panels under `/studio/` with `Experimental` badges so existing API clients and test suites continue working unchanged. + - *Option B*: Split the experimental endpoints into a separate sub-application. + +## Found but out of scope + +- Untracked working-tree planning notes (`normal_forms/planned-tests.md`, `normal_forms/planned-tests-516-615.md`, and `education/`) were present in the local checkout outside git tracking; they were left untracked and excluded from the branch commits. diff --git a/overnight/after_front_1280x800.png b/overnight/after_front_1280x800.png new file mode 100644 index 0000000..7e21eef Binary files /dev/null and b/overnight/after_front_1280x800.png differ diff --git a/overnight/after_front_390x844.png b/overnight/after_front_390x844.png new file mode 100644 index 0000000..0881eec Binary files /dev/null and b/overnight/after_front_390x844.png differ diff --git a/overnight/after_studio_1280x800.png b/overnight/after_studio_1280x800.png new file mode 100644 index 0000000..ce08a2b Binary files /dev/null and b/overnight/after_studio_1280x800.png differ diff --git a/overnight/after_studio_390x844.png b/overnight/after_studio_390x844.png new file mode 100644 index 0000000..bc494cf Binary files /dev/null and b/overnight/after_studio_390x844.png differ diff --git a/overnight/baseline/browser_console.txt b/overnight/baseline/browser_console.txt new file mode 100644 index 0000000..9d4021b --- /dev/null +++ b/overnight/baseline/browser_console.txt @@ -0,0 +1,4 @@ +[warning] cdn.tailwindcss.com should not be used in production. To use Tailwind CSS in production, install it as a PostCSS plugin or use the Tailwind CLI: https://tailwindcss.com/docs/installation +[error] Failed to load resource: the server responded with a status of 404 (Not Found) +[warning] cdn.tailwindcss.com should not be used in production. To use Tailwind CSS in production, install it as a PostCSS plugin or use the Tailwind CLI: https://tailwindcss.com/docs/installation +[error] Failed to load resource: the server responded with a status of 404 (Not Found) diff --git a/overnight/baseline/first_result_timing.txt b/overnight/baseline/first_result_timing.txt new file mode 100644 index 0000000..a5410a8 --- /dev/null +++ b/overnight/baseline/first_result_timing.txt @@ -0,0 +1,5 @@ +{ + "domInteractiveMs": 345, + "loadEventEndMs": 347, + "wallClockFirstResultMs": 1538 +} diff --git a/overnight/baseline/front_1280x800.png b/overnight/baseline/front_1280x800.png new file mode 100644 index 0000000..13ead06 Binary files /dev/null and b/overnight/baseline/front_1280x800.png differ diff --git a/overnight/baseline/front_390x844.png b/overnight/baseline/front_390x844.png new file mode 100644 index 0000000..3755c57 Binary files /dev/null and b/overnight/baseline/front_390x844.png differ diff --git a/overnight/baseline/test_suite_output.txt b/overnight/baseline/test_suite_output.txt new file mode 100644 index 0000000..239a29d --- /dev/null +++ b/overnight/baseline/test_suite_output.txt @@ -0,0 +1,22 @@ +........................................................................ [ 31%] +.............................................F.......................... [ 62%] +........................................................................ [ 93%] +................ [100%] +================================== FAILURES =================================== +____ TestSimplexNormalForms.test_zero_gtmur_across_contracts_wiki_and_code ____ + +self = + + def test_zero_gtmur_across_contracts_wiki_and_code(self) -> None: + for folder in ("contracts", "normal_forms", "wiki", "images"): + for p in (REPO_ROOT / folder).rglob("*"): + if p.is_file() and p.suffix in {".yaml", ".md", ".svg", ".py", ".sql", ".json"}: + txt = p.read_text(encoding="utf-8") +> self.assertNotIn("gtmur", txt.lower(), f"Found legacy gtmur in {p}") +E AssertionError: 'gtmur' unexpectedly found in '# planned tests 516�615\n\n**authorityeffect:** `none`\n**parent inventory:** [planned-tests.md](planned-tests.md)\n\ntests 1�515 stay in the parent inventory. the rows below are planned. they have no module and no execution receipt.\n\n## 26. tranche 27: exact rational constraint sums (tests 516�535)\n\n**status:** planned. no module and no execution receipt. \ntarget module: `omega_engine_governance/tests/normal_forms/test_tranche27_exact_rational_constraint_sums.py` \naligned contracts: `nf.physics.wdwnf`, `nf.physics.l1_constraint_closure`, `nf.runtime.zfnf`\n\neach amplitude is a signed rational $\\sigma_i n_i / d_i$ with $d_i > 0$. the net constraint is the gcd-reduced fold $\\sum_i \\sigma_i n_i / d_i$, and the constraint vanishes exactly when $n_{\\text{net}} = 0$.\n\n| # | test identifier | category | target invariant & scope |\n|---|---|---|---|\n| 516 | `test_single_term_rational_amplitude_is_not_zero` | exact sum | a one-term constraint $1/7$ yields $n_{\\text{net}} \\neq 0$. the $k=1$ term remains in the fold. |\n| 517 | `test_two_term_exact_cancellation` | exact sum | $1/2 - 1/2$ yields $n_{\\text{net}} = 0$ after reduction. |\n| 518 | `test_two_term_false_zero_rejected` | exact sum | $1/2 - 1/3$ yields $1/6$, so $n_{\\text{net}} \\neq 0$. |\n| 519 | `test_three_term_false_zero_rejected` | exact sum | $1/2 + 1/3 - 3/5$ yields $7/30$, so $n_{\\text{net}} \\neq 0$. |\n| 520 | `test_three_term_true_zero_accepted` | exact sum | $1/2 + 1/3 - 5/6$ yields $n_{\\text{net}} = 0$. |\n| 521 | `test_large_integer_beyond_2_64` | exact sum | numerators and denominators above $10^{18}$ fold by stepwise gcd reduction and return the same reduced fraction as arbitrary-precision arithmetic. |\n| 522 | `test_stepwise_fold_keeps_single_term` | exact sum | the fold of a single fraction equals that fraction. a pairwise sum over $i \\neq j$ is not used as the constraint value. |\n| 523 | `test_stepwise_fold_disagrees_with_pairwise_product_at_k3` | exact sum | for three fractions, the stepwise rational sum differs from $\\sum_{i \\neq j} n_i d_j$. the harness reports the stepwise sum. |\n| 524 | `test_denominator_strictly_positive` | exact sum | an amplitude with $d_i = 0$ is a typed refusal before any fold begins. |\n| 525 | `test_sign_applied_before_reduction` | exact sum | $\\sigma_i \\in \\{+1,-1\\}$ is applied to the numerator, and gcd reduction leaves a positive denominator. |\n| 526 | `test_unreduced_fractions_canonicalize` | exact sum | $2/4 + 1/2$ reduces to the same $(n_{\\text{net}}, d_{\\text{net}})$ as $1/2 + 1/2$. |\n| 527 | `test_wdw_constraint_vanishes_iff_numerator_zero` | wdwnf | the wheeler�dewitt constraint $h_{\\perp}$ is recorded as zero exactly when the folded numerator is zero. |\n| 528 | `test_positive_wdw_residual_refuses_preserve` | wdwnf | a folded residual of $1/2$ routes away from `preserve`. |\n| 529 | `test_momentum_constraint_uses_same_rational_fold` | l1 closure | the spatial diffeomorphism constraint uses the same signed rational fold as $h_{\\perp}$. |\n| 530 | `test_four_term_mixed_sign_cancellation` | exact sum | $1/3 + 1/6 - 1/2 + 0/1$ yields $n_{\\text{net}} = 0$. |\n| 531 | `test_zero_numerator_is_exact_zero` | exact sum | $0/5$ is exact zero and stays exact zero inside a larger fold. |\n| 532 | `test_negative_denominator_normalized` | exact sum | input $-1/-2$ is stored as $+1/2$ with $d > 0$. input $1/-2$ is stored as $-1/2$ with $d > 0$. |\n| 533 | `test_gcd_reduction_is_deterministic` | exact sum | two calls on the same multiset of fractions return identical $(n_{\\text{net}}, d_{\\text{net}})$. |\n| 534 | `test_rational_fold_order_independence` | exact sum | every permutation of a fixed list of signed fractions returns the same reduced sum. |\n| 535 | `test_float_constraint_payload_refused` | exact sum | a float payload such as `0.16666666666666666` is a typed refusal. the fold accepts only integer numerators and denominators. |\n\n---\n\n## 27. tranche 28: null totality, boolean identity, residual zero & candidate sets (tests 536�555)\n\n**status:** planned. no module and no execution receipt. \ntarget module: `omega_engine_governance/tests/normal_forms/test_tranche28_null_totality_and_guard_identity.py` \naligned contracts: `nf.evidence.certificate`, `nf.coda.eqnf`, `nf.runtime.zfnf`, `normal_form_contract_schema.yaml`\n\nboolean fields use `type(val) is bool`. sql disagreement uses `is distinct from`. guard $g_3$ requires `residual_mass == 0`. guard $g_5$ requires set equality of candidate identifiers.\n\n| # | test identifier | category | target invariant & scope |\n|---|---|---|---|\n| 536 | `test_bool_field_rejects_int_one` | boolean identity | a schema boolean rejects integer `1`. the mutation is the witness. |\n| 537 | `test_bool_field_rejects_int_zero` | boolean identity | a schema boolean rejects integer `0`. the mutation is the witness. |\n| 538 | `test_bool_field_accepts_true_and_false` | boolean identity | `true` and `false` pass a schema boolean check, and their python types are `bool`. |\n| 539 | `test_conditional_field_accepts_bool_or_conditional` | boolean identity | a field whose schema is boolean-or-`"conditional"` accepts `true`, `false`, and the string `"conditional"`. |\n| 540 | `test_conditional_field_rejects_other_strings` | boolean identity | the same field refuses `"true"`, `"false"`, `"yes"`, and the empty string. |\n| 541 | `test_null_preflight_flags_null_fact_value` | null totality | a totality preflight returns the row whose protected fact value is null. |\n| 542 | `test_null_preflight_flags_null_global_verdict` | null totality | a totality preflight returns the row whose `global_verdict` is null. |\n| 543 | `test_null_preflight_flags_null_local_product` | null totality | a totality preflight returns the row whose `local_product` is null. |\n| 544 | `test_sql_inequality_misses_null_disagreement` | null totality | `global_verdict <> local_product` returns no row when one side is null. the same row is returned by `is distinct from`. |\n| 545 | `test_is_distinct_from_detects_null_versus_value` | null totality | `null is distinct from 1` and `0 is distinct from null` both select the disagreeing row. |\n| 546 | `test_is_distinct_from_detects_value_mismatch` | null totality | two non-null unequal verdicts are selected by `is distinct from`. |\n| 547 | `test_is_distinct_from_accepts_equal_pair` | null totality | two equal non-null verdicts are absent from the `is distinct from` result. |\n| 548 | `test_zero_residual_guard_requires_exact_zero` | residual gate | guard $g_3$ passes only when `residual_mass == 0` as an exact rational. |\n| 549 | `test_half_residual_fails_under_positive_tolerance` | residual gate | residual mass $1/2$ fails $g_3$ when a caller supplies a positive numeric tolerance. |\n| 550 | `test_certificate_verify_is_executed` | certificate | an attached distance certificate is accepted only after `certificate.verify()` returns success. |\n| 551 | `test_certificate_distance_equals_residual_mass` | certificate | the validator requires `certificate.distance == residual_mass` on the exact rational. |\n| 552 | `test_contradictory_certificate_refuses` | certificate | a certificate whose distance differs from the computed residual mass produces an explicit refusal. |\n| 553 | `test_exhaustive_guard_requires_set_equality` | exhaustiveness | guard $g_5$ passes when the checked candidate-id set equals `packet.evaluator_class_e` and the lengths are equal. |\n| 554 | `test_duplicate_checks_fail_set_exhaustiveness` | exhaustiveness | a count `candidates_checked >= candidates_declared` with a repeated id and a missing declared id fails $g_5$. |\n| 555 | `test_extraneous_candidate_id_fails_exhaustiveness` | exhaustiveness | a checked id absent from the packet fails $g_5$ even when the counts match. |\n\n---\n\n## 28. tranche 29: loss-ledger trigger registry (tests 556�575)\n\n**status:** planned. no module and no execution receipt. \ntarget module: `omega_engine_governance/tests/normal_forms/test_tranche29_loss_ledger_trigger_registry.py` \naligned contracts: `nf.evidence.loss_ledger`, `nf.compilation.cpnf`, `nf.transport.gtmur`, `nf.motion.flow_control`, `nf.representation.gnf`, `nf.motion.locality_lrb`, `nf.epistemic.location`, `nf.epistemic.enf`\n\nthe closed registry in `normal_form_contract_schema.yaml` is the only source of trigger ids. `loss_ledger_required: conditional` carries one of those ids.\n\n| # | test identifier | category | target invariant & scope |\n|---|---|---|---|\n| 556 | `test_conditional_obligation_requires_trigger_id` | registry | `loss_ledger_required: conditional` with `loss_ledger_trigger_id: null` is a schema refusal. |\n| 557 | `test_conditional_prose_without_trigger_id_refused` | registry | a free-text loss commentary and a null trigger id is a schema refusal. |\n| 558 | `test_trigger_id_cpnf_lossy_compilation_lowering_resolves` | registry | `cpnf.lossy_compilation_lowering` resolves to the closed registry entry for lossy compilation lowering. |\n| 559 | `test_trigger_id_gtmur_unmapped_field_drop_resolves` | registry | `gtmur.unmapped_field_drop` resolves to the closed registry entry for unmapped field drop. |\n| 560 | `test_trigger_id_flow_control_buffer_drop_resolves` | registry | `flow_control.buffer_drop` resolves to the closed registry entry for buffer drop. |\n| 561 | `test_trigger_id_gnf_hyperedge_projection_loss_resolves` | registry | `gnf.hyperedge_projection_loss` resolves to the closed registry entry for hyperedge projection loss. |\n| 562 | `test_trigger_id_locality_lrb_tail_truncation_resolves` | registry | `locality_lrb.tail_truncation` resolves to the closed registry entry for lieb�robinson tail truncation. |\n| 563 | `test_trigger_id_epistemic_location_partition_divergence_resolves` | registry | `epistemic_location.partition_divergence` resolves to the closed registry entry for partition divergence. |\n| 564 | `test_trigger_id_enf_lossy_epistemic_transition_resolves` | registry | `enf.lossy_epistemic_transition` resolves to the closed registry entry for lossy epistemic transition. |\n| 565 | `test_unregistered_trigger_id_refused` | registry | `loss_ledger_trigger_id: "custom.operator_note"` is a schema refusal. |\n| 566 | `test_registry_keys_equal_schema_enum` | registry | the keys of `loss_ledger_trigger_registry` equal the non-null enum of `loss_ledger_trigger_id`. |\n| 567 | `test_required_false_permits_null_trigger` | registry | `loss_ledger_required: false` with a null trigger id passes the trigger check. |\n| 568 | `test_required_true_demands_ledger_entries` | ledger payload | `loss_ledger_required: true` with an empty entry list is a refusal. |\n| 569 | `test_required_true_rejects_missing_ledger_object` | ledger payload | `loss_ledger_required: true` with no ledger object is a refusal. |\n| 570 | `test_loss_ledger_required_rejects_int_zero_and_one` | boolean identity | integer `0` and integer `1` fail the `loss_ledger_required` type check. accepted values are `true`, `false`, and `"conditional"`. |\n| 571 | `test_trigger_fires_only_for_its_event` | predicate | `flow_control.buffer_drop` stays inactive on a compilation-lowering event, and `cpnf.lossy_compilation_lowering` stays inactive on a buffer-drop event. |\n| 572 | `test_inactive_trigger_omits_ledger` | predicate | when `loss_ledger_required` is `conditional` and the registered predicate is false, a missing ledger passes. |\n| 573 | `test_active_trigger_demands_ledger` | predicate | when the same contract\'s predicate is true, a missing ledger is a refusal. |\n| 574 | `test_sealed_ledger_digest_tracks_erased_attributes` | ledger payload | changing `erased_attributes` changes the sealed ledger digest. |\n| 575 | `test_parser_preserves_declared_trigger_id` | registry | parsing a contract with `loss_ledger_required: conditional` and `loss_ledger_trigger_id: gtmur.unmapped_field_drop` returns that id unchanged. a missing id stays null, and the conditional check then refuses. |\n\n---\n\n## 29. tranche 30: pseudometric separation & quotient factors (tests 576�595)\n\n**status:** planned. no module and no execution receipt. \ntarget module: `omega_engine_governance/tests/normal_forms/test_tranche30_pseudometric_and_quotient_factors.py` \naligned contracts: `nf.epistemic.odnf`, `nf.coda.eqnf`, `nf.transport.gtmur`\n\ndistance zero is a pseudometric fact. point equality is claimed only after a declared separation axiom. quotient distance is the $l_1$ distance on the quotient, and a factor through the quotient is unique on the declared kernel.\n\n| # | test identifier | category | target invariant & scope |\n|---|---|---|---|\n| 576 | `test_pseudometric_zero_keeps_distinct_ids` | pseudometric | two observer states with $d(o_1, o_2) = 0$ retain distinct identifiers when no separation axiom is declared. |\n| 577 | `test_equality_requires_separation_axiom` | pseudometric | a collapse of those states to one point is refused until the contract declares a separation axiom. |\n| 578 | `test_odnf_zero_divergence_routes_to_abstain` | odnf | odnf distance zero, with separation undeclared, routes to `abstain`. |\n| 579 | `test_positive_pseudometric_blocks_collapse` | pseudometric | $d(o_1, o_2) = 1/2$ refuses a collapse receipt. |\n| 580 | `test_pseudometric_nonnegative` | pseudometric | every evaluated pair returns $d \\ge 0$ as an exact rational. |\n| 581 | `test_pseudometric_symmetric` | pseudometric | $d(a, b) = d(b, a)$ on the fixture pairs. |\n| 582 | `test_pseudometric_triangle_inequality` | pseudometric | $d(a, c) \\le d(a, b) + d(b, c)$ on the fixture triple, with exact rational addition. |\n| 583 | `test_separation_axiom_makes_zero_into_equality` | pseudometric | after the contract declares separation, $d(a, b) = 0$ yields $a = b$ in the quotient of the pseudometric. |\n| 584 | `test_l1_quotient_distance_is_the_reported_distance` | quotient | the reported distance is the $l_1$ distance between quotient classes, computed from class representatives. |\n| 585 | `test_kernel_inclusion_checked_before_factor` | quotient | a map factors through the quotient only when the declared kernel sits inside the map\'s kernel. |\n| 586 | `test_factor_missing_a_kernel_pair_refused` | quotient | a candidate factor that separates two kernel-equivalent representatives is refused. |\n| 587 | `test_universal_factor_unique_on_classes` | quotient | two factors that agree on every quotient class are recorded as the same factor. |\n| 588 | `test_second_factor_disagreement_refused` | quotient | a second factor that disagrees on one class is refused as a universal factor. |\n| 589 | `test_quotient_identifies_only_the_declared_kernel` | quotient | representatives outside the declared kernel remain distinct classes. |\n| 590 | `test_nontrivial_class_is_not_a_point_equality_claim` | quotient | a class with two representatives is reported as one quotient point and two carrier points. |\n| 591 | `test_eqnf_unverified_quotient_refuses_preserve` | eqnf | an eqnf quotient whose verification status is `absent` refuses `preserve`. |\n| 592 | `test_gtmur_unmapped_field_opens_loss_ledger` | gtmur | dropping an unmapped field opens a loss-ledger entry bound to `gtmur.unmapped_field_drop`. |\n| 593 | `test_gtmur_mapped_roundtrip_preserves_payload` | gtmur | a payload whose fields are all in the declared map round-trips to the same canonical bytes. |\n| 594 | `test_certificate_does_not_supply_separation` | pseudometric | attaching a distance certificate leaves the separation axiom unset. zero distance still withholds point equality. |\n| 595 | `test_two_representatives_at_quotient_distance_zero` | quotient | two distinct representatives of one class have quotient distance zero and unequal carrier ids. |\n\n---\n\n## 30. tranche 31: operational pipeline & terminal routes (tests 596�615)\n\n**status:** planned. no module and no execution receipt. \ntarget module: `omega_engine_governance/tests/normal_forms/test_tranche31_operational_pipeline_and_terminal_routes.py` \naligned contracts: `nf.epistemic.authority`, `nf.evidence.certificate`, `nf.evidence.ddanf`, `nf.coda.eqnf`\n\nthe operational harness runs `route`, then `descend`, then `verify`, then `terminalize`, and stops at the first refusal. `guardevidence` is read from that trace. caller-supplied booleans are `guardattestations` and stay on the attestation side of the boundary.\n\n| # | test identifier | category | target invariant & scope |\n|---|---|---|---|\n| 596 | `test_stages_run_in_route_descend_verify_terminalize_order` | pipeline | a clean fixture records the four stage names in that order in the serialized trace. |\n| 597 | `test_route_refusal_skips_later_stages` | pipeline | a refusal from `route` leaves `descend`, `verify`, and `terminalize` absent from the trace. |\n| 598 | `test_descend_refusal_skips_verify_and_terminalize` | pipeline | a refusal from `descend` leaves `verify` and `terminalize` absent from the trace. |\n| 599 | `test_verify_refusal_skips_terminalize` | pipeline | a refusal from `verify` leaves `terminalize` absent from the trace. |\n| 600 | `test_trace_lists_each_executed_stage` | pipeline | the trace entries are exactly the stages that ran, each with its input digest and output digest. |\n| 601 | `test_trace_sha256_binds_canonical_json` | pipeline | the receipt digest equals the sha-256 of the rfc 8785 canonical json of the trace. |\n| 602 | `test_mutated_trace_byte_fails_digest` | pipeline | flipping one byte of the canonical trace makes the stored digest fail recomputation. |\n| 603 | `test_guard_evidence_is_read_from_the_trace` | evidence | `guardevidence` fields match the stage outputs in the trace and are absent when the stage did not run. |\n| 604 | `test_caller_true_without_trace_refuses_preserve` | attestation | a caller attestation `verified: true` with no trace refuses `preserve`. |\n| 605 | `test_attestation_input_type_is_guard_attestations` | attestation | the policy-evaluator entry point accepts `guardattestations` and refuses a payload typed as `guardevidence` when no trace is attached. |\n| 606 | `test_policy_evaluator_receipt_names_attestation_boundary` | attestation | the attestation receipt states that the evaluator judges caller-supplied attestations and records no pipeline execution. |\n| 607 | `test_observed_no_mixed_fiber_routes_to_abstain` | terminal route | evidence label `observednomixedfiberincorpus` routes to `abstain`. |\n| 608 | `test_claimed_view_determinate_routes_to_abstain` | terminal route | evidence label `claimedviewdeterminate` routes to `abstain`. |\n| 609 | `test_preserve_requires_machine_checked_and_verifier` | terminal route | `preserve` is emitted when `verification_status` is `machine_checked` and `verifier_required` is `true`. |\n| 610 | `test_preserve_refused_when_verifier_required_is_false` | terminal route | `verification_status: machine_checked` with `verifier_required: false` refuses `preserve`. |\n| 611 | `test_preserve_refused_when_verification_status_absent` | terminal route | `verifier_required: true` with `verification_status: absent` refuses `preserve`. |\n| 612 | `test_count_only_coverage_is_labeled_count_coverage` | exhaustiveness | a packet that supplies counts and no candidate ids is labeled count coverage. |\n| 613 | `test_count_coverage_does_not_emit_exhaustive` | exhaustiveness | the count-coverage label is refused as an `exhaustive` guard result. |\n| 614 | `test_replay_of_trace_reproduces_terminal` | replay | re-executing the stored trace yields the same terminal and the same sha-256 digest. |\n| 615 | `test_first_refusal_is_the_recorded_terminal` | pipeline | when `descend` refuses, the recorded terminal is that refusal, and later stage names do not appear. |\n\n---\n' : Found legacy gtmur in C:\Users\a343o\source\repos\simplex-normal-forms\normal_forms\planned-tests-516-615.md + +tests\test_normal_forms.py:57: AssertionError +=========================== short test summary info =========================== +FAILED tests/test_normal_forms.py::TestSimplexNormalForms::test_zero_gtmur_across_contracts_wiki_and_code +1 failed, 231 passed in 37.50s +Frontend component parsing and zero-step chase rendering passed. diff --git a/scripts/browser_smoke.cjs b/scripts/browser_smoke.cjs index b26fa96..a8eaf4a 100644 --- a/scripts/browser_smoke.cjs +++ b/scripts/browser_smoke.cjs @@ -115,6 +115,10 @@ async function copy(id) { page.on('response', r => { if (r.status() >= 400) report.http_errors.push({ url: r.url(), status: r.status() }); }); page.on('dialog', async dialog => { report.page_errors.push(`Dialog: ${dialog.message()}`); await dialog.dismiss(); }); await step('Application identity, assets and initial rendering', async () => { + const front = await page.goto(base + '/', { waitUntil: 'networkidle', timeout: 120000 }); + assert.equal(front.status(), 200); + assert.match(await page.title(), /Simplex Normal Forms Studio/); + await page.waitForFunction(() => document.querySelector('#relational-chase-status').innerText.includes('Lossless')); const r = await page.goto(base + '/studio/', { waitUntil: 'networkidle', timeout: 120000 }); assert.equal(r.status(), 200); assert.match(await page.title(), /Simplex Normal Forms Studio/); @@ -125,7 +129,7 @@ async function copy(id) { assert.equal(health.status(), 200); report.health = await health.json(); assert.equal(report.health.service, 'smplxnf-studio'); - for (const [urlPath, local] of [['/studio/', 'web/templates/index.html'], ['/', 'web/templates/overview.html'], ['/static/app.js', 'web/static/app.js'], ['/static/style.css', 'web/static/style.css']]) { + for (const [urlPath, local] of [['/', 'web/templates/front.html'], ['/', 'web/templates/overview.html'], ['/studio/', 'web/templates/index.html'], ['/static/app.js', 'web/static/app.js'], ['/static/style.css', 'web/static/style.css']]) { const response = await context.request.get(base + urlPath); assert.equal(response.status(), 200); const bytes = await response.body(); @@ -246,6 +250,14 @@ async function copy(id) { return layout(`${width}px-${view}-layout`); }); } + await page.goto(base + '/', { waitUntil: 'networkidle', timeout: 120000 }); + await page.waitForFunction(() => document.querySelector('#relational-chase-status').innerText.includes('Lossless')); + for (const width of [1280, 768, 390, 320]) { + await step(`${width}px layout: front`, async () => { + await page.setViewportSize({ width, height: width < 768 ? 844 : 900 }); + return layout(`${width}px-front-layout`); + }); + } await step('Browser console, runtime and network errors', async () => { assert.deepEqual(report.page_errors, []); assert.deepEqual(report.failed_requests, []); diff --git a/tests/test_frontend.cjs b/tests/test_frontend.cjs index ee8ba11..25e2ccf 100644 --- a/tests/test_frontend.cjs +++ b/tests/test_frontend.cjs @@ -40,6 +40,10 @@ vm.runInContext(fs.readFileSync(path.join(__dirname, '../web/static/app.js'), 'u assert.deepEqual(submitted.custom_components, [['A', 'B'], ['B', 'C']]); assert.match(getElement('relational-chase-status').innerHTML, /Lossy Join/); assert.match(getElement('chase-witness-box').innerHTML, /a_C/); + assert.match( + getElement('chase-witness-box').innerHTML, + /this row is in the join of the pieces but not in the original/ + ); assert.match(getElement('chase-steps-tbody').innerHTML, /no distinguished row/); assert.equal(getElement('btn-run-relational').disabled, false); } diff --git a/tests/test_relational_properties.py b/tests/test_relational_properties.py new file mode 100644 index 0000000..15ab586 --- /dev/null +++ b/tests/test_relational_properties.py @@ -0,0 +1,329 @@ +"""Property-based correctness tests for classical relational dependency algebra. + +Checks over seeded random functional-dependency sets on at most 6 attributes: +1. Attribute closure and candidate-key enumeration agree with brute force over all attribute subsets. +2. Bernstein 3NF synthesis is dependency-preserving and lossless (chase reaches a distinguished row). +3. Tsou-Fischer BCNF decomposition is lossless and every output table is in BCNF. +4. Chase lossy/lossless verdict agrees with actual natural join of projections on small instances, + and when lossy, spurious_tuple_witness appears in the natural join of projections of the chase + counterexample instance and not in the original relation. +""" + +from __future__ import annotations + +from itertools import combinations, product +import random +from typing import Dict, FrozenSet, Iterable, List, Sequence, Set, Tuple + +from normal_forms.domain.relational import ( + FunctionalDependency, + RelationalSchema, + check_bcnf, + chase_join_dependency, + compute_attribute_closure, +) +from normal_forms.domain.relational_advanced import ( + decompose_bcnf_tree, + project_functional_dependencies, + synthesize_3nf_bernstein, +) + + +def _brute_force_closure( + attrs: Sequence[str], + seed_subset: Iterable[str], + fds: Sequence[FunctionalDependency], +) -> FrozenSet[str]: + """Computes X^+ by checking all 2^|U| Boolean valuations satisfying F.""" + attr_list = sorted(attrs) + seed_set = set(seed_subset) + in_closure = set(attr_list) + + for bits in product((0, 1), repeat=len(attr_list)): + valuation = dict(zip(attr_list, bits)) + if not all(valuation[a] == 1 for a in seed_set): + continue + satisfies_fds = True + for fd in fds: + if all(valuation[a] == 1 for a in fd.determinant): + if not all(valuation[b] == 1 for b in fd.dependent): + satisfies_fds = False + break + if not satisfies_fds: + continue + for a in list(in_closure): + if valuation[a] == 0: + in_closure.remove(a) + + return frozenset(in_closure) + + +def _brute_force_candidate_keys( + attrs: Sequence[str], + fds: Sequence[FunctionalDependency], +) -> Set[FrozenSet[str]]: + """Enumerates all minimal superkeys by checking all non-empty subsets of U.""" + attr_list = sorted(attrs) + all_set = frozenset(attr_list) + superkeys: List[FrozenSet[str]] = [] + + for r in range(1, len(attr_list) + 1): + for comb in combinations(attr_list, r): + sub = frozenset(comb) + if _brute_force_closure(attr_list, sub, fds) == all_set: + superkeys.append(sub) + + minimal: Set[FrozenSet[str]] = set() + for sk in superkeys: + if not any(other < sk for other in superkeys): + minimal.add(sk) + return minimal + + +def _project_relation( + rows: Sequence[Dict[str, str]], + comp: Iterable[str], +) -> List[Dict[str, str]]: + cols = sorted(comp) + seen: Set[Tuple[str, ...]] = set() + out: List[Dict[str, str]] = [] + for row in rows: + key = tuple(row[c] for c in cols) + if key not in seen: + seen.add(key) + out.append({c: row[c] for c in cols}) + return out + + +def _natural_join( + left: Sequence[Dict[str, str]], + right: Sequence[Dict[str, str]], +) -> List[Dict[str, str]]: + if not left: + return [] + if not right: + return [] + left_cols = set(left[0].keys()) + right_cols = set(right[0].keys()) + shared = sorted(left_cols & right_cols) + all_cols = sorted(left_cols | right_cols) + + seen: Set[Tuple[str, ...]] = set() + joined: List[Dict[str, str]] = [] + for r1 in left: + for r2 in right: + if all(r1[c] == r2[c] for c in shared): + merged = {**r1, **r2} + tup = tuple(merged[c] for c in all_cols) + if tup not in seen: + seen.add(tup) + joined.append({c: merged[c] for c in all_cols}) + return joined + + +def _join_all_projections( + rows: Sequence[Dict[str, str]], + components: Sequence[Iterable[str]], +) -> List[Dict[str, str]]: + projections = [_project_relation(rows, comp) for comp in components] + if not projections: + return [] + acc = projections[0] + for proj in projections[1:]: + acc = _natural_join(acc, proj) + return acc + + +def _relation_satisfies_fds( + rows: Sequence[Dict[str, str]], + fds: Iterable[FunctionalDependency], +) -> bool: + for fd in fds: + det_cols = sorted(fd.determinant) + dep_cols = sorted(fd.dependent) + for i in range(len(rows)): + for j in range(i + 1, len(rows)): + if all(rows[i][c] == rows[j][c] for c in det_cols): + if not all(rows[i][c] == rows[j][c] for c in dep_cols): + return False + return True + + +def _random_schema(rng: random.Random) -> RelationalSchema: + n_attrs = rng.randint(2, 6) + attrs = [chr(ord("A") + i) for i in range(n_attrs)] + n_fds = rng.randint(1, 6) + fds: Set[FunctionalDependency] = set() + for _ in range(n_fds): + det_size = rng.randint(1, max(1, n_attrs - 1)) + det = frozenset(rng.sample(attrs, det_size)) + remaining = [a for a in attrs if a not in det] + if not remaining: + dep = frozenset(rng.sample(attrs, 1)) + else: + dep_size = rng.randint(1, min(2, len(remaining))) + dep = frozenset(rng.sample(remaining, dep_size)) + fds.add(FunctionalDependency(det, dep)) + return RelationalSchema(attributes=frozenset(attrs), dependencies=frozenset(fds)) + + +def test_closure_and_candidate_keys_match_brute_force() -> None: + rng = random.Random(20261105) + for iteration in range(150): + schema = _random_schema(rng) + attrs = sorted(schema.attributes) + fds = list(schema.dependencies) + + for r in range(len(attrs) + 1): + for comb in combinations(attrs, r): + got = compute_attribute_closure(comb, fds) + expected = _brute_force_closure(attrs, comb, fds) + assert got == expected, ( + f"Closure mismatch at seed=20261105 iter={iteration} " + f"subset={comb} fds={fds}: got={got}, expected={expected}" + ) + + got_keys = set(schema.candidate_keys()) + expected_keys = _brute_force_candidate_keys(attrs, fds) + assert got_keys == expected_keys, ( + f"Candidate keys mismatch at seed=20261105 iter={iteration} " + f"fds={fds}: got={got_keys}, expected={expected_keys}" + ) + + +def test_3nf_synthesis_is_dependency_preserving_and_lossless() -> None: + rng = random.Random(20261106) + for iteration in range(150): + schema = _random_schema(rng) + decomp = synthesize_3nf_bernstein(schema) + assert len(decomp) >= 1 + assert frozenset().union(*decomp) == schema.attributes + + # Dependency preservation: every input FD is implied by the union of FDs projected onto the 3NF tables + projected_union: List[FunctionalDependency] = [] + for comp in decomp: + projected_union.extend(project_functional_dependencies(schema.dependencies, comp)) + + for fd in schema.dependencies: + closure = compute_attribute_closure(fd.determinant, projected_union) + assert fd.dependent.issubset(closure), ( + f"3NF synthesis lost FD {fd} at seed=20261106 iter={iteration}: " + f"decomp={decomp}, projected_union={projected_union}" + ) + + # Lossless join: when decomposed into >=2 tables, chase reaches a distinguished row + if len(decomp) >= 2: + chase = chase_join_dependency( + heading=sorted(schema.attributes), + dependencies=schema.dependencies, + components=decomp, + ) + assert chase.is_implied is True, ( + f"3NF synthesis is not lossless at seed=20261106 iter={iteration}: " + f"schema={schema}, decomp={decomp}, chase={chase}" + ) + assert chase.distinguished_row_index is not None + dist_row = chase.final_tableau[chase.distinguished_row_index] + assert all(dist_row[a] == f"a_{a}" for a in schema.attributes) + + +def test_bcnf_decomposition_is_lossless_and_in_bcnf() -> None: + rng = random.Random(20261107) + for iteration in range(150): + schema = _random_schema(rng) + leaves = decompose_bcnf_tree(schema) + assert len(leaves) >= 1 + assert frozenset().union(*(s.attributes for s in leaves)) == schema.attributes + + for leaf in leaves: + ok_bcnf, reason = check_bcnf(leaf) + assert ok_bcnf is True, ( + f"BCNF leaf failed check_bcnf at seed=20261107 iter={iteration}: " + f"leaf={leaf}, reason={reason}" + ) + + if len(leaves) >= 2: + chase = chase_join_dependency( + heading=sorted(schema.attributes), + dependencies=schema.dependencies, + components=[s.attributes for s in leaves], + ) + assert chase.is_implied is True, ( + f"BCNF decomposition is lossy at seed=20261107 iter={iteration}: " + f"schema={schema}, leaves={leaves}, chase={chase}" + ) + assert chase.distinguished_row_index is not None + + +def test_chase_verdict_agrees_with_natural_join_and_spurious_tuple_witness() -> None: + rng = random.Random(20261108) + lossy_count = 0 + lossless_count = 0 + + for iteration in range(150): + schema = _random_schema(rng) + attrs = sorted(schema.attributes) + if len(attrs) < 3: + continue + + # Build a random 2-way or 3-way decomposition covering all attributes + k = rng.randint(1, len(attrs) - 1) + part1 = set(attrs[:k]) + part2 = set(attrs[k:]) + overlap = rng.sample(attrs, rng.randint(1, len(attrs) - 1)) + comp1 = frozenset(part1 | set(overlap[:1])) + comp2 = frozenset(part2 | set(overlap)) + if comp1 == schema.attributes or comp2 == schema.attributes: + continue + components = [comp1, comp2] + + chase = chase_join_dependency( + heading=attrs, + dependencies=schema.dependencies, + components=components, + ) + assert chase.is_implied in (True, False) + + # The final chase tableau is a relation over attrs + final_rows = [{c: row[c] for c in attrs} for row in chase.final_tableau] + joined_rows = _join_all_projections(final_rows, components) + + if chase.is_implied is False: + lossy_count += 1 + assert _relation_satisfies_fds(final_rows, schema.dependencies), ( + f"Lossy counterexample tableau violates FDs at iter={iteration}: {final_rows}" + ) + witness = chase.spurious_tuple_witness + assert witness is not None, "Lossy chase must return a spurious_tuple_witness" + witness_clean = {c: witness[c] for c in attrs} + assert witness_clean not in final_rows, ( + f"Spurious witness {witness_clean} was already in the original relation {final_rows}" + ) + assert witness_clean in joined_rows, ( + f"Spurious witness {witness_clean} did not appear in the join of projections {joined_rows}" + ) + else: + lossless_count += 1 + assert chase.spurious_tuple_witness is None + dist_witness = {c: f"a_{c}" for c in attrs} + assert dist_witness in final_rows + # Run chase to full fixpoint (early_exit=False) to get an FD-valid instance I + full_chase = chase_join_dependency( + heading=attrs, + dependencies=schema.dependencies, + components=components, + early_exit=False, + ) + valid_instance = _project_relation( + [{c: row[c] for c in attrs} for row in full_chase.final_tableau], + attrs, + ) + assert _relation_satisfies_fds(valid_instance, schema.dependencies) + rejoined = _join_all_projections(valid_instance, components) + assert len(rejoined) == len(valid_instance) and all( + r in valid_instance for r in rejoined + ), f"Lossless decomposition produced spurious tuples on {valid_instance}: {rejoined}" + + assert lossy_count >= 10, f"Expected at least 10 lossy cases, got {lossy_count}" + assert lossless_count >= 10, f"Expected at least 10 lossless cases, got {lossless_count}" + diff --git a/web/app.py b/web/app.py index 0b766db..e7a99a9 100644 --- a/web/app.py +++ b/web/app.py @@ -42,6 +42,7 @@ from normal_forms.domain.relational_advanced import ( check_eknf, decompose_bcnf_tree, + project_functional_dependencies, synthesize_3nf_bernstein, ) from normal_forms.domain.bqnf_validator import ( @@ -375,7 +376,9 @@ async def normalize_relational_schema(payload: RelationalNormalizeRequest) -> Di synthesized_raw = synthesize_3nf_bernstein(schema) synthesized_3nf: List[Dict[str, Any]] = [] for idx, sub_attrs in enumerate(synthesized_raw, 1): - sub_keys = [sorted(k) for k in cand_keys if frozenset(k).issubset(sub_attrs)] + proj_fds = frozenset(project_functional_dependencies(schema.dependencies, sub_attrs)) + sub_schema = RelationalSchema(attributes=sub_attrs, dependencies=proj_fds) + sub_keys = [sorted(k) for k in sub_schema.candidate_keys()] synthesized_3nf.append({ "table_name": f"rel_3nf_table_{idx}", "attributes": sorted(sub_attrs), @@ -405,8 +408,20 @@ async def normalize_relational_schema(payload: RelationalNormalizeRequest) -> Di components=components_to_chase, ) + sim_tab = [dict(r) for r in chase_res.initial_tableau] steps_data: List[Dict[str, Any]] = [] for s in chase_res.steps: + changed_cells: List[Dict[str, Any]] = [] + for r_idx, row in enumerate(sim_tab): + for col in chase_res.heading: + if row.get(col) == s.old_symbol: + row[col] = s.new_symbol + changed_cells.append({ + "row": r_idx + 1, + "column": col, + "from": s.old_symbol, + "to": s.new_symbol, + }) steps_data.append({ "step_number": s.step_number, "fd": str(s.fd_applied), @@ -414,15 +429,110 @@ async def normalize_relational_schema(payload: RelationalNormalizeRequest) -> Di "attribute_equated": s.attribute_equated, "old_symbol": s.old_symbol, "new_symbol": s.new_symbol, + "changed_cells": changed_cells, }) - # Generate SQL DDL - sql_ddl_statements: List[str] = [] + spurious_explanation = ( + "this row is in the join of the pieces but not in the original" + if (not chase_res.is_implied and chase_res.spurious_tuple_witness) + else None + ) + + # Generate SQL DDL for PostgreSQL and SQL Server + pg_statements: List[str] = ["-- Target 1: PostgreSQL DDL"] + mssql_statements: List[str] = [ + "-- Target 2: SQL Server DDL", + "-- Note (MAX aggregate): A SQL Server indexed view (WITH SCHEMABINDING) cannot include MAX() or MIN() because deleting the current maximum row cannot be repaired from the stored scalar alone without rescanning the group; maintain a sorted list of values per group instead.", + ] + + # Topologically order parent tables before child tables that reference them via foreign keys + table_by_name = {t["table_name"]: t for t in synthesized_3nf} + fk_targets_by_table: Dict[str, List[Dict[str, Any]]] = {t["table_name"]: [] for t in synthesized_3nf} for table in synthesized_3nf: - cols = ", ".join(f'"{col}" TEXT' for col in table["attributes"]) - pk_cols = ", ".join(f'"{c}"' for c in table["candidate_keys"][0]) if table["candidate_keys"] else "" - pk_clause = f", PRIMARY KEY ({pk_cols})" if pk_cols else "" - sql_ddl_statements.append(f'CREATE TABLE "{table["table_name"]}" ({cols}{pk_clause});') + tname = table["table_name"] + tattrs_set = set(table["attributes"]) + pk_set = set(table["candidate_keys"][0] if table["candidate_keys"] else table["attributes"]) + for other in synthesized_3nf: + oname = other["table_name"] + if oname == tname or not other["candidate_keys"]: + continue + other_pk_set = set(other["candidate_keys"][0]) + if other_pk_set.issubset(tattrs_set) and (other_pk_set != pk_set or oname < tname): + fk_targets_by_table[tname].append(other) + + def _table_sort_key(t: Dict[str, Any]) -> Tuple[int, int, str]: + return ( + len(t["candidate_keys"][0]) if t["candidate_keys"] else 99, + len(t["attributes"]), + t["table_name"], + ) + + ordered_tables: List[Dict[str, Any]] = [] + placed_names: set[str] = set() + remaining = sorted(synthesized_3nf, key=_table_sort_key) + while remaining: + ready = [ + t for t in remaining + if all(dep["table_name"] in placed_names for dep in fk_targets_by_table[t["table_name"]]) + ] + pick = ready[0] if ready else remaining[0] + ordered_tables.append(pick) + placed_names.add(pick["table_name"]) + remaining = [t for t in remaining if t["table_name"] != pick["table_name"]] + + created_tables: set[str] = set() + for table in ordered_tables: + tname = table["table_name"] + tattrs = table["attributes"] + pk = table["candidate_keys"][0] if table["candidate_keys"] else tattrs + secondary_keys = table["candidate_keys"][1:] if len(table["candidate_keys"]) > 1 else [] + not_null_cols = ( + {col for key in table["candidate_keys"] for col in key} + if table["candidate_keys"] + else set(tattrs) + ) + + # Foreign keys to already-created 3NF parent tables whose PK is a subset of this table's attributes + fk_clauses_pg: List[str] = [] + fk_clauses_ms: List[str] = [] + for other in fk_targets_by_table[tname]: + if other["table_name"] not in created_tables: + continue + other_pk = other["candidate_keys"][0] + pg_cols = ", ".join(f'"{c}"' for c in other_pk) + ms_cols = ", ".join(f"[{c}]" for c in other_pk) + fk_clauses_pg.append(f'FOREIGN KEY ({pg_cols}) REFERENCES "{other["table_name"]}" ({pg_cols})') + fk_clauses_ms.append(f"FOREIGN KEY ({ms_cols}) REFERENCES [{other['table_name']}] ({ms_cols})") + + pg_col_defs = [ + f'"{col}" TEXT{" NOT NULL" if col in not_null_cols else ""}' + for col in tattrs + ] + ms_col_defs = [ + f'[{col}] NVARCHAR(128){" NOT NULL" if col in not_null_cols else ""}' + for col in tattrs + ] + + pg_pk = f'PRIMARY KEY ({", ".join(f"{chr(34)}{c}{chr(34)}" for c in pk)})' + ms_pk = f'PRIMARY KEY ({", ".join(f"[{c}]" for c in pk)})' + + pg_uniques = [ + f'UNIQUE ({", ".join(f"{chr(34)}{c}{chr(34)}" for c in uk)})' + for uk in secondary_keys + ] + ms_uniques = [ + f'UNIQUE ({", ".join(f"[{c}]" for c in uk)})' + for uk in secondary_keys + ] + + pg_all = pg_col_defs + [pg_pk] + pg_uniques + fk_clauses_pg + ms_all = ms_col_defs + [ms_pk] + ms_uniques + fk_clauses_ms + pg_statements.append(f'CREATE TABLE "{tname}" (\n ' + ",\n ".join(pg_all) + "\n);") + mssql_statements.append(f"CREATE TABLE [{tname}] (\n " + ",\n ".join(ms_all) + "\n);") + created_tables.add(tname) + + sql_ddl_postgres = "\n".join(pg_statements) + sql_ddl_sqlserver = "\n".join(mssql_statements) return { "attributes": sorted(attrs), @@ -450,8 +560,11 @@ async def normalize_relational_schema(payload: RelationalNormalizeRequest) -> Di "final_tableau": list(chase_res.final_tableau), "distinguished_row_index": chase_res.distinguished_row_index, "spurious_tuple_witness": chase_res.spurious_tuple_witness, + "spurious_tuple_explanation": spurious_explanation, }, - "sql_ddl": "\n".join(sql_ddl_statements), + "sql_ddl_postgres": sql_ddl_postgres, + "sql_ddl_sqlserver": sql_ddl_sqlserver, + "sql_ddl": sql_ddl_postgres + "\n\n" + sql_ddl_sqlserver, } except HTTPException: raise @@ -939,13 +1052,16 @@ def project_chunks(chunks: Sequence[Mapping[str, Any]]) -> List[Dict[str, Any]]: # ============================================================================= -# Frontend SPA Route +# Frontend Routes # ============================================================================= -@app.get("/", include_in_schema=False) -async def serve_overview() -> FileResponse: - """One-screen BQNF overview. Plain HTML, not rendered through Jinja.""" - return FileResponse(templates_dir / "overview.html", media_type="text/html") +@app.get("/", response_class=HTMLResponse) +async def serve_front(request: Request): + return templates.TemplateResponse( + request=request, + name="front.html", + headers={"Cache-Control": "no-cache"}, + ) @app.get("/studio", include_in_schema=False) @@ -954,5 +1070,9 @@ async def redirect_studio() -> RedirectResponse: @app.get("/studio/", response_class=HTMLResponse) -async def serve_index(request: Request): - return templates.TemplateResponse(request=request, name="index.html") +async def serve_studio(request: Request): + return templates.TemplateResponse( + request=request, + name="index.html", + headers={"Cache-Control": "no-cache"}, + ) diff --git a/web/static/app.js b/web/static/app.js index 47532b0..9bdb3f9 100644 --- a/web/static/app.js +++ b/web/static/app.js @@ -180,10 +180,10 @@ function renderRelationalResults(data) { tablesContainer.innerHTML = ''; data.synthesized_3nf.forEach(t => { const card = document.createElement('div'); - card.className = 'p-3 bg-slate-950 rounded-lg border border-slate-800 flex items-center justify-between text-xs font-mono'; + card.className = 'p-3 bg-slate-950 rounded-lg border border-slate-800 flex flex-wrap items-center justify-between gap-2 text-xs font-mono'; const pk = t.candidate_keys[0] ? `{${t.candidate_keys[0].join(', ')}}` : 'None'; card.innerHTML = ` -
+
${t.table_name} (${t.attributes.join(', ')})
@@ -209,14 +209,14 @@ function renderRelationalResults(data) { const witnessBox = document.getElementById('chase-witness-box'); if (!data.chase.is_implied && data.chase.spurious_tuple_witness) { witnessBox.classList.remove('hidden'); - witnessBox.className = 'p-3 rounded-lg border border-rose-800/80 bg-rose-950/40 text-xs font-mono text-rose-300 space-y-1'; + witnessBox.className = 'p-3 rounded-lg border border-rose-800/80 bg-rose-950/40 text-xs font-mono text-rose-300 space-y-1 break-words'; witnessBox.innerHTML = `
- Concrete Spurious Tuple Counterexample Witness Produced: + Spurious Tuple Counterexample Witness:
-
Projecting base relations produces spurious tuple: ${JSON.stringify(data.chase.spurious_tuple_witness)}
-
Natural join fails to reconstruct original relation without extraneous artifacts.
+
Projecting base relations produces spurious tuple: ${JSON.stringify(data.chase.spurious_tuple_witness)} — this row is in the join of the pieces but not in the original.
+
Natural join fails to reconstruct the original relation without extraneous rows.
`; } else { witnessBox.classList.add('hidden'); @@ -234,12 +234,15 @@ function renderRelationalResults(data) { data.chase.steps.forEach(s => { const tr = document.createElement('tr'); tr.className = 'hover:bg-slate-900/50 transition'; + const cellsText = (s.changed_cells && s.changed_cells.length > 0) + ? s.changed_cells.map(c => `R${c.row}.${c.column}: ${c.from} → ${c.to}`).join(', ') + : `${s.old_symbol} → ${s.new_symbol}`; tr.innerHTML = ` ${s.step_number} ${s.fd} Rows (${s.rows_matched[0] + 1}, ${s.rows_matched[1] + 1}) ${s.attribute_equated} - ${s.old_symbol} → ${s.new_symbol} + ${cellsText} `; tbody.appendChild(tr); }); @@ -247,7 +250,7 @@ function renderRelationalResults(data) { // Tableau Matrix View const matrixEl = document.getElementById('chase-tableau-matrix'); - if (data.chase.final_tableau && data.chase.final_tableau.length > 0) { + if (matrixEl && data.chase.final_tableau && data.chase.final_tableau.length > 0) { const heading = data.chase.heading; let html = ''; heading.forEach(a => { html += ``; }); @@ -268,7 +271,12 @@ function renderRelationalResults(data) { } // SQL DDL Output - document.getElementById('relational-sql-ddl').innerText = data.sql_ddl; + const ddlEl = document.getElementById('relational-sql-ddl'); + if (ddlEl) ddlEl.textContent = data.sql_ddl; + const pgDdlEl = document.getElementById('relational-sql-ddl-postgres'); + if (pgDdlEl && data.sql_ddl_postgres) pgDdlEl.textContent = data.sql_ddl_postgres; + const msDdlEl = document.getElementById('relational-sql-ddl-sqlserver'); + if (msDdlEl && data.sql_ddl_sqlserver) msDdlEl.textContent = data.sql_ddl_sqlserver; } @@ -458,7 +466,7 @@ function renderCompilerResults(data) { // ----------------------------------------------------------------------------- -// Module 4: AI Context LossLedger Gateway +// Module 4: Token Budget Audit (Experimental) // ----------------------------------------------------------------------------- async function executeAiLossLedger() { @@ -485,7 +493,7 @@ async function executeAiLossLedger() { }); if (!res.ok) { const err = await res.json(); - throw new Error(err.detail || 'AI LossLedger evaluation failed'); + throw new Error(err.detail || 'Token budget audit evaluation failed'); } const data = await res.json(); renderAiResults(data); @@ -524,18 +532,18 @@ document.addEventListener('DOMContentLoaded', async () => { if (res.ok) { PRESETS = await res.json(); // Populate defaults - if (PRESETS.relational) { + if (PRESETS.relational && document.getElementById('relational-attributes-input')) { loadRelationalPreset('ecommerce'); } - if (PRESETS.bqnf) { + if (PRESETS.bqnf && document.getElementById('bqnf-events-input')) { document.getElementById('bqnf-events-input').value = JSON.stringify(PRESETS.bqnf.financial_ledger.events, null, 2); executeBqnfSimulation(); } - if (PRESETS.compiler) { + if (PRESETS.compiler && document.getElementById('compiler-carrier-json')) { document.getElementById('compiler-carrier-json').value = JSON.stringify(PRESETS.compiler.employee_bcnf.test_carrier, null, 2); executeCompilerLowering(); } - if (PRESETS.ai) { + if (PRESETS.ai && document.getElementById('ai-chunks-input')) { document.getElementById('ai-chunks-input').value = JSON.stringify(PRESETS.ai.rag_research_context.source_chunks, null, 2); executeAiLossLedger(); } diff --git a/web/templates/front.html b/web/templates/front.html new file mode 100644 index 0000000..5485f62 --- /dev/null +++ b/web/templates/front.html @@ -0,0 +1,218 @@ + + + + + + Simplex Normal Forms Studio | smplxnf.anomalon.com + + + + + + + + + +
+
+ + + Anomalon / Simplex-NF Studio + + + +
+
+ +
+ +
+
+

+ Relational 3NF / BCNF Normalization, Tableau Chase & Incremental MAX Maintenance +

+

+ Synthesize lossless 3NF tables, inspect every chase step and spurious row on lossy splits, and compare PostgreSQL / SQL Server DDL. +

+
+
+ + + + Open /studio/ + +
+
+ + +
+ +
+
+
+

1. Schema & Functional Dependencies

+ +
+
+ + +
+
+ + +
+
+ + +
+ +
+ + +
+
+

2. Why Indexed Views Cannot Hold MAX

+ Sorted List per Group +
+

+ A SQL Server indexed view (WITH SCHEMABINDING) forbids MAX() and MIN() because deleting a group's current maximum cannot be repaired from the single stored scalar without rescanning the group. +

+
+
Query: SELECT region, SUM(amount), MAX(amount) FROM sales WHERE status = 'paid' GROUP BY region
+
Sorted list (North): [25, 60, 75, 120, 250] → DELETE 250 → next MAX = 120 (0 table scans)
+
+
+
+ + +
+
+
+
Candidate Keys
+
—
+
+
+
Key Columns
+
—
+
+
+
Chase Status
+
—
+
+
+ + +
+
+

Normal Form Checks

+
+
+
+

Synthesized 3NF Tables (Primary Keys)

+
+
+
+ + +
+
+

Tableau Chase Steps (FD Applied & Cells Changed)

+ +
+ +
+
Row${a}
+ + + + + + + + + + + + +
StepFD AppliedRows EquatedColumnCells Changed
Loading preset...
+
+ + + +
+
+

Generated DDL: PostgreSQL & SQL Server (PK, UNIQUE, FK)

+ +
+
+
+
PostgreSQL
+ 
-- PostgreSQL DDL
+
+
+
SQL Server
+ 
-- SQL Server DDL
+
+
+ +
+ + + + + + + + + + + + diff --git a/web/templates/index.html b/web/templates/index.html index a14d5fe..8722ba9 100644 --- a/web/templates/index.html +++ b/web/templates/index.html @@ -57,22 +57,25 @@ @@ -157,18 +160,18 @@

—
-
Prime Attributes
+
Key Columns (Prime)
—
-
Chase Join Status
+
Join Losslessness (Chase)
—
-

Normal Form Decision Invariants

+

Normal Form Checks

@@ -177,18 +180,18 @@

N

- Bernstein (1976) 3NF Synthesis (Lossless & Dependency-Preserving) + 3NF Decomposed Tables (Lossless & Dependency-Preserving)

-

Run synthesis to generate decomposed relational tables.

+

Click Normalize to generate decomposed relational tables.

-

Relational Tableau Chase Execution Trace

+

Tableau Chase Steps (FD Applied & Cells Changed)

@@ -199,8 +202,8 @@

Relati Step FD Applied Rows Equated - Attribute - Symbol Mutation + Column + Cells Changed @@ -217,12 +220,25 @@

Relati

-
+
-

Generated Relational DDL

- +

Generated Relational DDL (PostgreSQL & SQL Server)

+
- 
-- SQL DDL will appear here after synthesis
+
+
+
PostgreSQL DDL (PK / UNIQUE / FK)
+ 
-- PostgreSQL DDL
+
+
+
SQL Server DDL (PK / UNIQUE / FK)
+ 
-- SQL Server DDL
+
+
+

+ Why a SQL Server indexed view cannot hold MAX: A SQL Server indexed view (WITH SCHEMABINDING) cannot include MAX() or MIN() because deleting the current maximum row cannot be repaired from the single stored scalar without rescanning the group; maintaining a sorted list of values per group avoids that rescan. +

+

@@ -230,18 +246,18 @@

Genera - +