docs: formalize issue 60 proofline specification

.proofline/criteria/ac-0015.md

@@ -0,0 +1,16 @@
+---
+id: "ac-0015"
+status: active
+---
+
+# 명시적 sell 미수락·미체결 상태 수렴
+
+## Criterion
+
+KIS submission 또는 authoritative order lookup이 sell 주문의 미수락·미체결을 명시적으로 확인하면 core는 실패 evidence를 기록하고 해당 dispatch를 정리하며 새 broker attempt를 생성하지 않고 slot을 broker-authoritative 보유수량의 `holding`으로 수렴시켜야 한다. 이 경로는 로컬 추정수량으로 보유량을 변경하거나 strategy에 broker retry 판단을 요구해서는 안 된다.
+
+## Verification
+
+- 성공 조건: `pending_sell`에서 명시적 rejection 또는 lookup-confirmed absence가 발생하면 기존 보유수량을 유지한 `holding`으로 전이하고 dispatch metadata가 정리되며 broker submit 호출은 한 번뿐이다.
+- 실패·경계 조건: 체결 가능성이 남은 unknown outcome을 rejection으로 취급하거나, 수량을 0으로 만들거나, 자동 새 주문을 제출하거나, broker-authoritative 수량과 다른 값으로 수렴하면 FAIL이다.
+- 검사 방법: `tests/application/test_execution_policy.py`, `tests/application/test_order_timeout_reconciliation.py`와 관련 repository transition tests에서 상태·수량·dispatch·broker call count를 단언하고 전체 회귀를 실행한다.

.proofline/criteria/ac-0016.md

@@ -0,0 +1,16 @@
+---
+id: "ac-0016"
+status: active
+---
+
+# 결과 불명확 submission의 중복 제출 방지와 reconciliation
+
+## Criterion
+
+주문 submission timeout, 연결 단절, 응답 누락 또는 응답 해석 실패로 broker acceptance 여부가 불명확하면 core는 original dispatch identity와 결과 불명확 sentinel을 durable하게 보존하고 새 broker order를 제출하지 않아야 한다. daemon 재시작과 반복 tick에서도 original order date·client identity를 사용한 broker lookup과 reconciliation을 먼저 수행하고 authoritative terminal evidence가 생기기 전에는 slot을 재사용 가능한 상태로 전환하지 않아야 한다.
+
+## Verification
+
+- 성공 조건: submit 결과 불명확 후 동일 slot의 반복 tick과 restart 모사에서 broker submit call count가 증가하지 않고 lookup/reconciliation이 실행되며 durable dispatch metadata가 유지된다.
+- 실패·경계 조건: timeout 자체로 terminal reject·holding·inactive를 추론하거나, sentinel을 지우거나, 새 broker attempt를 만들거나, 현재 날짜·wall-clock 값으로 original order identity를 대체하면 FAIL이다.
+- 검사 방법: `tests/application/test_order_timeout_reconciliation.py`의 timeout, restart, order visibility와 lookup fixture에서 call ordering·dispatch persistence·상태를 검증한다.

.proofline/criteria/ac-0017.md

@@ -0,0 +1,16 @@
+---
+id: "ac-0017"
+status: active
+---
+
+# strategy·TVR과 broker failure ownership 분리
+
+## Criterion
+
+KIS failure, raw broker error, broker attempt identity, retryability, retry schedule과 retry budget은 `trex-core` 내부 execution/reconciliation 경계를 벗어나 strategy 또는 TVR wire에 노출되어서는 안 된다. core도 broker failure를 retryable/non-retryable로 분류하여 자동 새 주문 attempt를 생성해서는 안 되며 strategy/TVR은 core가 수렴한 slot snapshot만 소비해야 한다. 이후 strategy가 독립적으로 생성한 별도 intent는 core의 자동 retry와 구분한다.
+
+## Verification
+
+- 성공 조건: sell response와 strategy-facing schema에 retryability·KIS error·attempt field가 없고 explicit reject 및 unknown outcome에서 자동 resubmit이 발생하지 않는다.
+- 실패·경계 조건: raw KIS payload나 retryable boolean이 strategy/TVR wire에 나타나거나, core가 retry schedule·budget을 산출하거나, 동일 intent에서 새 broker attempt를 자동 생성하면 FAIL이다.
+- 검사 방법: `tests/application/test_sell_retryable_flag.py`, messaging handler tests, execution rejection·unknown tests와 schema/document contract 검색을 실행한다.

.proofline/criteria/ac-0018.md

@@ -0,0 +1,16 @@
+---
+id: "ac-0018"
+status: active
+---
+
+# 주문 venue 기본값·명시값 보존과 AUTO 제거
+
+## Criterion
+
+intent venue가 누락되거나 null이면 core는 original order venue를 `SOR`로 정규화해야 하고 explicit `KRX`, `NXT`, `SOR`는 submit·ack·slot·restart·cancel 전 과정에서 변경 없이 보존해야 한다. `AUTO`는 admission, broker request와 persistence에서 거부해야 하며 기존 persisted AUTO는 migration으로 SOR로 전환해야 한다. core는 wall-clock time이나 session 추정으로 order venue를 KRX/NXT로 재라우팅해서는 안 된다.
+
+## Verification
+
+- 성공 조건: 누락/null→SOR, explicit KRX/NXT/SOR identity 보존, SOR 부분체결 후 잔량 cancel과 restart가 original SOR를 사용하는 흐름이 통과한다.
+- 실패·경계 조건: AUTO acceptance·저장, 시간 기반 venue 변환, ack actual venue로 slot order venue 덮어쓰기 또는 restart/cancel에서 original venue 손실은 FAIL이다.
+- 검사 방법: `tests/adapters/broker/test_venue.py`, `tests/application/test_venue_intent_flow.py`, migration/drift tests와 KIS request capture를 실행하여 wire·slot·SQL constraint를 단언한다.

.proofline/criteria/ac-0019.md

@@ -0,0 +1,16 @@
+---
+id: "ac-0019"
+status: active
+---
+
+# 원주문 venue와 실제 체결 venue의 durable 분리
+
+## Criterion
+
+core는 original `order_venue`와 broker-authoritative actual `execution_venue`를 서로 다른 의미로 보존해야 한다. `order_venue`는 KRX/NXT/SOR이며 submit, ack, slot, restart와 cancel에 사용한다. actual venue는 KRX/NXT 또는 미확정 NULL이며 KIS의 검증된 `ORD_EXG_GB`와 명시 exchange-id allowlist에서만 결정하여 fill, ledger와 outbox에 기록한다. `SOR`, 누락, 미지원 코드 또는 wall-clock time으로 actual venue를 추론해서는 안 된다. historical outbox SOR는 `order_venue=SOR`, actual NULL로 변환하고 migration replay는 신규 정상 조합을 오염시키지 않아야 한다.
+
+## Verification
+
+- 성공 조건: SOR order의 actual KRX/NXT fill이 `(order_venue=SOR, venue=KRX|NXT)`로 기록되고 cancel/restart는 SOR를 유지한다. historical SOR는 `(SOR,NULL)`이며 정상 `(order=KRX, actual=NXT)`는 migration 반복 후 보존된다.
+- 실패·경계 조건: actual SOR 저장, unknown code를 KRX/NXT로 추론, actual venue로 slot order venue 덮어쓰기, NULL actual SOR fill의 거짓 ledger 기록, AUTO·NULL order 저장 또는 migration replay 오염은 FAIL이다.
+- 검사 방법: KIS parser tests, execution ledger tests, `tests/adapters/persistence/test_postgresql_ledger_outbox.py`, `tests/adapters/persistence/test_migration_and_drift.py`를 실행한다. 실제 PostgreSQL에서 historical conversion, replay, round-trip과 check violation을 검증하고 전체 회귀·Ruff 및 독립 read-only QC를 수행한다.