Add M1 design documents: law script + API shapes (3 designs, recommend B)

- M1 law script format decision doc recommends S-expressions with fixed
  combinators for non-Turing provability, auditability, and immutability
  at runtime (S99). Includes example constitution with all L1-L5 invariants.

- M1 trader-wallet-marketplace API designs: compare 3 radically different
  shapes (minimal tokens, event-sourced ledger, GraphQL). Recommend Design B
  (ledger) for auditability, replay capability, and SAE integration.

- Ada config: core_config.gpr with GNAT 2022 compiler flags.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
Claude
2026-07-19 02:10:13 +00:00
parent eefdb2fb5f
commit 0f46e134fa
3 changed files with 1729 additions and 0 deletions
+28
View File
@@ -0,0 +1,28 @@
abstract project Core_Config is
for Source_Dirs use ();
type Yes_No_Type is ("yes", "no");
type Library_Type_Type is ("relocatable", "static", "static-pic");
Library_Type : Library_Type_Type := external ("CORE_LIBRARY_TYPE", "static");
Static_Build : Yes_No_Type := external ("CORE_STATIC_BUILD", "yes");
package Compiler is
for Default_Switches ("Ada") use
("-gnat2022",
"-gnatwa",
"-gnatwe",
"-gnatyyM",
"-gnaty3abcdefhijklmnoprstux",
"-Wall",
"-O2",
"-gnatf",
"-gnatpn");
end Compiler;
package Binder is
for Default_Switches ("Ada") use ("-Es");
end Binder;
end Core_Config;
File diff suppressed because it is too large Load Diff
+443
View File
@@ -0,0 +1,443 @@
# M1 Marketplace — Deterministic Law Script Format Decision Document
## Executive Summary
The M1 Marketplace's law script is a **constitution**: deterministic, auditable, non-Turing, loaded at startup, immutable at runtime (L2). This document compares three candidate formats for expressing M1's scoped invariants (L1–L5), position limits, drawdown stops, action allowlists, wallet-binding requirements, and chain allowlists. We recommend **S-expressions with a fixed combinator set** for its optimal balance of expressiveness, auditability, non-Turing guarantees, and failure-mode isolation.
---
## 1. Candidate Formats
### 1.1 Format A: Declarative Rule Table (YAML/TOML-style records)
**Structure:**
```yaml
rules:
- id: "rule_001"
name: "Max BTC position"
condition:
asset: "BTC"
action_type: "buy"
constraint: { position_limit: 10.0 }
- id: "rule_002"
name: "Unauthorized chains blocked"
condition:
action_type: "*"
constraint:
chain_allowlist: ["ethereum", "solana"]
```
**Expressiveness:**
- ✅ Naturally expresses static constraints (position limits, allowlists, drawdown stops).
- ⚠️ Awkward for conditional logic (e.g., "if position > X, then drawdown stop"). Requires deep nesting or external evaluation logic.
- ⚠️ Difficult to express negation, conjunction, or disjunction across multiple fields without ad-hoc extensions.
**Auditability:**
- ✅ Human-readable; rules are self-documenting.
- ✅ Schema validation possible (e.g., JSON Schema, OpenAPI).
- ⚠️ No built-in way to trace evaluation: which rules matched? In what order? Why did law_check pass or fail?
**Non-Turing Guarantee:**
- ✅ Structure is inherently acyclic (no loops, recursion, or branching).
- ⚠️ Depends on implementation: evaluator must be guaranteed to iterate once per rule, no internal loops.
- ⚠️ If evaluator uses external functions (e.g., "call_oracle"), non-Turing status is lost.
**Failure Modes:**
- **Silent mismatches:** A typo in a field name (e.g., `chain_alowlist`) silently skips the rule.
- **Ambiguous precedence:** If multiple rules match, which one applies? YAML provides no ordering semantics.
- **Extension creep:** New logic (e.g., time-based rules, cross-asset constraints) requires schema mutations.
---
### 1.2 Format B: S-expressions with Fixed Combinator Set
**Structure:**
```scheme
(law
(id "rule_001")
(name "Max BTC position")
(check (lambda (action trader wallet)
(and
(eq (asset action) "BTC")
(eq (action-type action) "buy")
(< (position trader "BTC") 10.0)))))
(law
(id "rule_002")
(name "Chain allowlist")
(check (lambda (action trader wallet)
(member (chain action) (list "ethereum" "solana")))))
```
**Expressiveness:**
- ✅ Combinator set (`and`, `or`, `not`, `<`, `>`, `member`, `eq`, etc.) is Turing-incomplete by construction.
- ✅ Natural for predicates, constraints, and conditional logic.
- ✅ Extensible via new combinators (e.g., add `ratio-check` for drawdown).
- ✅ Composable: build complex rules from simple primitives.
- ⚠️ Steep learning curve for non-programmers (COBOL-familiar operators may resist).
**Auditability:**
- ✅ Each rule is a pure function: input (action, trader, wallet) → output (pass/fail).
- ✅ Trace semantics are built-in: can log each combinator call, build proof trees.
- ✅ Debuggable: step through symbolic execution.
- ✅ Self-documenting via lambda structure.
**Non-Turing Guarantee:**
- ✅ Combinator set is closed; only allowed operations are enumerated (no `while`, `recurse`, `call-external`).
- ✅ Depth bound: lambda nesting is bounded by law complexity; evaluator can enforce max depth.
- ✅ Time bound: each combinator has known cost; evaluator can enforce max steps.
- ✅ Provably non-Turing if combinator set excludes recursion and cycles.
**Failure Modes:**
- **Syntax errors:** Malformed S-expressions fail at parse time; no silent skips.
- **Undefined combinator:** If a rule uses `(frobnicate ...)`, parser rejects it immediately.
- **Type mismatches:** If a rule tries `(< action "ethereum")` (comparing struct to string), evaluator fails gracefully.
- **Depth/step limits:** If a law is too complex, evaluator flags it at load time, not at runtime.
---
### 1.3 Format C: Decision-Table (Matrix Format)
**Structure:**
```
| Rule ID | Asset | Action | Position Limit | Chain Allowlist | Drawdown Stop | Outcome |
|---------|-------|--------|-----------------|-----------------|---------------|---------|
| R_001 | BTC | buy | < 10 | ethereum,solana | n/a | PASS |
| R_001 | BTC | buy | >= 10 | ethereum,solana | n/a | FAIL |
| R_002 | * | * | n/a | ethereum,solana | n/a | PASS if chain in list |
| R_003 | ETH | sell | n/a | ethereum,solana | < 20% loss | PASS |
```
**Expressiveness:**
- ✅ Intuitive for auditors: each row is a rule, each column is a fact or constraint.
- ⚠️ Difficult to express complex logic (e.g., "if position > X AND wallet binding missing, fail"). Requires cartesian product of rows.
- ⚠️ Scaling: N conditions × M values = O(N×M) rows; easily becomes unwieldy.
- ✅ Good for classification / risk matrices.
**Auditability:**
- ✅ Highly visual: auditor can scan rows and see all rules at once.
- ✅ Compliance-friendly: decision tables are used in regulated industries (banking, insurance).
- ⚠️ Redundancy: same constraint repeated across many rows; easy to introduce inconsistencies.
- ⚠️ No inherent proof structure: why did a row match? Requires external tracing.
**Non-Turing Guarantee:**
- ✅ Table is finite; no loops or recursion by structure.
- ⚠️ Depends on "Outcome" cell: if it can call arbitrary functions, non-Turing is lost.
- ⚠️ Row matching logic must be deterministic and acyclic.
**Failure Modes:**
- **Row ordering ambiguity:** If multiple rows match, which takes precedence? Table format doesn't specify.
- **Incomplete coverage:** If no row matches, what happens? Default to PASS or FAIL?
- **Maintenance complexity:** Adding a new constraint requires rebuilding the entire table (cartesian product).
- **Hidden correlations:** Hard to see relationships between rules (e.g., "R_001 always paired with R_003").
---
## 2. Comparative Analysis
| Criterion | A (Declarative) | B (S-expr) | C (Decision-table) |
|-----------|-----------------|------------|-------------------|
| **Expressiveness** | ⭐⭐ (static constraints) | ⭐⭐⭐⭐⭐ (composable predicates) | ⭐⭐⭐ (classification) |
| **Auditability** | ⭐⭐⭐ (readable, schema-valid) | ⭐⭐⭐⭐⭐ (proof trees, trace logs) | ⭐⭐⭐⭐ (visual, tabular) |
| **Non-Turing guarantee** | ⭐⭐⭐ (structural, not airtight) | ⭐⭐⭐⭐⭐ (provable, combinator-closed) | ⭐⭐⭐ (structural) |
| **Extensibility** | ⭐⭐ (schema mutation) | ⭐⭐⭐⭐ (add combinators) | ⭐ (cartesian explosion) |
| **Human readability** | ⭐⭐⭐⭐ | ⭐⭐⭐ (for programmers) | ⭐⭐⭐⭐ |
| **Failure-mode isolation** | ⭐⭐ (silent mismatches) | ⭐⭐⭐⭐⭐ (fail-fast parsing) | ⭐⭐⭐ (depends on semantics) |
---
## 3. Recommendation: S-expressions with Fixed Combinator Set
**We recommend Format B** for the following reasons:
1. **Non-Turing Provability (L2 requirement):** S-expressions with a closed combinator set are provably non-Turing. The Marketplace can enumerate all allowed operations at startup, verify no cycles or unbounded loops, and enforce step/depth limits at evaluation time. This is unmatched by Formats A and C.
2. **Auditability & Traceability:** Each law is a pure function with explicit inputs and outputs. The evaluator can build a **proof tree** showing which combinators matched, in what order, and why `law_check` passed or failed. Auditors can step through the logic symbolically. Formats A and C lack this transparency.
3. **Failure-Mode Isolation:** Parse-time and load-time failures catch errors immediately. A malformed law (undefined combinator, type mismatch, depth exceeded) fails hard at startup—no silent skips, no runtime surprises. This mirrors the COBOL vault invariant (S3 / S99).
4. **Extensibility without Mutation:** New constraints (drawdown ratio checks, wallet-binding logic, time-based rules) are added as new combinators, not schema mutations. The core evaluator remains stable.
5. **Compatibility with L3-L5:**
- **L3 (no wallet, no access):** Combinator `(wallet-bound? wallet)` is a primitive.
- **L4 (veto after law, before execution):** Combinator set does not include veto logic; law_check is orthogonal to veto_check.
- **L5 (logging):** Evaluator logs each law invocation and result; combinators are traceable.
6. **Operator + Homunculus Signatures (L2):** The S-expression law script is a single immutable text blob, signed at startup. Easier to sign and verify than YAML (schema-dependent serialization) or decision tables (multi-row format).
---
## 4. Fixed Combinator Set
The law script evaluator provides a **closed set** of combinators. No new combinators are added at runtime; changes to the combinator set require a restart with new signatures.
### Core Combinators
**Logical:**
- `(and expr1 expr2 ...)` — conjunction (short-circuits on false).
- `(or expr1 expr2 ...)` — disjunction (short-circuits on true).
- `(not expr)` — negation.
**Comparison:**
- `(eq x y)`, `(ne x y)` — equality / inequality.
- `(< x y)`, `(> x y)`, `(<= x y)`, `(>= x y)` — numeric comparison.
**Membership:**
- `(member item (list ...))` — item in list? Returns true/false.
- `(in-range value min max)` — value in [min, max)?
**Predicates on Action/Trader/Wallet:**
- `(asset-is action symbol)` — asset == symbol.
- `(action-type-is action type)` — action type (buy, sell, mint, etc.).
- `(position-limit trader asset limit)` — trader's position in asset < limit.
- `(drawdown-limit trader asset percent)` — realized drawdown < percent.
- `(chain-is action chain)` — blockchain == chain.
- `(wallet-bound wallet)` — wallet is non-null.
- `(wallet-approved wallet trader)` — wallet is approved for this trader (from M4 binding).
- `(status-is trader status)` — trader status (active, suspended, etc.).
**Arithmetic (safe):**
- `(+ x y)`, `(- x y)`, `(* x y)`, `(/ x y)` — bounded arithmetic (saturation on overflow).
**Control (non-Turing):**
- `(cond (test1 result1) (test2 result2) ...)` — if-then-else (no loops).
- `(comment "text" expr)` — documentation; evaluates expr, returns result.
### Forbidden Operations
- `(loop ...)`, `(while ...)`, `(recurse ...)` — unbounded iteration.
- `(call-external ...)`, `(invoke-oracle ...)` — non-deterministic side effects.
- `(eval ...)`, `(quote ...)` — metaprogramming.
---
## 5. Example Marketplace Constitution (M1-v1)
```scheme
;;; M1 Marketplace — Deterministic Law Script v1
;;; Loaded at startup; immutable at runtime (M1-L2).
;;; Operator & Homunculus signatures below.
;;; ============================================================
;;; HEADER: Version, Signatures, Metadata
;;; ============================================================
(constitution
(version "1.0")
(effective-date "2026-07-19T00:00:00Z")
(operator-signature "0x1234...abcd") ; Operator's Ed25519 signature
(homunculus-signature "0x5678...efgh") ; Homunculus's Ed25519 signature
(description "M1 Marketplace law script v1: enforces L1-L5 invariants, position limits, chain allowlists.")
)
;;; ============================================================
;;; L1: All market actions route through Marketplace
;;; (Implicit: law_check is the only gate. No on-chain bypass possible.)
;;; ============================================================
;;; ============================================================
;;; L3: No wallet, no access
;;; ============================================================
(law
(id "L3-wallet-binding")
(name "Trader must have bound wallet")
(description "L3 invariant: a trader without a bound wallet cannot submit actions.")
(check (lambda (action trader wallet)
(wallet-bound wallet))))
;;; ============================================================
;;; L4: Veto is checked after law, before execution
;;; (Implicit: law_check runs first, then veto_check. No veto in law script.)
;;; ============================================================
;;; ============================================================
;;; L5: Every action is logged
;;; (Implicit: evaluator logs all law_check invocations, pass or fail.)
;;; ============================================================
;;; ============================================================
;;; Position Limits (per-asset, per-trader)
;;; ============================================================
(law
(id "LIMIT-BTC")
(name "BTC position limit")
(description "No single trader may hold > 10 BTC.")
(check (lambda (action trader wallet)
(or
(not (asset-is action "BTC"))
(position-limit trader "BTC" 10.0)))))
(law
(id "LIMIT-ETH")
(name "ETH position limit")
(description "No single trader may hold > 100 ETH.")
(check (lambda (action trader wallet)
(or
(not (asset-is action "ETH"))
(position-limit trader "ETH" 100.0)))))
(law
(id "LIMIT-USDC")
(name "USDC position limit")
(description "No single trader may hold > 1M USDC.")
(check (lambda (action trader wallet)
(or
(not (asset-is action "USDC"))
(position-limit trader "USDC" 1000000.0)))))
;;; ============================================================
;;; Drawdown Stops
;;; ============================================================
(law
(id "STOP-20pct-drawdown")
(name "Drawdown stop at 20%")
(description "If a trader's realized drawdown exceeds 20%, no further sells (or limit actions) until reset.")
(check (lambda (action trader wallet)
(or
(not (action-type-is action "sell"))
(drawdown-limit trader "all" 20.0)))))
;;; ============================================================
;;; Action Allowlists: Only buy, sell, mint, provide_liquidity, withdraw, claim_rewards
;;; ============================================================
(law
(id "ACTION-allowlist")
(name "Only allowed action types")
(description "Marketplace only accepts: buy, sell, mint, provide_liquidity, withdraw_liquidity, claim_rewards.")
(check (lambda (action trader wallet)
(member (action-type action)
(list "buy" "sell" "mint" "provide_liquidity" "withdraw_liquidity" "claim_rewards")))))
;;; ============================================================
;;; Chain Allowlist: ethereum, solana, arbitrum
;;; ============================================================
(law
(id "CHAIN-allowlist")
(name "Supported chains only")
(description "Actions are allowed only on ethereum, solana, or arbitrum.")
(check (lambda (action trader wallet)
(member (chain action)
(list "ethereum" "solana" "arbitrum")))))
;;; ============================================================
;;; Wallet Approval: Wallet must be approved for this trader
;;; ============================================================
(law
(id "WALLET-approval")
(name "Wallet must be approved for trader")
(description "The bound wallet must be explicitly approved for this trader by M4.")
(check (lambda (action trader wallet)
(wallet-approved wallet trader))))
;;; ============================================================
;;; Trader Status: Only active traders can submit actions
;;; ============================================================
(law
(id "TRADER-status")
(name "Trader must be active")
(description "Only traders with status 'active' can submit actions. Suspended or banned traders are rejected.")
(check (lambda (action trader wallet)
(status-is trader "active"))))
;;; ============================================================
;;; End of Constitution
;;; ============================================================
```
---
## 6. Evaluation & Versioning
### Law Script Loading (Startup)
1. **Parse:** S-expression parser validates syntax. Reject if malformed.
2. **Verify Signatures:** Extract operator + Homunculus signatures; verify with Ed25519 public keys. Reject if invalid.
3. **Validate Combinators:** Scan all `(lambda ...)` expressions; ensure only allowed combinators are used. Reject if undefined combinator found.
4. **Enforce Depth Limits:** Check that lambda nesting depth < 20 (configurable). Reject if exceeded.
5. **Load into Memory:** Store law script as immutable bytecode. Set flag: law script is loaded and locked.
### Law Check Execution
```
law_check(action: MarketAction) -> { pass | violation(rule_id, reason) }
```
1. Iterate over all laws (in order of definition).
2. For each law, invoke `(check action trader wallet)`.
3. If lambda returns **false**, record violation(rule_id, reason) and stop.
4. If all laws return **true**, return pass.
5. Log every invocation: rule_id, inputs, output, timestamp.
### Versioning & Updates
- **Current Version:** `"1.0"` (loaded at startup).
- **Update Process:** Operator + Homunculus jointly author a new law script (version `"1.1"`), sign it, submit to Marketplace coordinator.
- **Activation:** Coordinator restarts Marketplace with new law script; old version is abandoned. (No in-flight migration; trades-in-progress must complete or be canceled.)
- **Audit Trail:** Every law script version is archived with signatures, timestamp, and change log.
---
## 7. Failure Modes & Mitigation
### Parse Failure
- **Mode:** Malformed S-expression (unmatched parens, undefined combinator).
- **Mitigation:** Fail at startup; operator is alerted; Marketplace does not boot. Prevents silent corruption.
### Signature Mismatch
- **Mode:** Law script is edited after signing (operator or Homunculus signature invalid).
- **Mitigation:** Fail at startup; abort boot. Ensures L2 immutability.
### Combinator Overflow
- **Mode:** Lambda nesting depth or step count exceeded (accidentally or maliciously complex law).
- **Mitigation:** Reject at load time if depth > limit; reject at runtime if steps > limit. Ensures termination.
### Silent Falses
- **Mode:** A law returns false due to unforeseen input (e.g., null asset).
- **Mitigation:** Combinator set includes explicit nil-checks (e.g., `(asset-is action "NULL")` returns false, not an error). Evaluator logs the false + reason.
### Type Mismatches
- **Mode:** Lambda tries to compare incompatible types (e.g., `(< "BTC" 10.0)`).
- **Mitigation:** Type-check at parse time or runtime. Reject with clear error. No silent type coercion.
---
## 8. Rationale for S-expressions
1. **Provable Non-Turing:** Closed combinator set with explicit enumeration. No ambiguity.
2. **Audit Trail:** Proof trees show exactly which laws matched, in what order. Compliance-ready.
3. **Fail-Fast Design:** Parse-time and load-time validation catch errors before runtime. Mirrors S99 / vault pattern.
4. **Composability:** Complex rules built from simple primitives. Easy to extend without schema mutations.
5. **Testability:** Each combinator is independently testable. Laws are pure functions.
6. **Operator + Homunculus Signatures:** Single immutable law text is signed; no serialization ambiguity.
---
## 9. Transition Path
1. **Phase 1 (Sprint N):** Implement S-expression parser + combinator evaluator. Write unit tests for all combinators.
2. **Phase 2 (Sprint N+1):** Wire M1 `law_check` to S-expression evaluator. Test with example constitution (above).
3. **Phase 3 (Sprint N+2):** Integrate M4 (wallet binding), M6 (veto), M7 (logging). End-to-end smoke test.
4. **Phase 4 (Sprint N+3):** Operator + Homunculus review; sign v1 law script. Deploy to production.
---
## 10. Open Questions for Review
1. **Combinator Set Completeness:** Are there missing combinators for L1-L5 or position logic?
2. **Step/Depth Limits:** What are safe upper bounds? (Suggest: max_depth=20, max_steps=1000.)
3. **Error Messages:** How granular should violation reasons be? (E.g., "position_limit_exceeded_BTC_5.2_of_10.0" vs. "position_limit_exceeded"?)
4. **Signature Algorithm:** Ed25519, ECDSA, or other? (Recommend: Ed25519, matching COBOL vault.)
5. **Tax Collection (M0):** Where does tax logic live—in M1 law script or in a separate M0 component? (Out of scope here; M1 calls tax stub.)
---
## Conclusion
**S-expressions with a fixed combinator set** provide the optimal combination of expressiveness, auditability, non-Turing provability, and failure-mode isolation for M1's deterministic law script. The format aligns with the COBOL vault pattern (S99 / immutability + dual signatures), scales naturally with new constraints, and enables full audit trails for compliance.