docs(proofline): approve line 0009 specification

.proofline/criteria/ac-0026.md

@@ -0,0 +1,18 @@
+---
+id: "ac-0026"
+status: active
+---
+
+# Slot occupancy와 독립된 strategy state lifecycle
+
+## Criterion
+
+`trex-core`는 슬롯의 strategy-state map과 각 entry를 slot occupancy lifecycle과 독립적으로 보존해야 한다. Slot이 어떤 경로로든 `INACTIVE`가 되어도 일반 lifecycle transition은 strategy state를 삭제하지 않아야 하며, inactive 상태와 이후 재점유 상태에서 저장된 entry와 version을 다시 읽을 수 있어야 한다. 재점유 뒤 같은 entry에 성공한 write는 close 전 version에 이어서 증가해야 한다. Strategy-state persistence schema, application model, store protocol, read filtering, `strategy_state.set` request/response 및 state CAS에는 `occupancy_seq`나 `expected_occupancy_seq`가 없어야 하며, occupancy 변경만으로 state를 숨기거나 write를 `occupancy_changed`로 거부해서는 안 된다. Slot 자체의 `occupancy_seq`, active-slot write gate, opaque data size limit, slot transition의 나머지 원자성과 별도 파괴적 전체 DB reset은 변경하지 않는다.
+
+## Verification
+
+- 보존 조건: active slot의 instance entry를 version 1 이상으로 저장한 뒤 전략 매도, safety-sell, forced-close 및 operator close를 포함한 각 `→ INACTIVE` 경로를 실행해도 저장소 entry와 version이 삭제되지 않는다. Inactive slot 조회와 이후 재점유 조회에서 같은 data·version이 보이고, 재점유 뒤 기존 version을 `expected_version`으로 사용한 성공 write가 version을 1 증가시킨다.
+- 격리 조건: 한 slot의 lifecycle transition이 해당 slot map의 일부 또는 전체 entry를 삭제하거나 다른 slot의 state를 변경하면 FAIL이다. Close-delete hook 제거 전후로 slot update, transition log, broker·ledger side effect와 transition failure 원자성이 기존 계약에서 달라지지 않아야 한다.
+- Occupancy 분리 조건: strategy-state migration/schema, dataclass, in-memory/PostgreSQL store contract, read path와 write RPC payload/response에 `occupancy_seq` 또는 `expected_occupancy_seq`가 남거나, occupancy mismatch read filtering 또는 `occupancy_changed` reject path가 실행되면 FAIL이다. Slot domain의 자체 `occupancy_seq`와 증가 규칙은 그대로 유지되어야 한다.
+- 경계 조건: inactive slot에 대한 신규 state write는 계속 `slot_inactive`로 거부되고 기존 state는 변경되지 않는다. Size limit 초과 write도 `state_too_large`로 거부되며 보존 중인 entry를 손상시키지 않는다. 명시적 전체 DB reset은 기존 범위의 데이터를 계속 제거할 수 있다.
+- 검사 방법: InMemory와 PostgreSQL fixtures에서 close 경로별 보존, inactive read, 재점유, version 연속성, write gate와 size limit parity를 검증한다. 기존 slot transition 회귀 테스트, persistence migration/round-trip 테스트, production daemon wiring, 전체 repository test와 정적 검사를 실행한다.

.proofline/criteria/ac-0027.md

@@ -0,0 +1,19 @@
+---
+id: "ac-0027"
+status: active
+---
+
+# Strategy-instance별 state identity와 version 격리
+
+## Criterion
+
+`trex-core`는 각 slot의 strategy state를 `data[strategy_instance_id] = {version, data, updated_at}` 형태의 하나의 slot-scoped map으로 저장해야 한다. `strategy_instance_id`는 entry의 저장·조회·CAS key이며 entry에 별도의 `strategy_id` metadata를 저장해서는 안 된다. `strategy_state.set`은 `{slot_id, strategy_instance_id, expected_version, data}`를 받아 required non-empty string instance ID, active slot, opaque data size limit와 해당 entry의 version만 검증해야 한다. Entry가 없을 때 `expected_version=0`인 성공 write는 version 1 entry를 만들고, 이후 성공 write는 그 entry의 version만 1 증가시켜야 한다. 같은 slot의 서로 다른 instance entry와 version은 서로 격리되어야 하며, 서로 다른 entry에 대한 동시 성공 write는 어느 entry도 유실하지 않고 모두 보존해야 한다. 기존 state에 대한 `strategy_id → strategy_instance_id` mapping·backfill·귀속 정책과 core-side instance registry를 도입해서는 안 된다.
+
+## Verification
+
+- 저장 형태: 한 slot에 instance A와 B를 저장하면 persistence round-trip 결과가 A·B key 아래 각각 `{version, data, updated_at}`를 보존하고 entry 내부에 `strategy_id`, `occupancy_seq` 또는 다른 identity metadata를 포함하지 않는다. Inner `data`는 입력한 opaque string과 byte 단위로 동일해야 한다.
+- Version 조건: 새 A에 `expected_version=0` write는 A version 1을 만들고 후속 성공 write는 A만 증가시킨다. B의 version과 data는 변하지 않는다. 존재하는 A에 `expected_version=0` 또는 stale version을 보내면 `version_conflict`로 거부하고 A·B 어느 entry도 변경하지 않는다.
+- 동시성 조건: 같은 slot의 A와 B에 동시에 유효한 write를 수행하면 둘 다 성공하고 두 entry의 새 data와 version이 모두 남아야 한다. 같은 entry에 경쟁하는 write는 version CAS에 따라 최대 한 건만 해당 expected version에서 성공하며 lost update가 없어야 한다.
+- Identity 조건: 같은 전략 종류의 서로 다른 `strategy_instance_id`는 독립 entry를 사용하고 다른 ID의 state를 상속하지 않는다. 재시작 뒤 같은 ID를 사용하는 owner는 기존 entry를 이어 사용한다. 누락·비문자열·빈 ID write는 non-retryable `bad_request`로 거부되어 map을 만들거나 변경하지 않는다.
+- 비변경 조건: active-slot gate와 data size limit를 우회하지 않으며 `slot_inactive`·`state_too_large`·`bad_request:*` 거부가 다른 entry를 변경하지 않는다. `correlation_id` 재사용만으로 write가 deduplicate되어서는 안 된다.
+- 검사 방법: InMemory/PostgreSQL 공통 contract suite, 실제 PostgreSQL row-lock 또는 동등한 원자적 update fixture, migration 및 restart round-trip에서 create/update/conflict, same-type instance 격리, A·B 동시 write, same-entry 경쟁, malformed ID와 다른 entry 무변경을 검증한다.

.proofline/criteria/ac-0028.md

@@ -0,0 +1,19 @@
+---
+id: "ac-0028"
+status: active
+---
+
+# 전략·operator slots RPC의 strategy state 가시성
+
+## Criterion
+
+`trex-core`의 `slots.req`는 전략 요청과 operator 조회의 strategy-state 가시성을 구분해야 한다. `spy=false`인 전략용 요청은 required non-empty string `strategy_instance_id`를 받아 각 반환 slot에서 `data[request.strategy_instance_id]`와 정확히 일치하는 entry 하나만 `strategy_state: {version, data, updated_at}` 단일 object로 제공해야 한다. 요청 ID에 해당하는 entry가 없으면 `strategy_state` field를 생략하고 다른 instance의 ID·state 또는 전체 map을 대신 반환해서는 안 된다. 누락·비문자열·빈 ID는 RPC-level error나 새 envelope 없이 `slots=[]`, `available_slots=null`, `degraded=false`, `reason="bad_request:strategy_instance_id"`, `message="strategy_instance_id must be a non-empty string"`인 non-retryable response를 반환해야 한다. `spy=true`인 operator 요청은 `strategy_instance_id`를 요구하지 않고 기존 filter·slot 조회와 watchdog 비갱신 동작을 유지하며, 각 반환 slot의 `strategy_state`에 전체 `strategy_instance_id → {version, data, updated_at}` map을 제공해야 한다. Operator 요청에 `strategy_instance_id`가 포함되어도 map을 특정 entry로 제한해서는 안 된다.
+
+## Verification
+
+- 전략 조회: 같은 slot map에 A와 B가 있을 때 `spy=false, strategy_instance_id=A` 요청은 `strategy_state`에 A의 `{version, data, updated_at}`만 반환하고 B의 ID·data와 outer map을 serialized payload 어디에도 포함하지 않는다. B 요청은 B만 반환하며 존재하지 않는 C 요청은 slot row의 `strategy_state`를 생략한다.
+- 잘못된 전략 요청: 누락, `null`, boolean, number, collection 및 빈 문자열 ID 각각에서 exact 기존 envelope인 `slots=[]`, `available_slots=null`, `degraded=false`, `reason="bad_request:strategy_instance_id"`, `message="strategy_instance_id must be a non-empty string"`을 반환한다. Slot, state 또는 다른 instance ID가 노출되거나 watchdog이 갱신되면 FAIL이다.
+- Operator 조회: `strategy_instance_id` 없이 `spy=true`로 기존 `universe`와 `slots` CLI가 성공하고 filter 결과와 watchdog 비갱신을 유지한다. A·B state가 있는 slot row의 `strategy_state`는 A와 B를 각각 `{version, data, updated_at}` entry로 포함한 전체 map이어야 한다. 같은 operator 요청에 A ID를 추가해도 B가 제거되지 않아야 한다.
+- 기존 계약 조합: AC-0023에 따라 제외된 slot은 strategy-state 가시성 형식을 적용하기 전에 계속 제외되고 warn-store failure는 기존 fail-closed 결과를 유지한다. 포함되는 holding slot의 broker-authoritative quantity와 unavailable metadata는 AC-0022를 유지하며 state 선택 때문에 바뀌지 않는다.
+- Wire 경계: 전략 응답의 단일 `strategy_state` object 안에는 `strategy_instance_id` key나 collection을 두지 않는다. Operator map의 key만 instance ID를 나타내며 각 value에는 identity metadata를 중복 저장하지 않는다. 별도 operator/diagnostic API, core-side instance registry 또는 caller 인증을 새로 요구하지 않는다.
+- 검사 방법: slots handler contract tests에서 전략 A/B/absent/malformed 요청과 operator no-ID/ID-present 요청을 serialized response 기준으로 검증한다. Operator CLI, watchdog, reconciliation exclusion, broker quantity, InMemory/PostgreSQL read parity와 production daemon handler wiring 회귀 테스트를 함께 실행한다.