From d3f84efb048dab17d0906449364a3a838d19aa69 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Mon, 12 Oct 2026 12:18:43 +0200 Subject: [PATCH 1/4] docs: propose typed logic compiler over shared masking algebra --- docs/ALGEBRAIC-LOGIC-COMPILER-RFC.md | 295 +++++++++++++++++++++++++++ 1 file changed, 295 insertions(+) create mode 100644 docs/ALGEBRAIC-LOGIC-COMPILER-RFC.md diff --git a/docs/ALGEBRAIC-LOGIC-COMPILER-RFC.md b/docs/ALGEBRAIC-LOGIC-COMPILER-RFC.md new file mode 100644 index 0000000..ee8360f --- /dev/null +++ b/docs/ALGEBRAIC-LOGIC-COMPILER-RFC.md @@ -0,0 +1,295 @@ +# RFC: Typed Logic Compiler over OGAR Classes, Methods, Schemas and the Mask/Fold Algebra + +**Date:** 2026-10-12. **Status:** DESIGN PROPOSAL / documentation only. **No new instruction, new CE64 meaning, persisted schema, runtime, permission or external write is authorized.** +**Companion:** [Falsification and migration plan](ALGEBRAIC-LOGIC-COMPILER-FALSIFICATION.md). +**Proposal ID:** D-TLAC-0. **Intent:** make heterogeneous logics typed readings and procedures over one existing physical executor, not multiple logic engines. + +## 0. Thesis, invariants and non-goals + +**Hypothesis:** A useful, finite subset of NARS/NAL and CE64, Heckhausen–Gollwitzer action-phase logic, OGIT/OGAR automation, IAM reconciliation, CRM workflows, and some PLN/MeTTa rules can lower through the **same physical mask/fold algebra**, provided each is bound to a *separate declared semantic type and proof obligations*. A shared machine instruction is **not** evidence that all those logics mean the same thing. + +Architectural separation: + +- **Class**: canonical OGAR identity, inheritance, applicable object/edge population, ClassView reading and access surface. +- **Schema**: typed fields, null/unknown policy, constraints, effect and evidence semantics, version and legal transitions. +- **Method**: stable function identity + signature, pure procedure or guarded action, claimed algebraic laws, body reference and provenance contract. +- **Compiler**: resolve symbols, bind types, normalize legal rewrites, lower to R2IL procedures and mask-risc; refuse unsound cases. +- **Physical execution**: borrowed SoA planes, `mask-risc::Program` and `ndarray::simd`, never a bespoke per-logic row loop. +- **DO boundary**: OGAR `ActionDef`/`ActionInvocation`, hard RBAC/state/commit checks, then capability executor. Reasoning can suggest an action; it cannot authorize one. + +**Unchanged contractual floors:** + +1. The 8-bit ALU/ISA lanes are meaning-free bytes. The V3 `classid:u32 + 12-byte opaque register` may be read differently under a ClassView. CE64, NARS frequency/confidence, epistemic bits, identity, SPO and witness are *readings*, not a hard-coded new layout. No bit/tenant/opcode mint here. +2. `ClassId` is address, never permission. Existing canonical id/codebook is linked, not duplicated. Version and class-scoped reading gates apply before decoding or writing. +3. No serialization or row/array materialization in the hot path; fold algebra reads borrowed lanes, graph-flow holds handles. Explicit, authorized and bounded materialization only at an external boundary. +4. No external effects from `mask-risc`, a NARS goal, an LLM tool response, a workflow branch or an `ActionProposal`. External mutation must traverse the hard OGAR gate. +5. No second reasoning executor unless a **named, executable insufficiency test** proves the existing procedures cannot express an exact required result within the specified memory/performance limits. +6. Do not treat a stated law (commutative, idempotent, monotone) as a free optimizer hint. A checked law certificate is a prerequisite for that rewrite. + +This is neither a new universal Boolean logic nor a claim of NARS/PLN/MeTTa equivalence. Population masks express selection; truths, bindings, source independence, ordered events, and external effects require richer typed objects and explicit laws. + +## 1. Verified code inventory (as examined on 2026-10-12) + +| Contract | Existing surface | Verified limitation / caveat | +|---|---|---| +| Canonical types | [`ogar-vocab`](../crates/ogar-vocab/src/lib.rs): `Class`, `MethodDecl` with `MethodKind` / `RecordSemantics` and opaque `body_source`, plus `ActionDef` / `ActionInvocation` / `KausalSpec` | `MethodDecl` describes harvested methods but is not a verified executable algebra body; `ActionDef.reads/writes` are name-level effect annotations, not computed values | +| Function inventory | [loco orchestration gap](LOCO-ORCHESTRATION-GAP.md): `LocoConcept::Inventory` 0x1702 is minted as a function registry concept | Full functions-as-objects address/body resolver is **not implemented** by that declaration | +| NARS vocab | [`ogar-loco/src/nars.rs`](../crates/ogar-loco/src/nars.rs): **34** recipes = **9 Datapath, 19 Control, 6 Gate**; class-selected vocabulary with `0x90..=0xB1` range | All Control recipes currently have `body_refs = 0`. A vocabulary row is not executable procedure parity | +| Bulk executor | [lance-graph mask-risc](https://github.com/AdaWorldAPI/lance-graph/blob/main/crates/lance-graph-mask-risc/src/ir.rs): `Pred`, `MaskOp::{And,Or,Xor,AndNot,Not,Ternlog,Gather}`, `Terminal::{Any,All,Count,Keep,BlendI32}`, grouped and strided folds | One `Program` has **one terminal**; outputs and ordering laws depend on terminal and input layout | +| Procedure dialect | [lance-graph R2IL](https://github.com/AdaWorldAPI/lance-graph/blob/main/crates/lance-graph-r2il/src/lib.rs): `FoldDialect` lowers fold calls onto mask-risc; `Val` is scalar/slot/address, no row-sized loco value | Unsupported R2IL operations and branches on populations deliberately refuse/poison, not automatically executed | +| CE64/NAL | [lance-graph #1496](https://github.com/AdaWorldAPI/lance-graph/pull/1496) **merged** documentation: D-HL-0..10 and D-NALP-0..11, sparse hypothesis layers and NAL compiler plan | `lance-graph-nal` / `ogar-nal` and 64 hypothesis lanes are **proposals**; no equivalence established by the document | +| PLN/attention | [#1497](https://github.com/AdaWorldAPI/lance-graph/pull/1497) **draft** PLN/Shannon/EIG source and falsifier map | PLN truth transfer and NARS confidence are distinct; scheduler comparisons unmeasured | +| Hyperon/MeTTa | [#1498](https://github.com/AdaWorldAPI/lance-graph/pull/1498) **draft** MeTTa/metagraph parity and source map | Row masks do not preserve a nondeterministic multiset of substitutions by themselves | +| Orchestration | [`graph-flow-kanban`](https://github.com/AdaWorldAPI/rs-graph-llm/blob/main/graph-flow-kanban/src/lib.rs): `Planning → CognitiveWork → Evaluation → {Commit,Plan,Prune}` | An **inner cognitive decision cycle**; not automatically the 4 psychological action phases | +| Action gate | [`graph-flow-action-ogar`](https://github.com/AdaWorldAPI/rs-graph-llm/blob/main/graph-flow-action-ogar/src/lib.rs): `GatedOgarHandler` wraps capability executor, runs only after `commit_via` def/RBAC/guard/MUL checks | No proposal may circumvent `ActionInvocation` or let a model construct an authorized action | +| Workflow ↔ fold | [`graph-flow-lance`](https://github.com/AdaWorldAPI/rs-graph-llm/blob/main/crates/graph-flow-lance/README.md): generation-checked plan/result handles, mask-set fanout-as-fold, explicit materialize | External handle identity, fold-result → stable `ActionInvocation` DO adapter, Quack/Rig retrieval and pause-as-bytes remain marked **Not built** | +| HubSPO-rs | [H-ADR-7](https://github.com/AdaWorldAPI/HubSPO-rs/blob/main/.claude/plans/hubspo-integration-v1.md): workflows and delays as Lance rows, Quack due masks, graph-flow execution | `ractor` and supervisor dependency/actor-per-record workflow are **explicitly forbidden** for this consumer | +| Rig | [AdaWorldAPI/rig](https://github.com/AdaWorldAPI/rig): provider/tool interfaces and separate LanceDB vector adapter | `rig-lancedb` does **not** implement the full lance-graph Quack/CE64 substrate | + +Read [OGAR as IR](OGAR-AS-IR.md), [The Firewall](THE-FIREWALL.md), [HIRO DO lift](HIRO-DO-ARM-LIFT.md) and [ActionHandler gate](ACTIONHANDLER-TURSTEHER.md) before changing types or runtime policy. + +## 2. Proposed compiler contract and dataflow + +```text +OGIT TTL / Ruby / Python / Elixir / CRM / IAM / Narsese / finite MeTTa + │ producer / parser (semantic source only) + ▼ +OGAR registry: ClassId + Class + MethodDecl + Schema + ClassView + │ link MethodOrdinal and declared semantic reading + ▼ +Typed LogicMethodSpec (sidecar; not a new core IR field) + │ effect & type check; legal algebraic rewrites only + ▼ +Pure expression graph → OGAR loco procedures / R2IL FoldDialect + │ + ▼ +mask-risc::Program → ndarray::simd over borrowed Lance planes + │ + ├── RowMask / FoldResult / Truth / BindingSet / PlanHandle + │ │ bounded RBAC materialize + │ ▼ + │ Rig / LLM + │ + ├── Evidence revision / new question / re-plan [THINK] + │ + └── ProposedAction [NOT executable] + │ + OGAR ActionInvocation + ClassRbac + StateGuard + MUL + │ + CapabilityExecutor [DO] + │ + idempotent receipt + observation + └── post-action evaluation / new evidence +``` + +**No new layer is justified solely to give existing operations an attractive name.** Use the existing `Class` and `MethodDecl` as canonical source declarations and resolve a separate typed compile-time method manifest until a specific lossless roundtrip test proves an IR extension is necessary. + +Proposed illustrative type signature, **pseudocode, not a shipped API**: + +```rust +struct LogicMethodSpec { + owner: ClassId, + ordinal: MethodOrdinal, // stable within owner; resolved by registry + schema_version: SchemaVersion, + reading: ClassViewReadingId, // declared bytes→semantics mapping + inputs: Vec, + output: Sort, // RowMask | Fold | Truth | Bindings | Goal | Plan + effect: EffectClass, // Pure | ReadVersion | Propose | ExternalMutate + body_ref: ContentAddressedRef, + evidence_policy: EvidencePolicy, + verified_laws: Vec, +} +``` + +A method has *identity* independent from its source-language string or runtime address. Binding resolves names to classids, field offsets, lane kinds and method ordinals **once**; the hot path gets prebound input/constant/slot addresses and versioned handles. + +### 2.1 A typed algebra, not a universal truth table + +A plain Boolean row mask is `RowMask`. It may be intersected only with a mask for the *same* row universe and source generation. A semijoin may transform mask universes only through a **declared typed foreign key**. Related sorts must remain distinct: + +- `RowMask`: selected row addresses. +- `Truth`: frequency/confidence together with independent source identities; combining values needs NARS law and evidence-overlap check. +- `EpistemicState`: direct/indirect, known/unknown etc. from declared CE64/59..63 interpretation, **not** equal to statistical confidence. +- `ThreeValued`: null and open-world unknown must not be silently mapped to a Boolean false. +- `Belnap4` or other multivalued logics: a proposed typed product of masks only if the lattice truth tables and merges are independently validated. +- `BindingMultiset`: ordered/nested and multiply matching substitutions. Cannot be represented as a single row mask in general. +- `StateTransition`: from-state, guard, ordered event, to-state and terminal/deadline semantics. +- `ActionProposal`: intent and expected effects; never an authorized mutation. + +Distinct semantic readings can reuse the *same* ndarray/mask-risc instructions without assuming equal inference laws or equal results. + +### 2.2 Law-aware rewrites with precise refusals + +| Law/procedure | Valid physical interpretation | Guard/negative counterexample | +|---|---|---| +| Boolean `AND/OR/NOT/TERNLOG` | exact combinational mask logic on one population and version | null/unknown/SQL three-valued tables and RBAC scope mismatch | +| Existential `Any/All/Count` | mask reduction | choice of empty-set convention is schema-specific; existential bindings not just row count | +| Semijoin `Gather/EqU32Via` | mask across FK edge, with gated fetch | missing FK/out-of-range, circular traversal, cardinality/multiset/ordered output | +| Finite numeric fold | `GroupReduce`, `GroupPowerSums`, `GroupCrossPowerSums` where already supported | overflow bounds, weight conversion, rounding/order and duplicated evidence | +| Conditional typed lane | `BlendI32` for selected lane values | class/property permission and semantic sort of chosen values | +| Structural state guard | mask over typed state + `on_enter` effect proposal | execution is never a masked write; persistence, approval and ordering remain explicit | +| Revision / retraction | accumulate **independent** evidence; then apply checked truth function once | `Σw` is not idempotent under replay; repeated source cannot inflate NARS confidence | +| Schedule / fixpoint | external typed composition of finite folds | termination, monotonicity and iteration order need a certificate; general recursion not silently supported | +| Contextual causality | CE64 Pearl/epistemic facet predicates + independent interventions | association/correlation is not proof of causal effect | + +A verified law is keyed by **method id + semantic reading version + input sorts + null policy + evidence policy + numerical bounds**. No certificate means no reorder/fuse. Do not invent shared NARS/PLN truth math because both expose "confidence". + +### 2.3 Three equivalent Boolean guards (first proof target) + +Illustrative declarations, **not a new DSL implementation**: + +```text +class IAMUser { + schema Directory; + method needs_license_review() : RowMask = + active & !licensed & independent_evidence; +} +class Deal { + schema HubSPO; + method may_enter_stage() : RowMask = + active & !blocked & properties_complete; +} +class CognitiveCycle { + schema Rubicon; + method may_advance() : RowMask = + eligible & !veto & gate_open; +} +``` + +After binding each field to its own domain lanes, all three have the **same canonical Boolean expression shape**, so their optimized *operator sequence* can be equivalent. They do **not** share physical lane IDs, population identity or semantics. The first falsifier compares canonicalized plan shape and separate plain-loop oracles under adversarial masks, including null/unknown and domain mismatches. + +### 2.4 NARS revision as a weighted fold (gated hypothesis) + +D-NALP proposes carrying a fixed-point weight `w` and frequency `f` with an independent evidential stamp per delta. For each statement key, the group cross-power fold can calculate `Σw` and `Σ(w·f)` exactly within documented bounds; derive frequency and confidence **once at the end**, not by repeatedly rounding u8 revisions. This is only legal after a provenance check that contributing stamps are independent or have been deduplicated under the agreed NARS rule. + +```text +Source observations → immutable indexed deltas → typed stamp-overlap guard +→ statement-key semijoin → GroupCrossPowerSumsI32 +→ truth law / scalar oracle → output Truth +``` + +No semantic guarantee that the exact current NARS confidence formula, D-HL hypothesis layers or ONA are equivalent until the pinned differential suite passes. A missing per-row truth-producing terminal is **a probe question**, not automatic permission to add an opcode. + +## 3. Heckhausen/Gollwitzer Rubicon as an outer action-phase model + +The psychological action-phase model distinguishes **predecisional deliberation**, **preactional planning**, **actional execution** and **postactional evaluation**. Gollwitzer's implementation intentions refine the preaction phase: *if context X, then act Y*. An internal goal commitment is **not** a permission to mutate production state. + +Separate **three** boundaries: + +1. **Goal-intention selection (psychological Rubicon):** choose a goal under competing hypotheses and evidence. +2. **Action planning:** choose an if/then situation/action method, compute preconditions and simulation, set wait/approval policy. +3. **OGAR hard commit:** verify ActionDef match, ClassRbac, StateGuard, MUL gate, freshness/idempotency and any required human authorization **before the real executor**. + +The existing `lance_graph_contract::kanban::KanbanColumn` / `graph-flow-kanban` cycle is `Planning→CognitiveWork→Evaluation→{Commit,Plan,Prune}`. Its `Evaluation` is **pre-acceptance cognitive validation**. It is **not** the psychological postaction evaluation of an observed external effect. Preserve the existing enum discriminants and transition semantics; add an *outer* typed phase projection (or graph-flow context) if validated, rather than renumbering the inner state machine. + +```text +Outer: deliberate → goal_intention → implementation_intention → execute + │ OGAR authorization + revise_goal ← postaction_expected_vs_observed ← external receipt +Inner: Planning → CognitiveWork → Evaluation → Commit | Plan | Prune +``` + +Postaction evaluation must distinguish observed consequence, causal attribution and confidence update. A "success" returned by an executor is not the same as observed target state. No Libet timing offset is a universal psychological calibration; current offsets are internal code conventions, not a measured physiological fact for IAM/CRM. + +## 4. ONA, PLN and Hyperon remain independent oracles + +- [OpenNARS for Applications](https://github.com/opennars/OpenNARS-for-Applications) has `NAR_AddInputBelief`, `NAR_AddInputGoal` and `NAR_AddOperation`; `Decision_Execute` performs selected operations in ONA. **Adapt the selected operation to `ActionProposal`**, never run an ONA callback against IAM/CRM. Compare goals, anticipated consequences, failures and procedure choices on pinned fixtures. +- #1496/D-NALP: literal Narsese oracle vs typed mask-risc lowering, source independence and sparse hypothesis layers. +- #1497: separate *logic* parity from FIFO/confidence/Shannon/EIG/Moore/Staunen *attention* policies, with equal candidate/evidence/compute budgets. +- #1498: MeTTa output can be nondeterministic with repeated substitutions, nested atoms and higher-order rewrites. A Boolean mask of matching source rows is not a proven replacement for a typed multiset or general metagraph recursion scheme. Preserve exact cardinality, ordering policy and error/empty distinctions; otherwise refuse. +- Distinguish observation truth, inference uncertainty, epistemic evidence strength and causal intervention. Correlation or confidence does not create entitlement to execute. + +**Research anchors (conceptual, not runtime parity):** Heckhausen & Gollwitzer (1987), *Thought contents and cognitive functioning in motivational versus volitional states of mind*; Gollwitzer (1999), *Implementation Intentions: Strong Effects of Simple Plans*. Executable sources: [ONA](https://github.com/opennars/OpenNARS-for-Applications), [modern PLN](https://github.com/trueagi-io/PLN), [Hyperon](https://github.com/trueagi-io/hyperon-experimental). + +## 5. Virtualized actor semantics without ractor dependence + +A stable logical actor is *address* `(tenant,ClassId,NodeGuid)` + versioned state + pending events. Its execution is activated by a mask over persisted work, not a permanent actor process. On activation: read generation-checked scope, borrow required data, run pure methods, propose an action, revalidate before DO, write receipt. The durable owner remains the Lance version/write lane; a per-object actor is not necessary. + +Erlang/OTP `gen_statem` is a **behavioral oracle** for postposition, entry effects, timeouts and ordered event replay; BEAM/ractor may remain optional isolated control-plane adapters, not required hot-path runtimes. HubSPO-rs H-ADR-7 prohibits ractor/supervisor workflow actors and stores resume/deadline/offset as rows with Quack due masks. Cross-process action delivery must prove stable ordering, backpressure, replay and idempotent **external outcome**, not just exactly-once local fold. + +## 6. Rig ↔ graph-flow ↔ lance-graph ↔ OGAR + +- **Rig = LangChain-shaped interface:** models/tools/retrieval, not independent canonical truth. Its LanceDB vector adapter is not general Quack/CE64 retrieval. +- **rs-graph-llm graph-flow = LangGraph-shaped orchestration:** stateful task graph, session pause/resume, condition edges, outer action intent. Retain `graph-flow-lance` handle-only Context for plans/results; materialize only a bounded, policy-projected export to a model. +- **lance-graph = execution and versioned knowledge substrate:** R2IL, Quack, mask-risc, folds, sparse CE64 and source generation checks. +- **OGAR = class/method/signature/authority:** capability declaration and actual effect gate. `GatedOgarHandler` cannot be bypassed by any agent. +- **z8run = trigger/external edge orchestration, where present:** already shares the handle registry with graph-flow-lance; do not fork a second one. + +Explicit known missing seams in [graph-flow-lance README](https://github.com/AdaWorldAPI/rs-graph-llm/blob/main/crates/graph-flow-lance/README.md): cross-process handle identity, Quack retrieval via Rig, suspension-as-bytes, fold result→stable DO invocation mapping, and z8run's AI nodes consolidation. Arrival time must **not** be action identity: duplicate MQTT/QoS1 or webhook delivery must not repeat a side effect. + +## 7. IAM and HubSPO worked semantic examples + +### IAM source conflict and license repair (simulation first) + +```text +Observed (v): AD status active; Entra license missing; HR sources disagree. +Pure query: tenant_scope ∩ active ∩ ¬licensed ∩ independent_source +Hypotheses: delayed provisioning | missing group | competing source overwrote +Goal: verified correct assignment WITHOUT violating canonical source precedence +Method: inspect_memberships → simulate_assignment → validate uniqueness/capacity +Proposal: ActionDef.assign_license(NodeGuid, desired_license, witness, source_version) +Gate: source authority, unique UPN/SMTP, ActorContext role, approval, idempotency +After DO: read next independent Entra observation; compare desired vs observed. +Update: CE64/NARS belief about cause only after evidence-overlap and counterfactual checks. +``` + +Canonical GUID joins, source precedence, identity uniqueness and grants are **hard invariants**, not learning weights. If the postaction observation fails, do not blindly repeat the same external mutation. + +### HubSPO workflow / deal stage + +```text +Query: CRM owned rows (dir-sim team membership) ∩ stage predicate ∩ due workflow +Intent: advance deal only if required fields present and explicit trigger applies +ActionDef: move_stage; StateGuard: allowed previous stage(s) +graph-flow: plan → optional human approval → run_gated +Workflow run state / resume_at / offset: persisted Lance rows, due via Quack mask +Postaction: observe accepted CRM version and side-effect receipts, update plan +``` + +The CRM owner mask is a compiled owner-set filter, not an OU-tree sibling/parent walk. Field-level authorization precedes wire/materialization. No actor-per-deal, custom timer supervisor or DataFusion fallback is implied. + +## 8. Function inventory, effect system and read/write authority + +A function can be *represented* as an OGAR-identified object even if execution happens elsewhere. A method body may be an R2IL procedure, a graph-flow plan (control), an opaque external handler (effect) or explicitly unsupported. The registry needs typed address, body hash/version, parameters, result sort, approved input lenses, effect level, provenance requirement and verified optimizer laws. + +| Effect class | Result | Permitted executor | +|---|---|---| +| Pure | RowMask, Truth, Fold, CandidateSet | existing R2IL / mask-risc / ndarray only | +| ReadVersion | generation-checked plan/result handle | authorized Lance read; declared scope | +| Propose | inert ActionProposal with witness | deterministic builder / graph-flow, no side effects | +| ExternalMutate | receipt / observed next version | **only** OGAR commit-checked CapabilityExecutor + external idempotency/outbox | + +A raw prompt, NARS goal or method return type must **never** be coerced into `ExternalMutate`. Use explicit typed escalation. A stale generation, absent schema reading, unauthorized field, duplicate effect or unresolved bindings set yields a typed refusal. + +## 9. Decision queue (no automatic implementation approval) + +- **O1** Where is the first lossless, linked Function Inventory body stored? Existing `MethodDecl`/`ActionDef`, sidecar, or new canonical field? Require codegen roundtrip. +- **O2** Stable method identity/version and canonical numeric ordinals; no string lookups/inline handlers on hot path. +- **O3** Sort system for mask universe/version/scope, Null/Unknown, Truth/Stamp, BindingMultiset, ActionProposal. +- **O4** Certification/rewrite regime for laws; numeric bounds, overflow, idempotency, order, independent sources. +- **O5** CE64 reading version and evidence overlap; defer to D-HL and D-NALP operators. +- **O6** Psychological goal commitment vs technical `KanbanColumn::Commit` vs OGAR gate; outer state home. +- **O7** Cross-process plan and action IDs, deterministic replay and external receipts/outbox. +- **O8** How exactly Rig obtains bounded, policy-checked Quack exports without alternate state authority. +- **O9** Executable exact subset for ONA/NAL/PLN/MeTTa; unsupported outputs refused, not approximate without label. +- **O10** Whether actor activation semantics improves a measured workload without contradicting HubSPO H-ADR-7. +- **O11** Minimal primitive/byte only after insufficiency proof; no second evaluator. +- **O12** Provenance through revision, action execution and postaction causal evaluation without double count. + +## 10. Wave plan and owners + +| Wave | Deliverable | Exit rule | +|---|---|---| +| W0 **this PR** | document typed architecture, truth boundaries and falsifiers | docs only, no ABI/code edits | +| W1 | pure 3-domain Boolean-guard normalization prototype | same normalized ops; separate independent scalar oracles | +| W2 | Function Inventory address + method binding/roundtrip | no duplicate authoritative method table and no hot string | +| W3 | NARS stamped revision / typed epistemic gates | exact oracle + duplicates/overflow/unknown falsifiers | +| W4 | psychological goal/implementation/postaction typed state | distinct pre/post evaluation, event/timeout parity | +| W5 | mock-only IAM/CRM proposal → gate → receipt → observe | hard policy failure closes without external command | +| W6 **conditional** | smallest necessary new typed primitive/sort only | documented failing counterexample from earlier waves | + +Owners: **OGAR** semantic IR/inventory; **lance-graph** bind and physical folds/evidence; **ndarray** generic SIMD implementation; **rs-graph-llm** graph and action execution; **Rig** untrusted model IO; **IAM/HubSPO** domain source authority and policy. No wave changes other repos implicitly. + +Details and executable negative controls: [falsification plan](ALGEBRAIC-LOGIC-COMPILER-FALSIFICATION.md). + +**Architecture in one line:** *Classes choose contextual meaning, schemas constrain it, methods name laws, mask/fold algebra performs eligible pure work, and OGAR alone admits effects.* From 6c2b73f47cad5dc72434733f1b217396e2d8cf18 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Mon, 12 Oct 2026 12:22:17 +0200 Subject: [PATCH 2/4] docs: specify typed logic algebra falsifiers and staged acceptance gates --- .../ALGEBRAIC-LOGIC-COMPILER-FALSIFICATION.md | 256 ++++++++++++++++++ 1 file changed, 256 insertions(+) create mode 100644 docs/ALGEBRAIC-LOGIC-COMPILER-FALSIFICATION.md diff --git a/docs/ALGEBRAIC-LOGIC-COMPILER-FALSIFICATION.md b/docs/ALGEBRAIC-LOGIC-COMPILER-FALSIFICATION.md new file mode 100644 index 0000000..3cf8c82 --- /dev/null +++ b/docs/ALGEBRAIC-LOGIC-COMPILER-FALSIFICATION.md @@ -0,0 +1,256 @@ +# D-TLAC falsification, parity, safety and migration plan + +**Date:** 2026-10-12. **Status:** RESEARCH PLAN, NO TESTS EXECUTED HERE. +**Parent proposal:** [Typed logic algebra compiler RFC](ALGEBRAIC-LOGIC-COMPILER-RFC.md). +**Scope:** OGAR method-as-object / semantic binder ↔ lance-graph R2IL-mask-risc ↔ rs-graph-llm/Rig ↔ OGAR hard DO gate ↔ IAM and HubSPO. No production actions. No source-bit reinterpretation. + +## 0. A conjecture becomes evidence only by surviving an oracle + +### Falsification discipline + +Each experiment must specify: +- **Claim:** one *particular* semantic/physical equivalence, not universal expressivity. +- **Oracle:** independent plain-loop, formal state transition, pinned ONA/Hyperon/PLN runtime or existing source-verified method. +- **Input surface:** class/field mapping, sort, population identity, snapshot generation, schema reading, null/evidence policy, auth scope. +- **Counterexample arm:** a known wrong implementation must fail (e.g. dropped Not, Sum where idempotent Max is required, duplicate evidential base, reused stale handle). +- **Measurements:** allocation bytes, decoded bytes, fold/scan counts, CPU/time when relevant, IO/ops, error identity, cardinality, replay results. Do not call absence of extra allocations "zero cost". +- **Kill condition:** stop this lowering when semantics differ, not merely improve performance until discrepancy is hidden. +- **Permission:** probes may not mint opcodes, persist CE64 meanings, change default ClassView interpretation, modify production IAM/HubSPO or execute remote commands. + +Required labels: [G] observed in current code; [P] proposed test not executed; [H] semantic hypothesis; [X] disproven. A passing fixture is evidence for the tested subset and versions only. + +### Independent oracles and controls + +| Subject | Semantic oracle | Material reference / control | +|---|---|---| +| Boolean mask & relation guards | plain scalar iteration plus SQL-style truth-table oracle | same rows/versions/keys, deterministic mask-risc byte program | +| Typed method binding | OGAR `Class/MethodDecl/ActionDef` roundtrip and symbol table | reject unbound class, wrong reading, duplicate method name+version | +| NARS | pinned literal Narsese implementation(s), ONA C tests and scalar truth formulas; use separate roots | per-case truth values, substitutions, evidential stamps, temporal implications | +| PLN | pinned modern PLN MeTTa rules/fixture interpreter | don't silently use NARS formula as PLN oracle | +| Hyperon/MeTTa | pinned Hyperon interpreter with native fixture and output multiplicity | explicit multiset of substitutions and error/unreduced cases | +| Phase transition | explicitly defined Heckhausen/Gollwitzer phase semantics; OGAR/kanban contract transition table for inner loop | never compare postaction phase to precommit Evaluation as though equal | +| Erlang `gen_statem` | bounded scripted OTP reference on isolated fixture (if available) | postpone/FIFO, entry, timeout and retry traces | +| IAM | dir-sim snapshot validator and policy oracle | no directory API mutation, source precedence/uniqueness and known tenant | +| HubSPO | H-ADR-7 persisted workflow and field/owner mask oracle | compare prior/next Lance version and mock executor receipt | + +Every pin needs repo commit SHA, toolchain, feature flags and fixture hash in the experimental report. Upstream license/runtime is an integration concern, **not** a reason to silently substitute a homemade oracle. + +## 1. Type and truth semantics to prove before compiling + +Proposed method sort skeleton (illustrative, not implemented): + +```text +RowMask +Truth +Epistemic +BindingsMultiset +Transition +ActionProposal +AuthorizedAction +``` + +**T1: Population and version:** AND/OR inputs must have the same universe, tenant and snapshot version, unless a typed join is explicitly performed. Stale plan handles fail closed, even when the raw number of rows coincides. + +**T2: Three-valued and open-world logic:** represent TRUE and FALSE as disjoint masks, UNKNOWN as neither (or two-bit known+value), and define truth tables explicitly. Kleene AND: + +```text +T(A∧B) = T(A) ∩ T(B) +F(A∧B) = F(A) ∪ F(B) +U(A∧B) = universe \ (T ∪ F) +NOT: T(¬A)=F(A); F(¬A)=T(A); U(¬A)=U(A) +SQL WHERE keeps T only; missing/unknown ≠ false +``` + +This shape is a candidate implementation over masks, not a proof that other epistemic logics use Kleene tables. Test \`UNKNOWN ∧ FALSE = FALSE\`, \`UNKNOWN ∧ TRUE = UNKNOWN\`, \`NOT UNKNOWN = UNKNOWN\`, and empty/all-null columns. Encode source absence separately from a false belief. + +**T3: Belnap/positive-negative evidence (optional):** if four-valued `{neither,true,false,both}` is requested, the two evidence-support masks are a typed product; their knowledge/truth order and conflict resolution cannot be inferred from a single TERNLOG immediate. Require a full independent 16-case binary operation table per operator before any rewrite. + +**T4: Quantifiers and multiplicity:** `Any/All` operate over a declared universe; universal over the empty set must use the declared mathematical/SQL convention. Distinctness, correlated joins, order and repeated bindings require separate typed witnesses. \`Count(mask)\` is not necessarily \`Count(bindings)\`. + +**T5: Algebra law metadata:** the compiler must reject invalid claims of associativity, commutativity and idempotence. A law certificate includes sort, version, overflow regime, null policy, evidence policy, and a reduced/optimized-vs-unoptimized oracle. Especially **Sum is not idempotent**, and floating regrouping is not byte-exact by default. + +## 2. Probe grid: semantic parity + +The following tests are **proposed**. Names specify their first intended case and a disable/kill arm. All entries remain unchecked until a run records full receipt. + +| ID | Construct and fixture | Oracle | Kill / disable guard | +|---|---|---|---| +| **TLAC-P01** | Three domain expressions with form \`A & !B & C\`: IAM active/unlicensed/evidenced, HubSPO active/unblocked/complete, Rubicon eligible/not-vetoed/gate-open; sparse/dense/empty/all masks, 1/63/64/65/256/257 rows | plain loop per domain + normalized mask-risc op graph | Make \`Not\` a no-op or swap field binder: at least one fixture **must** go red; plan graph shape may match while lane identity must remain distinct | +| **TLAC-P02** | Typed mismatches: foreign tenant, class, row universe, source generation, semantic ClassView reading, wrong-lane width | type-check refusal | If mismatched inputs produce a mask, fail; *equal row count* is not compatibility | +| **TLAC-P03** | Null/Unknown 3VL truth-table exhaustive 3×3 pairs and nullable field comparisons | Kleene/SQL scalar | Treat missing as false or \`NOT NULL\` as \`TRUE\`: red; if not, test is vacuous | +| **TLAC-P04** | `Any/All/Count/Keep` on zero rows and 1/64/65 selected, tail bits set | scalar quantifier oracle | Remove tail mask clearing / change empty ALL behavior: red | +| **TLAC-P05** | FK semijoin (gated `Gather` / `EqU32Via`) with repeated, missing and out-of-range IDs, forbidden field scope, 1%/50%/100% survivor masks | scalar FK resolution and owner/field policy | Force ungated gather or return false on authorized rows; semantics red for invalid FK; benchmark must also report read bytes | +| **TLAC-P06** | GroupCount/Sum/PowerSums/CrossPowerSums and \`BlendI32\` on mixed signs, bounds and nullable lanes; mutate group order | exact mathematical reference under current documented widths; scalar baseline | overflow silently wraps/saturates, combines finalized means or changes unsupported sort to scalar: red | +| **TLAC-P07** | NARS truth deduction/induction/abduction/revision with pinned f/c, disjoint stamps and delayed duplicate deliveries | scalar NARS/ONA fixtures | Remove stamp overlap check: doubled contribution changes result and **must** be rejected | +| **TLAC-P08** | CE64 statistical f/c and 59..63 epistemic reading, valid/invalid class reading, alternatives for bits 40..63 | explicit ClassView interpretation + bit-exact raw register | Remove reading gate, convert bytes as implicit semantic model, alter storage bits: red | +| **TLAC-P09** | Two mutually exclusive hypotheses over same node/row and sparse delta ordering; merge-on-read vs in-place revision | exact scalar rational / weighted accumulator + D-HL oracle | Under overlapping evidence, extra confidence or c=u8 stall must be visible; test must include a case where candidate differs from reference | +| **TLAC-P10** | Modern PLN rule and ONA NAL counterpart on same premises; vary formula and attention separately | pinned upstream independent engines | Any **unlabeled** difference in truth/confidence or ordering is a refusal, not harmonized "parity" | +| **TLAC-P11** | Hyperon \`(pair (bin) (bin))\` producing four solutions, repeated vars, nested outputs, empty and unreduced/Error | pinned MeTTa interpreter multiset | Two source rows collapsed into only two results instead of four: fail; only equal \`COUNT\` not sufficient | +| **TLAC-P12** | 4 action phases and two crossings: predecision goal-intention, preaction plan, OGAR guard/commit, postaction observed outcome | table state machine + event trace | Map existing inner \`Evaluation\` onto postaction without observed receipt: red | +| **TLAC-P13** | Erlang-style postpone, FIFO resume, timeout cancellation, entry effect and crash/retry against persisted virtual-state record | scripted OTP or formal reference traces | Reordering postponed events, running twice or missing timeout: fail; do not need BEAM in production | +| **TLAC-P14** | IAM identity conflict (duplicate UPN/SMTP normalized), HR source precedence, two tenants, 2nd source with stale membership, missing license | dir-sim and hard-policy oracle | NARS confidence overrides precedence/RBAC or produces a live write: fail | +| **TLAC-P15** | HubSPO team scope: direct membership, nested subteam, ADMINS nested but not subteam, sibling/parent groups, field mask; 10M logical population | `hubspo-iam::scope` and independent scalar owner oracle | Parent/sibling leaks; masked field reaches Rig output; actor/supervisor dependency appears: fail | +| **TLAC-P16** | Repeated action delivery, crash after external provider success before local receipt, crash before send, clock skew | idempotent mock API + outbox/reconcile protocol | Provider effect count ≠ 1 for logically same invocation; local version alone insufficient | +| **TLAC-P17** | Handle/session resumed at identical generation then republished source, old plan and old result | current `graph-flow-lance` stale-source tests | If stale handle executes/materializes on new generation, fail | +| **TLAC-P18** | Unauthorized field, wrong scope, adversarial model-generated tools, fabricated \`AuthorizedAction\` | OGAR `run_gated` mock executor call count + canary | Any denied/missing-field observation or external call before gate: fail | +| **TLAC-P19** | Goal/procedure learning: ONA suggests action, OGAR only builds proposal, blocked gate, observed expectation failure | ONA selected operation vs independent expected action and mock receipt | ONA callback reaches API before gate, or a failed postcondition treated as success: fail | +| **TLAC-P20** | Rewrites: unoptimized vs certified fused TERNLOG, mask survivor gating, effectful order preserved | bit-exact mask + deterministic action trace | Fusion changes truth rows, action order, source version or provenance: fail | + +### Anti-vacuity requirements + +- At least one non-empty, non-full mask per target scenario; at least one *differing* result under wrong source/tenant/field/null/unknown. +- Stamps must overlap and not overlap; if only disjoint stamps exist then removing overlap check cannot prove anything. +- One paired numeric dataset must cause intermediate u8 revision vs exact accumulation to differ by **at least 2 confidence/frequency codes** under the stated precision. +- Include cases with 2+ bindings for one atom and with four outcomes from a two-binary-slot product; otherwise Hyperon equivalence is untested. +- Independently vary inference rules vs schedulers; a model answering from cached prior evidence is an invalid run. +- An external mock must increment a counter **after** committing its own effect but **before** failure injection, to expose the crash-after-send window. + +## 3. Algebraic equivalence is not semantic equivalence + +Comparison levels (**do not skip**): + +1. **L0 shape**: same typed method signature, universe, version, authorization and ClassView reading. +2. **L1 pure algebra**: same normalized primitive call DAG under independent bound ids, not the same hard-coded lanes across domains. +3. **L2 value parity**: exact masks/scalars/typed result sets under independent oracle. For approximate numeric laws declare tolerance *in advance*. +4. **L3 provenance parity**: evidence independence/duplicate handling; no statistical laundering. +5. **L4 transition parity**: correct order, postponement, timeout, source version, goal/action/postaction distinction. +6. **L5 external effect parity**: authorization and exactly-once *logical* effect via idempotency/reconciliation. Not inferable from L1–L4. +7. **L6 runtime viability**: peak memory, row materializations, read bytes, time, parallel load, model tokens, number of folds. + +A library may pass L0–L2 and still **not** implement NARS/PLN, temporal planning or safe IAM. Report levels independently. + +### Minimal canonicalization test + +```text +Input 1: IAM.active AND NOT IAM.licensed AND IAM.independently_grounded +Input 2: CRM.active AND NOT CRM.blocked AND CRM.complete +Input 3: Rubicon.eligible AND NOT Rubicon.veto AND Rubicon.gate_open + +Normalization -> AND(AND(a, NOT(b)), c) or one equivalent 3-input truth table +Physical operations -> 3 predicates + bitwise combination + Keep +Bound sources: ALWAYS different classid, fields, tenant, generation and auth. +Test equality of normalized *op shapes*, not equality of bound Program bytes. +``` + +Negative case: under a NULL-aware source, `NOT missing` remains UNKNOWN. Without known/validity masks, a seemingly equivalent Boolean plan must be rejected or explicitly lowered with the extra validity mask; otherwise the compiler changes semantics. + +## 4. NARS/CE64 and causal epistemology matrix + +| Concern | Separate representation | Required test | +|---|---|---| +| Observed frequency | NARS f/statistical frequency | scalar truth oracle; never call this causal probability | +| Evidence confidence | NARS c/statistical weight, `Σw` accumulator | duplicate/overlap stamps and round-once bounds | +| Epistemic status | declared CE64 reading in bits 59..63 | direct vs indirect, intermediate known/unknown, class version | +| Correlation vs causation | explicit CARE/Pearl/counterfactual interpretation | ablation/intervention fixture; observational association alone not promoted | +| Hypothesis concurrency | Alpha sparse delta overlays, versions, 64 layers **design** | layer isolation and merge-on-read vs 10 existing rung lanes; no hidden persisted-bit decision | +| Change of belief | explicit revise/suspend/refuse verdict | no reweight without new independent root | +| Attention policy | FIFO/confidence, Shannon, EIG, Moore/Staunen | equal rule set/evidence budget/CPU & decode bytes | +| Goal/action | ONA goal/procedure suggestion | action proposal, gate separation and observed outcome | + +Crucial numerical bound: group moments with a weighted f are safe only under the chosen integer width, bounded rows and signedness. If a missing primitive is required to write computed per-row truth values, first prove a *typed lane-producing* insufficiency against the already available `BlendI32` and the R2IL procedure path; add the smallest generic primitive only after that proof. + +## 5. Rubicon and external DO acceptance contract + +The proposed outer state table is **not** the existing Kanban enum: + +| Outer phase | Input | Output | Mandatory constraint | +|---|---|---|---| +| Deliberation | candidate goals/hypotheses | chosen goal intention, alternatives rejected | evidence/provenance preserved | +| Preaction | goal + contextual if/then | plan, applicable `ActionDef`, deadlines/witness | fixed authority and environment preconditions | +| Action | approved invocation | executor receipt + next observed version | `commit_via`; idempotent external effect | +| Postaction | expected vs observed | satisfaction/feedback, revise/continue/escalate | do not treat successful API call as proven goal outcome | + +The inner cycle remains `Planning→CognitiveWork→Evaluation→{Commit,Plan,Prune}`; its \`Evaluation\` happens before accepting/persisting candidate cognitive result, whereas outer postaction evaluates a realized action. Provide two separate typed state components, or a demonstrated lossless projection before merging their types. + +**Fault injection timeline:** + +```text +T0 source v read / private logical invocation id built +T1 goal proposed and plan generation pinned +T2 action guard/RBAC/current-generation check +T3 outbox prepared (idempotency key and requested effect) +T4 provider mutates (inject crash BEFORE receipt is saved) +T5 replay with same key checks provider receipt before resend +T6 observe source version v+1; postcondition may still fail +T7 append evidential witness without reusing an old stamp as new support +``` + +At T4→T5, neither an isolated Lance append nor a claimed "exactly once" local queue suffices. A real integration must have idempotent provider behavior or an explicit reconciliation protocol. + +### IAM simulation fixture + +- Users with valid and conflicting UPN/mail/proxy-address; normalize for comparisons without changing canonical GUID. +- HR source A vs source B ordered by an explicitly declared authority/date rule, plus recently changed account. +- Missing Entra license, delayed provisioning, wrong group membership, and a false-positive NARS proposal. +- Approver lacking required role, absent tenant grant, stale directory generation, and a second concurrent reconciliation. +- Expected: deterministic plan shows diffs, does no production write, refuses duplicates; NARS can rank investigations but never override authority/uniqueness/grants. + +### HubSPO scope and CRM fixture + +- Owned record vs team-owned vs global; direct team group vs nested subteam vs non-team AD group; sibling/parent excluded. +- Company/deal stage guard and required properties, plus NULL fields, workflow resume_at and published version offset. +- Field-level sensitive property withheld from export before a model sees it. +- Expected: Quack mask equals independent scalar authorized owner set. Workflow state and due run in Lance rows; no ractor dependencies, actor mailboxes or new timers. + +## 6. Performance and memory: report facts, don't predict speed + +Report by row count `n ∈ {0,1,63,64,65,256,257,4096,1_000_000,10_000_000}` (if feasible) and mask selectivity `p ∈ {0,0.001,0.01,0.5,1}`. For each oracle-matching program measure: + +- cold/warm wall time (median and dispersion), CPU time, number of physical fold programs/terminals, decoded bytes, bytes read from Lance and scratch peak; +- allocated bytes per invocation and peak heap, particularly **no row-sized intermediate** in the method stack; +- output count, truth values and error/refusal case, exact stale handle behavior; +- idempotent replay counts and external API call count (mock); +- when Rig participates, materialized export bytes/tokens and whether denied fields appear. + +Compare independent arms: + +- scalar reference vs mask-risc compiled method; +- specialized hand-written current guard vs generic typed compiler; +- fused ternlog vs ordinary mask ops vs survivor-gated condition; +- current R2IL procedure vs proposed method-linked procedure; +- persistent row workflow vs materialized actor reference *only in isolated benchmark*, not as HubSPO dependency; +- NARS identical inference engine with FIFO/confidence/Shannon/EIG/Moore scheduling; then identical scheduler with NARS vs PLN where semantics allow. + +**KILL on overhead without expressivity:** if generic typed dispatch adds meaningful hot path allocations, row copies, extra folds, or serializes/allocates row-sized values, do not promote; fix the binder/offline compilation or stop. Never claim a wall-time target that was not benchmarked. + +**KILL on useless optimization:** identical semantic outcomes with increased code/bytes/complexity and no measured improvement in CPU, IO, memory, or maintainability => keep the simple existing procedure. + +## 7. Implementation waves / ownership / no-go checkpoints + +| Wave | Code owner | Deliverable (only after preceding gate) | Stop test | +|---|---|---|---| +| **W0** | OGAR docs | this RFC, this falsification plan, discovery-map pointer | docs don't alter runtime or ABI | +| **W1** | lance-graph test consumer + OGAR declarations | pure canonical 3-guard declaration and binder, no new opcode | P01–P06, P20 and disabled guards | +| **W2** | OGAR `ogar-loco` / vocabulary inventory | function-as-object identity + body-ref resolution under canonical classid | missing/stale/duplicate function refuses; W1 parity unchanged | +| **W3** | lance-graph CE64/NAL + OGAR reading | candidate stamped revision, exact truth and epistemic mask | P07–P11, no persisted bit meanings change | +| **W4** | rs-graph-llm | typed outer phase context, inner Kanban preserved; graph-flow-lance stable plan/session handle | P12, P13, P17 | +| **W5** | OGAR + IAM / HubSPO + rs-graph-llm | mock-only stable DO plan → gate → outbox receipt → observation → revision | P14–P19; forbidden dependency guards stay green | +| **W6** | only measured deficient primitive owner | smallest new typed lane operator/sort or refused subset | fail-before/green-after with oracle, ABI migration and version gate | + +**Shared rule:** no producer-to-DDL behavioral lowering; no AI callback executing commands; no actor-per-object dependency in HubSPO; no cross-repo change without its own review/contract parity. Existing classids and method ordinals are retrieved, not re-minted. Newly proposed IDs require a separate minting decision. + +### Open exact decisions + +- Which class reading/version defines CE64 and which bit fields are currently blocked under D-HL? +- What data model represents evidential source identity and exclusion of stamp overlap, even when all row keys match? +- Can `MethodDecl` remain source AST while Inventory carries linked typed executable bodies, avoiding a new canonical field? +- What method-result sorts need new type-level representation, versus new machine operations? +- Which outer phase and Intent/ImplementationIntention type attaches to `graph-flow`? How are action goal targets and postaction observations versioned? +- What is the exact stable invocation identity and provider receipt contract on durable restart? +- How are law certificates verified/invalidated if the ClassView/field schema evolves? +- Can the zero-row and typed unknown cases be represented without new bool semantics in the global ISA? + +## 8. PR review checklist + +- [x] **Design only**: no files outside documentation are required by this plan. +- [x] Current code and explicit "Not built" gaps linked without treating plans as implementations. +- [x] No new opcode/semantic bits or automatic action authorization proposed. +- [x] Semantic mismatch, provenance, null/unknown, temporal and effects explicitly separated. +- [x] P01–P20 with independent oracles, error expectations and negative/disable controls specified. +- [ ] No tests claimed executed; executable probes not yet implemented. +- [ ] No performance parity claimed; benchmarks deferred to wave-specific PRs. +- [ ] Upstream ONA/PLN/Hyperon runtime versions and licenses pinned at test implementation. +- [ ] Security review of plan and external API receipt semantics before any real IAM/CRM mutation. +- [ ] Explicit operator decision on optional new types/bytes/generic primitives. + +**Conclusion:** a single *physical* masking and fold executor can host many *typed* logic families if the compiler preserves the family-specific laws and refuses all unsupported semantics. The test above determines the subset, not the architectural slogan. From 0e4aa9c7360bc321db82157ff00dda36dd1130ca Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Mon, 12 Oct 2026 12:23:05 +0200 Subject: [PATCH 3/4] docs: index typed logic algebra hypothesis with graded status --- docs/DISCOVERY-MAP.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/DISCOVERY-MAP.md b/docs/DISCOVERY-MAP.md index 7df82b9..ce98ae4 100644 --- a/docs/DISCOVERY-MAP.md +++ b/docs/DISCOVERY-MAP.md @@ -2265,3 +2265,5 @@ isolation. The map's job is to keep them visible. population is DETECTABLE via a poison flag, never ABORTABLE. Making it a true refusal needs `truthy -> Result` in `ogar-loco` — its own PR, its own blast radius, named here rather than done quietly. + +- **[D-TLAC-0] one *typed* logic-method compiler over existing mask/fold primitives, not four execution engines — OGAR Class/MethodDecl/Schema/ClassView → R2IL/mask-risc/ndarray; NARS/CE64, Rubicon/GoalIntention, OGIT DO arm, IAM and HubSPO are semantically distinct readings — [H] — EPIPHANY (2026-10-12, docs-only, no parity run) — [RFC](ALGEBRAIC-LOGIC-COMPILER-RFC.md), [falsifier matrix TLAC-P01..P20](ALGEBRAIC-LOGIC-COMPILER-FALSIFICATION.md) — depends [OGAR-AS-IR](OGAR-AS-IR.md), [LOCO-ORCHESTRATION-GAP](LOCO-ORCHESTRATION-GAP.md), [HIRO DO](HIRO-DO-ARM-LIFT.md), lance-graph #1496 (merged research plans), #1497/#1498 (draft research maps), rs-graph-llm graph-flow-lance/graph-flow-action-ogar, HubSPO H-ADR-7. **Floor:** 8-bit ISA remains semantic-free; no new byte, bit, classid, runtime or effect authority. **First falsifier:** three independently typed Boolean guard methods normalize to one operator shape without sharing row universe; overlapping evidence and an unauthorized DO action MUST refuse. No tests claimed executed. From fe704a0b064f3725aaf92092e8b860c2daf02fe4 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Mon, 12 Oct 2026 12:23:08 +0200 Subject: [PATCH 4/4] docs: link typed logic compiler proposal from design guards --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index f253276..064d2ce 100644 --- a/README.md +++ b/README.md @@ -85,6 +85,7 @@ Until it ships, keep existing auth — do NOT re-introduce a `*Bridge` as a stop | Guard | Read before | |---|---| +| [Typed logic compiler RFC](docs/ALGEBRAIC-LOGIC-COMPILER-RFC.md) + [falsification plan](docs/ALGEBRAIC-LOGIC-COMPILER-FALSIFICATION.md) | proposing a typed logic/method/scheme lowering over R2IL and mask-risc; documentation-only, no new runtime or ISA | | [OGAR as IR](docs/OGAR-AS-IR.md) | designing any IR addition (a new `Class` field, `ActionDef` variant, `KausalSpec` slot, lowering pass) | | [Consumer best practices](docs/OGAR-CONSUMER-BEST-PRACTICES.md) | any consumer call site (classid · `APP_PREFIX` · `ClassView` · `*Bridge`) | | [SurrealQL-AST trap pre-flight](docs/SURREAL-AST-TRAP-PREFLIGHT.md) | producer→IR · transcode · codegen · `.surql` authoring |