feat(echo): function-effect lattice, number-system stratification, and carrier-aware classification by hyperpolymath · Pull Request #44 · hyperpolymath/jtv-lang

hyperpolymath · 2026-06-18T02:11:27Z

Takes Echo from "proven lattice" to "carrier-aware compiler feature" in three cohesive steps. lake build + cargo fmt/clippy/test all green; zero sorry/admit/axiom; no unwrap/unwrap_or.

1 · Proofs — Echo × Epistemic function-effect lattice (Lean SECTION 5, ADR-0009)

Completes the (b) "Echo + Epistemic first-class" workstream on the proof side.

Epistemic (hidden/bounded/full = Opaque/Partial/Transparent) + Epistemic.join + comm/assoc/idem.
FunctionEffect — a point in Echo × Epistemic — with componentwise join + the three laws. These make effect::resolved_effects' call-graph join fold order- and repetition-independent (so g ∘ f carries effect f ⊔ effect g however calls are arranged).

2 · Proofs — number-system stratification (Lean SECTION 6)

Answers "are number systems additive on proofs, a rework, or stratified?" — stratified.

NumAlgebra (abelianGroup/approxGroup/nonGroup) maps 1:1 onto the Echo lattice; NumSystem + algebra + echo is the stratification map.
hex_binary_collapse (hex/binary are ℤ-encodings → int's tier), exact_groups_safe, float_not_safe/float_neutral (IEEE-754 non-associativity → neutral), no_current_system_breaks, reversal_tier_by_algebra.

3 · Compiler — carrier-aware Echo classification (Rust: `echo.rs`, `effect.rs`)

The first compiler-side step of "Echo as a real typesystem feature." Previously echo.rs classified every x += v as Safe from statement shape alone, ignoring the carrier; SECTION 6 shows that's incomplete.

additive_algebra / carrier_echo / NumAlgebra — the Rust mirror of SECTION 6.
CarrierEnv (var → BasicType) threaded through env-aware classifiers; a reversible += now grades as shape ⊔ carrier, so x += v over a float is Neutral even with no self-reference. Shape-only wrappers preserved (empty env ⇒ every carrier defaults to Int/Safe), so existing callers and behaviour are unchanged.
own_effect seeds the env from parameter type annotations, so fn f(x: float) { reverse { x += y } } resolves to echo Neutral end-to-end.

Default-carrier soundness: a variable absent from the env is treated as Int (Safe), not "unknown-lossy" — JtV numeric literals default to int (inferType (lit _) = int in Lean), so the only lossy carrier (float) is exactly the one that must be annotated/inferred to exist. Fuller inferred-local-type envs are a later slice.

🤖 Generated with Claude Code

https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742

…0009) Adds SECTION 5 to the Lean development: the formal counterpart of the Rust `epistemic.rs` + `effect.rs` slices that completed ADR-0009 D1-D3. * `Epistemic` inductive (hidden/bounded/full = Opaque/Partial/Transparent; the lowercase keywords are reserved in Lean, hence the rename) with `Epistemic.join` (full absorbing, hidden unit) and the lattice laws epi_join_comm / epi_join_assoc / epi_join_idem. * `FunctionEffect` structure — a point in the product lattice `Echo × Epistemic` — with componentwise `FunctionEffect.join` and the laws feffect_join_comm / feffect_join_assoc / feffect_join_idem proved from the Echo (SECTION 1) and Epistemic component laws. The three product laws are exactly what makes call-graph composition (`resolved_effects` in effect.rs) well-defined: the join fold is order- and repetition-independent, so `g ∘ f` carries `effect f ⊔ effect g` however the calls are arranged. `lake build` green; zero sorry/admit/axiom. Completes the (b) workstream (Echo + Epistemic first-class) on the proof side. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742

github-actions · 2026-06-18T02:12:33Z

🔍 Hypatia Security Scan

Findings: 51 issues detected

Severity	Count
🔴 Critical	0
🟠 High	25
🟡 Medium	26

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "scorecard_wrapper_missing_job_permissions",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (10 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/crates/jtv-core/benches/interpreter_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (6 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/crates/jtv-core/benches/parser_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Js.Array2 deprecated -- use Array (3 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/vscode-extension/src/Extension.res",
    "action": "search_replace",
    "rule_module": "migration_rules",
    "severity": "high"
  },
  {
    "reason": "Js.Promise deprecated -- use Promise (2 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/vscode-extension/src/Extension.res",
    "action": "module_replace",
    "rule_module": "migration_rules",
    "severity": "medium"
  },
  {
    "reason": "Belt.Array deprecated -- use Array (30 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/packages/jtv-analyzer/src/Main.res",
    "action": "module_replace",
    "rule_module": "migration_rules",
    "severity": "high"
  },
  {
    "reason": "Belt.Option deprecated -- use Option (2 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/packages/jtv-analyzer/src/Main.res",
    "action": "module_replace",
    "rule_module": "migration_rules",
    "severity": "medium"
  },
  {
    "reason": "Js.Array2 deprecated -- use Array (7 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/packages/jtv-analyzer/src/Main.res",
    "action": "search_replace",
    "rule_module": "migration_rules",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…roundwork) Adds SECTION 6: the reversibility tier of `+` over a number system is not a per-system stipulation but is *forced* by the carrier's additive algebra. * `NumAlgebra` (abelianGroup / approxGroup / nonGroup) — one constructor per Echo tier; the algebra tower maps 1:1 onto the SECTION 1 Echo lattice, so three levels suffice (a finer Monoid ⊂ CancellativeMonoid ⊂ Group tower would collapse onto the same 3-valued codomain). * `NumSystem` (the seven addable JtvType carriers) + `NumSystem.algebra` + `NumAlgebra.echo` + `NumSystem.echo` — the stratification map. Headline theorems pin the two design facts: * `hex_binary_collapse` — hex/binary are *encodings of ℤ*, not new algebras, so they carry int's tier exactly (encoding ≠ algebra). * `exact_groups_safe` — int/rational/complex/symbolic are exact abelian groups, hence `safe`. * `float_not_safe` / `float_neutral` — IEEE-754 addition is non-associative, so its reversal is lossy; the stratification lifts float to `neutral`. This is the single place "addition-only ⇒ reversible" is qualified by the carrier (and does not threaten the abstract lattice laws — those grade, not compute). * `no_current_system_breaks` — `breaking` is presently empty, reserved for a future non-invertible (nonGroup) system. * `reversal_tier_by_algebra` — ties the tier back to the SECTION 1/2b reversal policies: `safe` ⇔ exact abelian group; non-`breaking` ⇔ not a nonGroup. This answers the design question "are number systems additive on proofs, or a rework, or stratified?" — they are *stratified*: the existing Int results become the ℤ (abelianGroup) instance, and each further carrier is classified by its additive algebra rather than reproving the spine. `lake build` green; zero sorry/admit/axiom. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742

github-actions · 2026-06-18T02:19:04Z

🔍 Hypatia Security Scan

Findings: 51 issues detected

Severity	Count
🔴 Critical	0
🟠 High	25
🟡 Medium	26

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "scorecard_wrapper_missing_job_permissions",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (10 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/crates/jtv-core/benches/interpreter_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (6 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/crates/jtv-core/benches/parser_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Js.Array2 deprecated -- use Array (3 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/vscode-extension/src/Extension.res",
    "action": "search_replace",
    "rule_module": "migration_rules",
    "severity": "high"
  },
  {
    "reason": "Js.Promise deprecated -- use Promise (2 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/vscode-extension/src/Extension.res",
    "action": "module_replace",
    "rule_module": "migration_rules",
    "severity": "medium"
  },
  {
    "reason": "Belt.Array deprecated -- use Array (30 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/packages/jtv-analyzer/src/Main.res",
    "action": "module_replace",
    "rule_module": "migration_rules",
    "severity": "high"
  },
  {
    "reason": "Belt.Option deprecated -- use Option (2 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/packages/jtv-analyzer/src/Main.res",
    "action": "module_replace",
    "rule_module": "migration_rules",
    "severity": "medium"
  },
  {
    "reason": "Js.Array2 deprecated -- use Array (7 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/packages/jtv-analyzer/src/Main.res",
    "action": "search_replace",
    "rule_module": "migration_rules",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

Makes Echo classification consult the carrier's number system, not just the statement shape — the first compiler-side step of "Echo as a real typesystem feature". Operational counterpart of JtvEcho.lean SECTION 6. echo.rs: * NumAlgebra / additive_algebra / carrier_echo — the Rust mirror of the Lean stratification (AbelianGroup -> Safe, ApproxGroup -> Neutral, NonGroup -> Breaking; hex/binary share int's class as Z-encodings; Bool/String have no additive algebra). * CarrierEnv (var -> BasicType) threaded through env-aware classifiers (classify_*_in_env, function_echo_in_env). A reversible `+=` now joins its statement shape (self-ref -> Neutral) with its carrier echo, so `x += v` over a float grades Neutral even without self-reference. * Shape-only wrappers (classify_stmts, function_echo, ...) preserved: an empty env defaults every carrier to Int (Safe), so existing behaviour and the other callers are unchanged. effect.rs: * own_effect now seeds a CarrierEnv from the function's parameter type annotations, so `fn f(x: float) { reverse { x += y } }` resolves to echo Neutral end-to-end through resolved_effects. Default-carrier soundness: a variable absent from the env is treated as Int (Safe), not "unknown-lossy" — JtV numeric literals default to int (inferType (lit _) = int in Lean), so the only lossy carrier (float) is exactly the one that must be annotated/inferred to exist. Fuller inferred-local-type envs are a later slice. No unwrap/unwrap_or (avoids Hypatia dangerous-default). cargo fmt + clippy clean; 122 lib tests pass incl. 4 new carrier-aware cases. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742

github-actions · 2026-06-18T06:05:29Z

🔍 Hypatia Security Scan

Findings: 51 issues detected

Severity	Count
🔴 Critical	0
🟠 High	25
🟡 Medium	26

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "scorecard_wrapper_missing_job_permissions",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (10 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/crates/jtv-core/benches/interpreter_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (6 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/crates/jtv-core/benches/parser_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Js.Array2 deprecated -- use Array (3 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/vscode-extension/src/Extension.res",
    "action": "search_replace",
    "rule_module": "migration_rules",
    "severity": "high"
  },
  {
    "reason": "Js.Promise deprecated -- use Promise (2 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/vscode-extension/src/Extension.res",
    "action": "module_replace",
    "rule_module": "migration_rules",
    "severity": "medium"
  },
  {
    "reason": "Belt.Array deprecated -- use Array (30 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/packages/jtv-analyzer/src/Main.res",
    "action": "module_replace",
    "rule_module": "migration_rules",
    "severity": "high"
  },
  {
    "reason": "Belt.Option deprecated -- use Option (2 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/packages/jtv-analyzer/src/Main.res",
    "action": "module_replace",
    "rule_module": "migration_rules",
    "severity": "medium"
  },
  {
    "reason": "Js.Array2 deprecated -- use Array (7 occurrences)",
    "type": "deprecated_api",
    "file": "/home/runner/work/julia-the-viper/julia-the-viper/packages/jtv-analyzer/src/Main.res",
    "action": "search_replace",
    "rule_module": "migration_rules",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…atification) The runtime-value half of the number-system stratification (ADR-0010, realizing ADR-0007 D6), complementing the type-level carrier_echo merged in #44. number.rs: * Value::number_system(&self) -> Option<BasicType> — a runtime value's number system (None for the non-numeric carriers bool/string/list/tuple/token/unit). * Value::reversal_echo(&self) -> Echo — the reversal tier forced by that value's additive algebra, delegating to echo::carrier_echo so the algebra->tier map has a single source of truth (mirrors JtvEcho.lean SECTION 6). docs/design-decisions/0010-number-system-stratification.adoc: * Records the 3-level additive-algebra tower (abelianGroup/approxGroup/nonGroup) 1:1 with the Echo lattice, the seven systems' classification (hex/binary = Z-encodings; float = approxGroup -> Neutral), the carrier-aware += grading (shape join carrier) + default-carrier=Int soundness, and the one-algebra/three-surfaces (proof/type/value) mirror. * Honestly reconciles with ADR-0007 D6: float is an approximate group, not a D6-cancellative monoid, so among the seven systems D6's cancellative (Neutral) and idempotent (Breaking) routes are anticipated-but-uninhabited; the towers meet at Safe/Neutral/Breaking. STATE.a2ml: register ADR-0010; record the Echo-arc + stratification milestone; mark (b) and the stratification classification landed; gap-005 partial (value- level type_preservation beyond tau=int still open); flag the float-locals CarrierEnv-inference soundness slice as next. cargo fmt + clippy clean; 124 lib tests pass (2 new). No unwrap/unwrap_or. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742

hyperpolymath changed the title ~~feat(JtvEcho): mechanise Echo×Epistemic function-effect lattice (ADR-0009)~~ feat(JtvEcho): Echo×Epistemic function-effect lattice + number-system stratification Jun 18, 2026

hyperpolymath changed the title ~~feat(JtvEcho): Echo×Epistemic function-effect lattice + number-system stratification~~ feat(echo): function-effect lattice, number-system stratification, and carrier-aware classification Jun 18, 2026

hyperpolymath marked this pull request as ready for review June 18, 2026 06:10

hyperpolymath merged commit 7db5c28 into main Jun 18, 2026
32 checks passed

hyperpolymath deleted the claude/dazzling-albattani-ubS9r branch June 18, 2026 06:10

hyperpolymath mentioned this pull request Jun 18, 2026

feat(number): runtime-value Echo bridge + ADR-0010 (number-system stratification) #45

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(echo): function-effect lattice, number-system stratification, and carrier-aware classification#44

feat(echo): function-effect lattice, number-system stratification, and carrier-aware classification#44
hyperpolymath merged 3 commits into
mainfrom
claude/dazzling-albattani-ubS9r

hyperpolymath commented Jun 18, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jun 18, 2026

Uh oh!

github-actions Bot commented Jun 18, 2026

Uh oh!

github-actions Bot commented Jun 18, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

hyperpolymath commented Jun 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

1 · Proofs — Echo × Epistemic function-effect lattice (Lean SECTION 5, ADR-0009)

2 · Proofs — number-system stratification (Lean SECTION 6)

3 · Compiler — carrier-aware Echo classification (Rust: echo.rs, effect.rs)

Uh oh!

github-actions Bot commented Jun 18, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 18, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 18, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

hyperpolymath commented Jun 18, 2026 •

edited

Loading

3 · Compiler — carrier-aware Echo classification (Rust: `echo.rs`, `effect.rs`)