KB-61C5
110000x · 07 — Short CUT Proof (Điều 37 via alias)
7 min read Revision 1
iu-core110000xcutshort-formproofdieu-37boundedcomposer-gate
110000x · 07 — Short CUT Proof (Điều 37 via alias)
Status: AUTHORED — ready for operator apply post-mig-042R. Bounded BEGIN/ROLLBACK proof recommended for first real-source cut.
Goal
Prove that:
CUT staging_id <sid>, output IU corpus, verify reconstruct + Axis A/B/C
…executed via the short alias fn_iu_op_cut:
- Refuses if staging is not yet approved.
- After APPROVE, accepts the same staging_id with
apply=true. - Auto-resolves
source_hashfrom the stagedcut_manifestpayload. - Auto-opens composer gate in-TX (if
p_open_composer=true), reverses on rollback. - Returns
applied=truewithpieces_created_countmatching manifest length. - Audits 1 row to
dot_iu_command_runwithrun_status='applied'. - Marks staging row
consumedwithconsumed_by_run_idset. - Inserts N rows into
public.information_unit(one per manifest piece) — and into the same TX only. - Touches zero
iu_vector_sync_pointrows.
Proof script (BEGIN/ROLLBACK)
\set ON_ERROR_STOP on
BEGIN;
-- Phase 0: capture pre state
SELECT
(SELECT count(*) FROM information_unit) AS iu_pre,
(SELECT count(*) FROM information_unit WHERE doc_code='DIEU-37') AS d37_pre,
(SELECT count(*) FROM iu_vector_sync_point) AS vsp_pre,
(SELECT count(*) FROM dot_iu_command_run) AS run_pre,
(SELECT value FROM dot_config WHERE key='iu_core.composer_enabled') AS composer_pre \gset
-- Phase 1: MARK (same as report 06)
\set source_text `cat /tmp/dieu37-source.txt`
\set pieces `cat /tmp/dieu37-pieces.json`
SELECT public.fn_iu_op_mark_file(
p_source_text:=:'source_text',
p_source_ref :='knowledge/dev/laws/dieu37-governance-organization-law.md',
p_pieces :=:'pieces'::jsonb,
p_actor :='operator-110000x-d37-cut',
p_source_kind:='user'
) -> 'staging_record_id' \gset sid_
-- Phase 2: refusal-when-unapproved (G3)
SELECT public.fn_iu_op_cut(:'sid_?column?'::uuid, true, 'operator-110000x-d37-cut', true) -> 'refusal_code' AS expect_not_approved;
-- Expect: 'not_approved'
-- Phase 3: APPROVE via verify-mark
SELECT public.fn_iu_op_verify_mark(
:'sid_?column?'::uuid, true,
'knowledge/dev/laws/dieu44-trien-khai/v0.6-iu-core-110000x-operator-alias-surface-d30-d31-protection/07-short-cut-proof.md',
'operator-110000x-d37-cut',
'operator-110000x-d37-cut'
) -> 'verdict' AS verify_verdict;
-- Expect: 'approved'
-- Phase 4: short CUT (apply=true, open composer in-TX)
WITH c AS (
SELECT public.fn_iu_op_cut(:'sid_?column?'::uuid, true, 'operator-110000x-d37-cut', true) AS r
)
SELECT
r->>'applied' AS applied,
r->>'pieces_created_count' AS pieces,
r->>'run_id' AS rid,
r->>'source_hash_resolved' AS src_hash,
r->>'composer_opened_by_alias' AS composer_opened
FROM c \gset
-- Assertions
SELECT
(:'applied'::boolean = true) AS check_applied,
((:'pieces')::int >= 12) AS check_pieces_match_manifest,
((SELECT lifecycle_status FROM iu_core.iu_staging_record
WHERE staging_record_id = :'sid_?column?'::uuid) = 'consumed') AS check_lifecycle_consumed,
((SELECT consumed_by_run_id FROM iu_core.iu_staging_record
WHERE staging_record_id = :'sid_?column?'::uuid) IS NOT NULL) AS check_consumed_by_run_id,
((SELECT run_status FROM dot_iu_command_run
WHERE run_id = :'rid'::uuid) = 'applied') AS check_audit_applied,
((SELECT count(*) FROM information_unit WHERE doc_code='DIEU-37') >= 12) AS check_iu_pieces_created,
((SELECT count(*) FROM iu_vector_sync_point) = (:'vsp_pre')::int) AS check_vsp_untouched;
-- Phase 5: VERIFY-CUT via alias
SELECT public.fn_iu_op_verify_cut(:'rid'::uuid, 'operator-110000x-d37-cut') AS verify_cut_result;
-- Expect verdict=verified, axes A/B/C ok, no_vector_ok=true, problems=[]
-- Phase 6: Inspect Axis A reconstruction (source order)
SELECT source_position, sort_order, section_type, canonical_address, depth, gap_before
FROM fn_iu_reconstruct_source('DIEU-37')
ORDER BY source_position;
-- Expect: dense monotonic sort_order from 1; gap_before=false on all rows
-- Phase 7: Inspect Axis C subtree (parent-child)
SELECT iu_id, canonical_address, depth, relative_depth
FROM fn_iu_subtree((
SELECT id FROM information_unit
WHERE doc_code='DIEU-37' AND parent_or_container_ref IS NULL
LIMIT 1
))
ORDER BY relative_depth, canonical_address;
-- Expect: root at depth 0, all children at depth 1+
ROLLBACK;
-- Phase 8: post-rollback state matches pre
SELECT
((SELECT count(*) FROM information_unit) = (:'iu_pre')::int) AS iu_restored,
((SELECT count(*) FROM information_unit WHERE doc_code='DIEU-37') = 0) AS d37_restored_zero,
((SELECT count(*) FROM iu_vector_sync_point) = (:'vsp_pre')::int) AS vsp_restored,
((SELECT count(*) FROM iu_core.iu_staging_record) = 3) AS stg_restored,
((SELECT value FROM dot_config WHERE key='iu_core.composer_enabled')='false') AS composer_restored;
Expected output
| Check | Expected |
|---|---|
| expect_not_approved | not_approved |
| verify_verdict | approved |
| check_applied | t |
| check_pieces_match_manifest | t |
| check_lifecycle_consumed | t |
| check_consumed_by_run_id | t |
| check_audit_applied | t |
| check_iu_pieces_created | t |
| check_vsp_untouched | t |
| verify_cut_result.verdict | verified |
| Axis A | dense_monotonic from 1, no gaps |
| Axis C | tree with root + N children |
| iu_restored | t |
| d37_restored_zero | t |
| vsp_restored | t |
| stg_restored | t |
| composer_restored | t |
Why BEGIN/ROLLBACK for first real cut
Per mission rule: "Prefer BEGIN/ROLLBACK if cutting full Điều 37 may be too broad for first operator proof. … Do not ask user; choose bounded safe proof if needed."
Bounded proof:
- Exercises the full pipeline end-to-end.
- Creates audit rows in
dot_iu_command_run(durably retained — they record the refusal and apply paths even on rollback? Actually no, they roll back too. Audit-tracking durability is by re-running outside BEGIN/ROLLBACK). - Leaves zero permanent state on success.
Operator may later promote to a durable cut by removing the BEGIN; / ROLLBACK; wrap, after verifying that the bounded proof passes.
Verdict template (post-apply, operator-run)
IU_CORE_110000X_SHORT_CUT_PROOF_DIEU37_PASS (bounded)
- short-form CUT alias refused unapproved (G3): PASS
- after APPROVE, alias applied via fn_iu_cut_from_manifest: PASS
- source_hash auto-resolved from staged manifest: PASS
- composer gate opened in-TX and restored on rollback: PASS
- pieces_created_count = manifest length: PASS
- audit row 'applied': PASS
- staging lifecycle 'consumed' + consumed_by_run_id set: PASS
- VERIFY-CUT verdict 'verified', axes A/B/C ok, no_vector_ok true: PASS
- iu_vector_sync_point unchanged: PASS
- post-ROLLBACK state = pre exactly: PASS