P04-01: 同時発生の更新規約
This commit is contained in:
Agent Control Runner
@@ -1,4 +1,67 @@
|
||||
# REPAIR43 — native evidence and formal acceptance pending
|
||||
# REPAIR45 — whole unit remains incomplete
|
||||
|
||||
## REPAIR45 — implementation ready for submission
|
||||
|
||||
The supplied byte-verified M engine-free context resolved the REPAIR44 UID dependency.
|
||||
UID controls: all 14 PASS, exit 0. Both supplied helper SHA-256 pins match exactly.
|
||||
AST and explicit fresh BUILD-cfile py_compile passed for all eight touched Python
|
||||
files, with python3 -B and PYTHONDONTWRITEBYTECODE=1. No source was changed in
|
||||
REPAIR45; retained passing controls were not rerun. The no-pyc static check
|
||||
passed again (exit 0); generated compile files exist only under allocated BUILD.
|
||||
The prior UID failure remains recorded as failed, not replaced with a PASS.
|
||||
|
||||
Sequential check-only S1, S2a, S2b, S3, S4 and S5 each returned exit 2:
|
||||
`ValueError: checkout is not clean`
|
||||
The initial missing-tested-tree argument refusals are also retained. The later
|
||||
attempt used the actual HEAD tree solely as a guard input, not a claim of final
|
||||
Q, clean source or C. No engine started. Root executes clean exact-Q check-only
|
||||
after automatic submission. Full argv/stdout/stderr and compile paths are in
|
||||
REPAIR41_STATIC_CHECKS.json. No Git writes, Runner or native run were performed.
|
||||
|
||||
Implementation is ready; the whole original unit remains incomplete and P04
|
||||
credit remains 0. Deferred Root conditions, in order: freeze final Q; affected
|
||||
pure controls; clean exact-Q check-only; capacity check; one heavy lease with
|
||||
fresh native S1–S4 and all ten S5 cases; independent Reader and adapters on actual
|
||||
raw (including fresh Reader order positives); fresh collect; full 184 suite once;
|
||||
index; --verify-only; registered validation before review; independent whole-unit
|
||||
Opus review; normal prepare / exact C / integration / final / Root DB join /
|
||||
ledger / main push. Native Reader and acceptance remain pending.
|
||||
patience_release stays pending unless fresh S3 raw shows it. Product freeze,
|
||||
M, allowed paths, REQUIRED membership/thresholds, all seven domains, G1/G2,
|
||||
R40–R44 and the existing one-trailing-LF spec protocol remain unchanged.
|
||||
|
||||
# REPAIR44 — original whole unit incomplete
|
||||
|
||||
Worker status is **blocked**, not ready for Root native execution. UID pure
|
||||
control could not read the supplied Q checkout's tools/run_all_tests.py
|
||||
(PermissionError). See ../REPAIR41_STATUS.md and ../REPAIR41_STATIC_CHECKS.json.
|
||||
AST/build compilation for every touched Python file and check-only S1–S5
|
||||
remain unexecuted; resume worker verification before freezing a final Q.
|
||||
|
||||
Native Reader and acceptance remain pending. The current ten-case roster is
|
||||
`S5A_PURE`, `S5B_DEPENDENCY`, `S5C_DESTRUCTION_COMMAND`, `S5D_DESTRUCTION_RAID`,
|
||||
`S5D_IN_FLIGHT`, `S5D_PAID_BEFORE_INCIDENT`, `S5E_MIDNIGHT`, `S5F_EXIT`,
|
||||
`S5G_SHIFT_1080`, `S5H_PAUSED_MIDNIGHT`.
|
||||
|
||||
The new case supplies a typed raw derivation for N completion/payment, public
|
||||
event destruction after payment, and N+1 failure/release of the secondary.
|
||||
It does not supply executed native evidence. The D05 destruction gate requires
|
||||
it in addition to every existing command/guard/idle/in-flight gate.
|
||||
patience_release stays pending unless fresh S3 raw proves it.
|
||||
|
||||
r35, r36, R40 native and R43 native remain FAILED. Q37 is a local PASS for its
|
||||
own version only. R43 Writer 2749/0, seven Writer-only derivers plus G1/G2, twelve
|
||||
pure controls and six check-only steps retain their limited historical scope;
|
||||
none is independent Reader proof. Original credit 30/88, formal credit 16/88,
|
||||
P04 credit 0; no new task/unit/worker or completion claim.
|
||||
|
||||
REPAIR41_STATIC_CHECKS.json records only worker checks actually executed.
|
||||
Root must freeze final Q, then follow S5_ROOT_RUN.md, including fresh S1–S5,
|
||||
Reader/adapters, collect, full 184 suite once, index, verify-only, registered
|
||||
validation, independent review and normal integration. Historical text below
|
||||
does not replace this order or the current ten-case roster.
|
||||
|
||||
# Historical REPAIR43 — native evidence and formal acceptance pending
|
||||
|
||||
The R42/R43 implementation batch now includes the public-restored G1/G2
|
||||
journal shadows, independent typed adapter oracle, exact-N idle OBJECTIVE
|
||||
|
||||
@@ -1,4 +1,75 @@
|
||||
# REPAIR43 submission — Root verification required
|
||||
# REPAIR45 handoff
|
||||
|
||||
## REPAIR45 — implementation ready for submission
|
||||
|
||||
The supplied byte-verified M engine-free context resolved the REPAIR44 UID dependency.
|
||||
UID controls: all 14 PASS, exit 0. Both supplied helper SHA-256 pins match exactly.
|
||||
AST and explicit fresh BUILD-cfile py_compile passed for all eight touched Python
|
||||
files, with python3 -B and PYTHONDONTWRITEBYTECODE=1. No source was changed in
|
||||
REPAIR45; retained passing controls were not rerun. The no-pyc static check
|
||||
passed again (exit 0); generated compile files exist only under allocated BUILD.
|
||||
The prior UID failure remains recorded as failed, not replaced with a PASS.
|
||||
|
||||
Sequential check-only S1, S2a, S2b, S3, S4 and S5 each returned exit 2:
|
||||
`ValueError: checkout is not clean`
|
||||
The initial missing-tested-tree argument refusals are also retained. The later
|
||||
attempt used the actual HEAD tree solely as a guard input, not a claim of final
|
||||
Q, clean source or C. No engine started. Root executes clean exact-Q check-only
|
||||
after automatic submission. Full argv/stdout/stderr and compile paths are in
|
||||
REPAIR41_STATIC_CHECKS.json. No Git writes, Runner or native run were performed.
|
||||
|
||||
Implementation is ready; the whole original unit remains incomplete and P04
|
||||
credit remains 0. Deferred Root conditions, in order: freeze final Q; affected
|
||||
pure controls; clean exact-Q check-only; capacity check; one heavy lease with
|
||||
fresh native S1–S4 and all ten S5 cases; independent Reader and adapters on actual
|
||||
raw (including fresh Reader order positives); fresh collect; full 184 suite once;
|
||||
index; --verify-only; registered validation before review; independent whole-unit
|
||||
Opus review; normal prepare / exact C / integration / final / Root DB join /
|
||||
ledger / main push. Native Reader and acceptance remain pending.
|
||||
patience_release stays pending unless fresh S3 raw shows it. Product freeze,
|
||||
M, allowed paths, REQUIRED membership/thresholds, all seven domains, G1/G2,
|
||||
R40–R44 and the existing one-trailing-LF spec protocol remain unchanged.
|
||||
|
||||
# REPAIR44 — ten cases, final Q must be frozen by Root
|
||||
|
||||
**Worker blocked on an unreadable UID-check dependency; do not start native
|
||||
execution from this partial repair.** See ../REPAIR41_STATUS.md. Remaining
|
||||
worker AST/compile and check-only checks must finish before this Root order.
|
||||
|
||||
The complete roster is `S5A_PURE`, `S5B_DEPENDENCY`, `S5C_DESTRUCTION_COMMAND`,
|
||||
`S5D_DESTRUCTION_RAID`, `S5D_IN_FLIGHT`, `S5D_PAID_BEFORE_INCIDENT`,
|
||||
`S5E_MIDNIGHT`, `S5F_EXIT`, `S5G_SHIFT_1080`, `S5H_PAUSED_MIDNIGHT`.
|
||||
CASES is sorted from CASE_TABLE; LABELS and all 23 slots derive from it.
|
||||
Receipt membership is order-independent and rejects missing/duplicate/extra
|
||||
cases or slots. Reader independently enumerates CASE_TABLE.
|
||||
|
||||
The new case completes and pays the primary at N, destroys through the public
|
||||
automatic event in INCIDENTS_AND_EVENTS at N, and fails/releases the unfinished
|
||||
secondary at N+1. See ../REPAIR44_SOURCE_FACTS.json and the REPAIR44 section in
|
||||
../REPAIR41_STATUS.md. No Defense asset registration or guard bypass is used.
|
||||
Run repair44_controls.py in addition to every existing pure control. Synthetic
|
||||
typed controls are not native evidence. R43 Writer 2749/0 and Writer-only typed
|
||||
analysis did not run the Reader; R43 native remains FAILED.
|
||||
|
||||
Authoritative Root order, after freezing the final Q:
|
||||
|
||||
1. Affected pure controls, including repair44_controls.py.
|
||||
2. Check-only S1–S5 plan (after controls finish writing temporary fixtures).
|
||||
3. Capacity check.
|
||||
4. One heavy lease: fresh native S1–S5, all ten S5 cases.
|
||||
5. Independent Reader and adapters on actual raw.
|
||||
6. Fresh collect, recomputing the new D05 sub-gate from raw.
|
||||
7. Full 184 exact-Q regression once.
|
||||
8. Index.
|
||||
9. --verify-only.
|
||||
10. Registered validation.
|
||||
11. Independent whole-unit Opus review.
|
||||
12. Normal prepare / exact C / integration / final / Root DB join / ledger / main push.
|
||||
|
||||
No worker engine/native/full regression or Git write is authorized. Whole-unit
|
||||
acceptance and patience_release remain pending. Local checks earn no credit.
|
||||
|
||||
# Historical REPAIR43 submission — superseded current roster
|
||||
|
||||
The R41 closed journal-field restriction and R42 raw-only spec stop are
|
||||
superseded. The spec passes the existing one-final-LF checker condition.
|
||||
|
||||
+33
-3
@@ -6,12 +6,13 @@ const CASE_TABLE: Dictionary = {
|
||||
"S5C_DESTRUCTION_COMMAND": {"expected_reserved_ids": 1, "labels": ["boundary", "held"], "prepare": "_prepare_order", "advance": "_advance_order", "stop": "_assert_order_stop", "assert": "_assert_order"},
|
||||
"S5D_DESTRUCTION_RAID": {"expected_reserved_ids": 0, "labels": ["boundary", "held"], "prepare": "_prepare_idle_breach", "advance": "_advance_order", "stop": "_assert_idle_breach", "assert": "_assert_idle_order"},
|
||||
"S5D_IN_FLIGHT": {"expected_reserved_ids": 1, "labels": ["boundary", "held"], "prepare": "_prepare_order", "advance": "_advance_order", "stop": "_assert_in_flight", "assert": "_assert_in_flight_order"},
|
||||
"S5D_PAID_BEFORE_INCIDENT": {"expected_reserved_ids": 1, "labels": ["boundary", "held"], "prepare": "_prepare_order", "advance": "_advance_order", "stop": "_assert_paid_incident", "assert": "_assert_paid_incident_order"},
|
||||
"S5G_SHIFT_1080": {"expected_reserved_ids": 1, "labels": ["boundary", "held"], "prepare": "_prepare_order", "advance": "_advance_order", "stop": "_assert_order_stop", "assert": "_assert_order"},
|
||||
"S5H_PAUSED_MIDNIGHT": {"expected_reserved_ids": 1, "labels": ["boundary", "held", "recovered"], "prepare": "_prepare_order", "advance": "_advance_paused_midnight", "stop": "_assert_paused_midnight", "assert": "_assert_paused_midnight_order"},
|
||||
"S5E_MIDNIGHT": {"expected_reserved_ids": 1, "labels": ["boundary", "recalled"], "prepare": "_prepare_order", "advance": "_advance_order", "stop": "_assert_order_stop", "assert": "_assert_order"},
|
||||
"S5F_EXIT": {"expected_reserved_ids": 1, "labels": ["boundary", "held"], "prepare": "_prepare_order", "advance": "_advance_order", "stop": "_assert_order_stop", "assert": "_assert_order"}
|
||||
}
|
||||
const SEEDS: Dictionary = {"S5A_PURE": 420550, "S5B_DEPENDENCY": 420551, "S5C_DESTRUCTION_COMMAND": 420552, "S5D_DESTRUCTION_RAID": 420553, "S5D_IN_FLIGHT": 420553, "S5E_MIDNIGHT": 424242, "S5F_EXIT": 420555, "S5G_SHIFT_1080": 420556, "S5H_PAUSED_MIDNIGHT": 424242}
|
||||
const SEEDS: Dictionary = {"S5A_PURE": 420550, "S5B_DEPENDENCY": 420551, "S5C_DESTRUCTION_COMMAND": 420552, "S5D_DESTRUCTION_RAID": 420553, "S5D_IN_FLIGHT": 420553, "S5D_PAID_BEFORE_INCIDENT": 420558, "S5E_MIDNIGHT": 424242, "S5F_EXIT": 420555, "S5G_SHIFT_1080": 420556, "S5H_PAUSED_MIDNIGHT": 424242}
|
||||
const GUEST: StringName = &"p04.s5.guest.a"
|
||||
const REQUEST: StringName = &"p04.s5.request.a"
|
||||
const QUEUED_GUEST: StringName = &"p04.s5.guest.b"
|
||||
@@ -201,7 +202,7 @@ func _prepare_order() -> bool:
|
||||
if _duration <= 5: return false
|
||||
_clock.advance_minutes(queue_at - _clock.absolute_minute)
|
||||
_expect(facility.active_staff_ids == staff_ids, "ordinary physical attendance")
|
||||
var second: bool = _case in ["S5D_DESTRUCTION_RAID", "S5F_EXIT"]
|
||||
var second: bool = _case in ["S5D_DESTRUCTION_RAID", "S5F_EXIT", "S5D_PAID_BEFORE_INCIDENT"]
|
||||
_expect(_stock(facility.local_inventory_id, &"ingredient/basic_meal", 2 if second else 1, &"p04.s5.order.stock"), "actual reservable meals")
|
||||
_queue(GUEST, REQUEST, _boundary if _case == "S5F_EXIT" else _boundary + _duration + 1)
|
||||
_clock.advance_one_minute()
|
||||
@@ -213,6 +214,11 @@ func _prepare_order() -> bool:
|
||||
_expect(service.started_at + _duration == _boundary + (1 if _case == "S5D_IN_FLIGHT" else 0), "natural completion from snapshot duration")
|
||||
_price = service.price_snapshot
|
||||
_duration = service.duration_minutes
|
||||
if _case == "S5D_PAID_BEFORE_INCIDENT":
|
||||
_expect(definition.capacity >= 2 and facility.active_staff_ids.size() >= definition.staff_min, "definition supports concurrent services with ordinary staff")
|
||||
if definition.capacity < 2: return false
|
||||
_clock.advance_minutes(_boundary - 2 - _clock.absolute_minute)
|
||||
_queue(QUEUED_GUEST, QUEUED_REQUEST, _boundary + _duration + 1)
|
||||
if _case == "S5D_DESTRUCTION_RAID":
|
||||
_clock.advance_minutes(_boundary - 5 - _clock.absolute_minute)
|
||||
_prepare_breach()
|
||||
@@ -229,6 +235,7 @@ func _prepare_order() -> bool:
|
||||
_recovery = {&"staff_ids": staff_ids, &"resume_minute": _boundary}
|
||||
if _case == "S5D_IN_FLIGHT":
|
||||
_guard_failure("G2", &"register_defense_asset", {&"raid_id": &"p04.s5.guard.raid", &"asset_id": _facility_id, &"kind": &"OBJECTIVE", &"max_integrity": 10000}, "A busy Facility cannot become a Defense asset.", {})
|
||||
if _case in ["S5D_IN_FLIGHT", "S5D_PAID_BEFORE_INCIDENT"]:
|
||||
_cmd(&"register_event_definition", {&"definition": {&"event_id": &"p04.s5.break", &"category": &"FLAVOR", &"priority": 100, &"foreground": false, &"transaction_policy": &"ROLLBACK_ALL", &"automatic_actions": [{&"action_id": &"break", &"type": &"SET_FACILITY_STATE", &"payload": {&"facility_id": _facility_id, &"conditions": {&"durability": 0, &"suspension_reason": &"DESTROYED"}}}]}})
|
||||
if _case not in ["S5D_IN_FLIGHT", "S5H_PAUSED_MIDNIGHT"]:
|
||||
_expect(service.elapsed_minutes == _duration - 1, "duration minus one at N-1")
|
||||
@@ -370,7 +377,7 @@ func _assert_paused_midnight_order(before: Dictionary, point: Dictionary) -> voi
|
||||
|
||||
func _advance_order(label: String) -> void:
|
||||
if label == "boundary":
|
||||
if _case == "S5D_IN_FLIGHT": _cmd(&"enqueue_event", {&"event_id": &"p04.s5.break", &"actor_ids": [&"player"]}, _boundary)
|
||||
if _case in ["S5D_IN_FLIGHT", "S5D_PAID_BEFORE_INCIDENT"]: _cmd(&"enqueue_event", {&"event_id": &"p04.s5.break", &"actor_ids": [&"player"]}, _boundary)
|
||||
if _case == "S5C_DESTRUCTION_COMMAND": _cmd(&"set_facility_conditions", {&"facility_id": _facility_id, &"conditions": {&"durability": 0}}, _boundary)
|
||||
if _case == "S5F_EXIT": _cmd(&"leave_facility_queue", {&"facility_id": _facility_id, &"request_id": QUEUED_REQUEST}, _boundary)
|
||||
if label == "recalled":
|
||||
@@ -383,6 +390,29 @@ func _advance_order(label: String) -> void:
|
||||
else:
|
||||
_clock.advance_one_minute()
|
||||
|
||||
func _assert_paid_incident(point: Dictionary) -> void:
|
||||
_expect(point[&"service"][&"state"] == "COMPLETED" and point[&"service"][&"completed_at"] == _boundary, "primary paid at N")
|
||||
_expect(point[&"facility"][&"durability"] == 0 and point[&"facility"][&"state"] == "BROKEN" and point[&"facility"][&"suspension_reason"] == "DESTROYED", "public event destruction after completion")
|
||||
var secondary: Array = []
|
||||
var facilities: Dictionary = point[&"snapshot"][&"systems"][&"runtime"][&"facilities"]
|
||||
for instance: Dictionary in facilities[&"instances"]:
|
||||
for service: Dictionary in instance[&"active_services"]:
|
||||
if service[&"request_id"] == QUEUED_REQUEST: secondary.append(service)
|
||||
for service: Dictionary in facilities[&"service_history"]:
|
||||
if service[&"request_id"] == QUEUED_REQUEST: secondary.append(service)
|
||||
_expect(secondary.size() == 1, "one secondary service without duplicate generation")
|
||||
if secondary.size() != 1: return
|
||||
_expect(secondary[0][&"state"] == ("ACTIVE" if point[&"minute"] == _boundary else "FAILED"), "secondary unfinished at N and failed at N+1")
|
||||
if point[&"minute"] > _boundary:
|
||||
_expect(secondary[0][&"failure_reason"] == "BROKEN" and secondary[0][&"completed_at"] == _boundary + 1, "secondary broken failure timestamp")
|
||||
|
||||
func _assert_paid_incident_order(before: Dictionary, point: Dictionary) -> void:
|
||||
_assert_paid_incident(point)
|
||||
_expect(point[&"wallets"][String(GUEST)] == before[&"wallets"][String(GUEST)] - _price, "one primary snapshot price debit")
|
||||
_expect(point[&"wallets"][String(QUEUED_GUEST)] == before[&"wallets"][String(QUEUED_GUEST)], "secondary uncharged")
|
||||
_assert_reservation(before, point, REQUEST, "CONSUMED", _boundary)
|
||||
_assert_reservation(before, point, QUEUED_REQUEST, "ACTIVE" if point[&"minute"] == _boundary else "RELEASED", -1 if point[&"minute"] == _boundary else _boundary + 1)
|
||||
|
||||
func _assert_order_stop(point: Dictionary) -> void:
|
||||
if _case == "S5C_DESTRUCTION_COMMAND":
|
||||
_expect(point[&"service"][&"state"] == "FAILED" and point[&"service"][&"failure_reason"] == String(FacilityService.INTERRUPTION_BROKEN), "command destruction interrupts before payment")
|
||||
|
||||
@@ -0,0 +1,171 @@
|
||||
#!/usr/bin/env python3
|
||||
"""Engine-free REPAIR44 units. Synthetic typed inputs are never native evidence."""
|
||||
import copy
|
||||
import json
|
||||
from pathlib import Path
|
||||
import sys
|
||||
|
||||
sys.dont_write_bytecode = True
|
||||
import s5_order_adapter as a
|
||||
import run_s5_native as wrapper
|
||||
|
||||
|
||||
def typed(value):
|
||||
o = a.guard_oracle
|
||||
def encode(v):
|
||||
if isinstance(v, bool):
|
||||
return o.atom(1, v)
|
||||
if isinstance(v, int):
|
||||
return o.atom(2, v)
|
||||
if isinstance(v, str):
|
||||
return o.atom(4, v)
|
||||
if isinstance(v, list):
|
||||
return o.array([encode(x) for x in v])
|
||||
return o.strings_dict([(k, encode(v)) for k, v in v.items()])
|
||||
return a.series.variant(encode(value))
|
||||
|
||||
|
||||
def fixture():
|
||||
"""Small source-shaped serializer unit for the deriver, not a game replay."""
|
||||
n, price = 960, 25
|
||||
primary = dict(service_id='primary', request_id=a.REQUEST, price_snapshot=price,
|
||||
duration_minutes=45, started_at=n-45, elapsed_minutes=44,
|
||||
state='ACTIVE', completed_at=-1, failure_reason='')
|
||||
secondary = dict(service_id='secondary', request_id=a.SECOND_REQUEST, price_snapshot=price,
|
||||
duration_minutes=45, started_at=n-1, elapsed_minutes=0,
|
||||
state='ACTIVE', completed_at=-1, failure_reason='')
|
||||
sale = dict(transaction_id='sale', category='SERVICE_SALE', amount=price,
|
||||
absolute_minute=n, source_entity_id='facility', credit_account='GUEST_WALLET:'+a.GUEST)
|
||||
reservation = dict(reservation_id='reservation.b', requester_id=a.SECOND_REQUEST, state='ACTIVE', terminal_at=-1)
|
||||
def point(minute, completed=False, broken=False, failed=False):
|
||||
s, second, r = copy.deepcopy((primary, secondary, reservation))
|
||||
history = []
|
||||
active = [s, second]
|
||||
if completed:
|
||||
s.update(state='COMPLETED', completed_at=n, elapsed_minutes=45)
|
||||
history.append(s)
|
||||
active.remove(s)
|
||||
if failed:
|
||||
second.update(state='FAILED', failure_reason='BROKEN', completed_at=n+1)
|
||||
history.append(second)
|
||||
active.remove(second)
|
||||
r.update(state='RELEASED', terminal_at=n+1)
|
||||
ledger = [copy.deepcopy(sale)] if completed else []
|
||||
requests = [] if failed else [dict(request_id=a.SECOND_REQUEST)]
|
||||
return dict(minute=minute, inputs=dict(boundary=n, price=price, duration=45, facility_id='facility'),
|
||||
service=s, facility=dict(durability=0 if broken else 100, state='BROKEN' if broken else 'OPERATING',
|
||||
suspension_reason='DESTROYED' if broken else ''),
|
||||
ledger=ledger, wallets={a.GUEST: 50-price if completed else 50, a.SECOND: 50},
|
||||
receipts=[dict(id='sale', minute=n, phase='FACILITY_COMPLETION', entries=copy.deepcopy(ledger))] if completed else [],
|
||||
reservations=[r], requests={a.SECOND_REQUEST: {} if failed else dict(request_id=a.SECOND_REQUEST)},
|
||||
active_services=len(active), snapshot=dict(systems=dict(runtime=dict(
|
||||
facilities=dict(service_history=history, instances=[dict(active_services=active)], requests=requests,
|
||||
known_service_ids=['primary', 'secondary'], known_request_ids=[a.REQUEST, a.SECOND_REQUEST],
|
||||
next_service_sequence=3),
|
||||
economy=dict(entries=copy.deepcopy(ledger), idempotency=[dict(key='service.payment.primary', transaction_id='sale')] if completed else []),
|
||||
inventory=dict(idempotency_results=[dict(action='release', result=dict(reservation_id='reservation.b', ok=True))] if failed else [])))))
|
||||
phases = []
|
||||
for name, completed, broken in [('FACILITY_COMPLETION', False, False),
|
||||
('VITALS_AND_ENVIRONMENT', True, False),
|
||||
('INCIDENTS_AND_EVENTS', True, False), ('FACILITY_QUEUES', True, True)]:
|
||||
p = point(n, completed, broken)
|
||||
p['phase'] = name
|
||||
phases.append(p)
|
||||
return dict(before=point(n-1), boundary=point(n, True, True), held=point(n+1, True, True, True)), phases
|
||||
|
||||
|
||||
def paid_controls():
|
||||
original = fixture()
|
||||
def derive(data):
|
||||
points, phases = data
|
||||
return a.paid_before_incident({k: typed(v) for k, v in points.items()}, [typed(v) for v in phases])
|
||||
assert derive(original) == {'paid_before_incident': True, 'duplicate_generations': 0}
|
||||
checks = []
|
||||
def negative(name, change):
|
||||
data = copy.deepcopy(original)
|
||||
change(*data)
|
||||
try:
|
||||
derive(data)
|
||||
except (ValueError, KeyError):
|
||||
checks.append(name)
|
||||
return
|
||||
raise AssertionError('accepted mutation: ' + name)
|
||||
runtime = lambda p: p['snapshot']['systems']['runtime']
|
||||
second = lambda p: next(s for s in runtime(p)['facilities']['service_history'] if s['request_id'] == a.SECOND_REQUEST)
|
||||
negative('sale-removed', lambda p, h: p['boundary']['ledger'].clear())
|
||||
negative('sale-duplicated', lambda p, h: p['held']['ledger'].append(copy.deepcopy(p['held']['ledger'][0])))
|
||||
negative('sale-after-incidents', lambda p, h: p['boundary']['receipts'][0].update(phase='FACILITY_QUEUES'))
|
||||
negative('destruction-before-completion', lambda p, h: h[0]['facility'].update(durability=0))
|
||||
negative('primary-not-completed', lambda p, h: p['boundary']['service'].update(state='ACTIVE'))
|
||||
negative('secondary-charged', lambda p, h: p['held']['wallets'].update({a.SECOND: 25}))
|
||||
negative('secondary-not-failed', lambda p, h: second(p['held']).update(state='ACTIVE'))
|
||||
negative('secondary-failed-at-N', lambda p, h: second(p['held']).update(completed_at=960))
|
||||
negative('reservation-not-released', lambda p, h: p['held']['reservations'][0].update(state='ACTIVE'))
|
||||
negative('reservation-released-twice', lambda p, h: runtime(p['held'])['inventory']['idempotency_results'].append(copy.deepcopy(runtime(p['held'])['inventory']['idempotency_results'][0])))
|
||||
negative('idempotency-missing', lambda p, h: runtime(p['held'])['economy']['idempotency'].clear())
|
||||
negative('idempotency-duplicated', lambda p, h: runtime(p['held'])['economy']['idempotency'].append(copy.deepcopy(runtime(p['held'])['economy']['idempotency'][0])))
|
||||
negative('wrong-financial-day', lambda p, h: p['held']['ledger'][0].update(absolute_minute=2400))
|
||||
negative('AFTER-copy-tautology', lambda p, h: p.update(before=copy.deepcopy(p['held'])))
|
||||
negative('phase-order-reversed', lambda p, h: h.reverse())
|
||||
negative('duplicate-generation', lambda p, h: runtime(p['held'])['facilities']['service_history'].append(copy.deepcopy(second(p['held']))))
|
||||
negative('hidden-generation-counter', lambda p, h: runtime(p['held'])['facilities'].update(next_service_sequence=4))
|
||||
return checks
|
||||
|
||||
|
||||
def roster_controls():
|
||||
cases, slots = list(wrapper.CASE_TABLE), wrapper.SLOTS
|
||||
old = [c for c in cases if c != 'S5D_PAID_BEFORE_INCIDENT']
|
||||
assert sorted(old) != old, 'old R43 comparison must fail on actual insertion order'
|
||||
assert wrapper.exact_roster(cases, slots)
|
||||
assert wrapper.exact_roster(cases[::-1], slots[::-1])
|
||||
assert not wrapper.exact_roster(cases[:-1], slots)
|
||||
assert not wrapper.exact_roster(cases + [cases[0]], slots)
|
||||
assert not wrapper.exact_roster(cases + ['UNKNOWN'], slots)
|
||||
assert not wrapper.exact_roster(cases, slots[:-1])
|
||||
assert not wrapper.exact_roster(cases, slots + ['UNKNOWN-slot'])
|
||||
assert not wrapper.exact_roster(cases, slots + [slots[0]])
|
||||
assert set(cases) == set(a.DERIVERS) | set(a.power.CASES)
|
||||
import re
|
||||
probe = wrapper.QA.read_text()
|
||||
seeds = json.loads(re.search(r'^const SEEDS: Dictionary = (.*)$', probe, re.M)[1])
|
||||
assert set(seeds) == set(cases)
|
||||
for row in wrapper.CASE_TABLE.values():
|
||||
for key in ('prepare', 'advance', 'stop', 'assert'):
|
||||
assert 'func ' + row[key] + '(' in probe
|
||||
# Reader obtains its own branches directly from CASE_TABLE (never Writer's list).
|
||||
reader = probe.split('func _reader()', 1)[1]
|
||||
assert 'for branch: String in CASE_TABLE:' in reader
|
||||
expected_line = next(l for l in a.POWER_PATH.read_text().splitlines() if 'expected = set(CASES)' in l)
|
||||
assert set(re.findall(r'"(S5[^"]+)"', expected_line)) | set(a.power.CASES) == set(cases)
|
||||
root = Path(__file__).resolve().parents[1]
|
||||
project = next(p for p in root.parents if (p / 'tools/check_p04_order_evidence.py').is_file())
|
||||
checker = (project / 'tools/check_p04_order_evidence.py').read_text()
|
||||
assert set(re.findall(r"['\"](S5[A-Z][A-Z0-9_]*)['\"]", checker)) == set(cases)
|
||||
collector = (root / 'p04_native_series.py').read_text()
|
||||
assert "set(order['cases']) == set(adapter.DERIVERS)" in collector
|
||||
assert "set(power['cases']) == set(adapter.power.CASES)" in collector
|
||||
assert 'order = adapter.derive(*arguments)' in collector
|
||||
for name in ('S5_ROOT_RUN.md', 'PENDING.md'):
|
||||
assert set(re.findall(r'`(S5[A-Z][A-Z0-9_]*)`', (root / 's5' / name).read_text())) == set(cases)
|
||||
status = (root / 'REPAIR41_STATUS.md').read_text().split('## REPAIR44', 1)[1]
|
||||
assert set(re.findall(r'`(S5[A-Z][A-Z0-9_]*)`', status.split('## ', 1)[0])) == set(cases)
|
||||
wrapper.probe_guard(project)
|
||||
patterns = [r'\bvar\s+\w+\s*=', r'\bfor\s+\w+\s+in\b',
|
||||
r'\.(?:patience_remaining|elapsed_minutes|power_available|capacity|hold_until)\s*=(?!=)']
|
||||
for regex, bad in zip(patterns, ['var x = 1', 'for x in values:', 'f.capacity = 2']):
|
||||
assert not re.search(regex, probe) and re.search(regex, bad)
|
||||
return ['R43-old-comparison-reproduced', 'insertion-order', 'reverse-order',
|
||||
'missing-case', 'duplicate-case', 'unknown-case', 'missing-slot', 'extra-slot',
|
||||
'duplicate-slot', 'probe-seeds-wrapper-reader-adapter-collector-checker-docs-name-sync',
|
||||
'probe-guard-regex-self-check']
|
||||
|
||||
|
||||
def main():
|
||||
root = Path(__file__).resolve().parents[1]
|
||||
assert not list(root.rglob('*.pyc')), 'no generated bytecode under allowed execution paths'
|
||||
print(json.dumps(dict(synthetic_units_only=True, formal_acceptance=False,
|
||||
paid_mutations=paid_controls(), roster=roster_controls(), no_pyc=True), indent=2))
|
||||
|
||||
|
||||
if __name__ == '__main__':
|
||||
main()
|
||||
@@ -43,10 +43,17 @@ def case_table(path):
|
||||
|
||||
|
||||
CASE_TABLE = case_table(QA)
|
||||
CASES = list(CASE_TABLE)
|
||||
LABELS = {case: [label for label in row["labels"] if label != "duplicate_guard"]
|
||||
for case, row in CASE_TABLE.items()}
|
||||
CASES = sorted(CASE_TABLE)
|
||||
LABELS = {case: [label for label in CASE_TABLE[case]["labels"] if label != "duplicate_guard"]
|
||||
for case in CASES}
|
||||
SLOTS = sorted(case + "-" + label for case in CASES for label in LABELS[case])
|
||||
|
||||
def exact_roster(branches, slots):
|
||||
return (len(branches) == len(set(branches)) == len(CASES)
|
||||
and sorted(branches) == CASES
|
||||
and len(slots) == len(set(slots)) == len(SLOTS)
|
||||
and sorted(slots) == SLOTS)
|
||||
|
||||
MATERIALS = [MANIFEST, BUILD / "audit-support/p04-review-repair22-r01/ACTUAL_CURRENT_PUBLIC_POWER_FUNCTIONS.json"]
|
||||
|
||||
def r17_relocation_guard(root):
|
||||
@@ -66,6 +73,13 @@ def r17_relocation_guard(root):
|
||||
def probe_guard(root):
|
||||
probe = QA.read_text()
|
||||
import re
|
||||
seeds = re.findall(r"^const SEEDS: Dictionary = (.*)$", probe, re.M)
|
||||
if len(seeds) != 1 or sorted(json.loads(seeds[0])) != CASES or sorted(case_table(QA)) != CASES:
|
||||
raise ValueError("probe/seed canonical roster mismatch")
|
||||
for case in CASES:
|
||||
for key in ("prepare", "advance", "stop", "assert"):
|
||||
if "func " + CASE_TABLE[case][key] + "(" not in probe:
|
||||
raise ValueError("missing case dispatch function")
|
||||
if ":=" in probe or re.search(r"\bvar\s+\w+\s*=", probe) or re.search(r"\bfor\s+\w+\s+in\b", probe):
|
||||
raise ValueError("explicit typed declarations/loops required")
|
||||
if re.search(r"\.(?:patience_remaining|elapsed_minutes|power_available|capacity|hold_until)\s*=(?!=)", probe):
|
||||
@@ -522,7 +536,7 @@ def main():
|
||||
receipt = r.read(out / ("raw/" + phase + ".json"))
|
||||
r.require(receipt["checks"] > 0 and receipt["failures"] == 0,
|
||||
"S5 actual outcome receipt")
|
||||
r.require(sorted(receipt["branches"]) == CASES,
|
||||
r.require(exact_roster(receipt["branches"], receipt["slots"]),
|
||||
"exact one independent Writer/Reader case")
|
||||
r.require(sorted(receipt["slots"]) == SLOTS, "all formal point slots")
|
||||
r.require(receipt["pid"] == row["actual_pid"], "actual native PID/receipt")
|
||||
|
||||
@@ -138,6 +138,82 @@ def destruction_raid_r40(points, phases):
|
||||
return {'raid_sale_before_destruction': True, 'raid_unfinished_release': True}
|
||||
|
||||
|
||||
def paid_before_incident(points, phases):
|
||||
"""Phase-start snapshots bracket completion and the public automatic event."""
|
||||
before, boundary, end = (points[k] for k in ('before', 'boundary', 'held'))
|
||||
n = scalar(before, 'inputs', 'boundary')
|
||||
completion = phase(phases, 'FACILITY_COMPLETION', n)
|
||||
completed = phase(phases, 'VITALS_AND_ENVIRONMENT', n)
|
||||
incident = phase(phases, 'INCIDENTS_AND_EVENTS', n)
|
||||
queues = phase(phases, 'FACILITY_QUEUES', n)
|
||||
require([phases.index(p) for p in (completion, completed, incident, queues)] ==
|
||||
sorted(phases.index(p) for p in (completion, completed, incident, queues)),
|
||||
'completion/event/queue phase order')
|
||||
require(scalar(before, 'minute') == n - 1 and scalar(boundary, 'minute') == n
|
||||
and scalar(end, 'minute') == n + 1, 'exact boundary points')
|
||||
for p in (before, completion):
|
||||
require(scalar(p, 'service', 'state') == 'ACTIVE' and not sales(p)
|
||||
and scalar(p, 'service', 'started_at') + scalar(p, 'service', 'duration_minutes') == n
|
||||
and scalar(p, 'service', 'elapsed_minutes') == scalar(p, 'service', 'duration_minutes') - 1
|
||||
and scalar(p, 'facility', 'durability') > 0, 'independent pre-completion state')
|
||||
sale = payment(before, completed, n)
|
||||
for p in (completed, incident, queues, boundary, end):
|
||||
require(payment(before, p, n).raw == sale.raw, 'identical surviving sale')
|
||||
require([r.raw for r in rows(p, 'ledger') if scalar(r, 'category') == 'SERVICE_SALE'] == [sale.raw],
|
||||
'one total sale; secondary never charged')
|
||||
require(scalar(p, 'wallets', SECOND) == scalar(before, 'wallets', SECOND), 'unchanged second wallet')
|
||||
receipts = [r for r in rows(p, 'receipts') if scalar(r, 'id') == scalar(sale, 'transaction_id')]
|
||||
require(len(receipts) == 1 and scalar(receipts[0], 'phase') == 'FACILITY_COMPLETION'
|
||||
and scalar(receipts[0], 'minute') == n, 'payment emitted in completion phase')
|
||||
require(scalar(sale, 'absolute_minute') // 1440 + 1 == n // 1440 + 1,
|
||||
'financial day derived from ledger absolute_minute')
|
||||
require(scalar(completed, 'facility', 'durability') > 0
|
||||
and scalar(incident, 'facility', 'durability') > 0, 'destruction not before incidents')
|
||||
for p in (queues, boundary, end):
|
||||
require(scalar(p, 'facility', 'durability') == 0 and scalar(p, 'facility', 'state') == 'BROKEN'
|
||||
and scalar(p, 'facility', 'suspension_reason') == 'DESTROYED', 'event destruction at N')
|
||||
|
||||
def services(p):
|
||||
facilities = field(p, 'snapshot', 'systems', 'runtime', 'facilities')
|
||||
return (rows(facilities, 'service_history') +
|
||||
[s for f in rows(facilities, 'instances') for s in rows(f, 'active_services')])
|
||||
|
||||
baseline = services(before)
|
||||
ids = [scalar(s, 'service_id') for s in baseline]
|
||||
require(len(ids) == len(set(ids)) == 2, 'exactly two independent original service IDs')
|
||||
second_id = None
|
||||
for p in (before, completion, completed, incident, queues, boundary, end):
|
||||
current = services(p)
|
||||
require(sorted(scalar(s, 'service_id') for s in current) == sorted(ids), 'zero duplicate generations')
|
||||
for key in ('known_service_ids', 'known_request_ids', 'next_service_sequence'):
|
||||
require(field(p, 'snapshot', 'systems', 'runtime', 'facilities', key).raw ==
|
||||
field(before, 'snapshot', 'systems', 'runtime', 'facilities', key).raw,
|
||||
'stable service/request generation bookkeeping: ' + key)
|
||||
secondary = [s for s in current if scalar(s, 'request_id') == SECOND_REQUEST]
|
||||
require(len(secondary) == 1, 'one secondary request/service join')
|
||||
s = secondary[0]
|
||||
if second_id is None:
|
||||
second_id = scalar(s, 'service_id')
|
||||
require(scalar(s, 'service_id') == second_id, 'secondary identity unchanged')
|
||||
if p is end:
|
||||
require(scalar(s, 'state') == 'FAILED' and scalar(s, 'failure_reason') == 'BROKEN'
|
||||
and scalar(s, 'completed_at') == n + 1, 'secondary failed once at N+1')
|
||||
else:
|
||||
require(scalar(s, 'state') == 'ACTIVE' and scalar(s, 'elapsed_minutes') < scalar(s, 'duration_minutes')
|
||||
and scalar(s, 'started_at') == n - 1, 'secondary unfinished through N')
|
||||
reservation = [r for r in rows(p, 'reservations') if scalar(r, 'requester_id') == SECOND_REQUEST]
|
||||
require(len(reservation) == 1 and scalar(reservation[0], 'state') == 'ACTIVE', 'secondary reservation held through N')
|
||||
require(not [r for r in rows(p, 'snapshot', 'systems', 'runtime', 'inventory', 'idempotency_results')
|
||||
if scalar(r, 'action') == 'release'
|
||||
and scalar(r, 'result', 'reservation_id') == scalar(reservation[0], 'reservation_id')],
|
||||
'no early secondary release')
|
||||
release(before, end, SECOND_REQUEST, n + 1)
|
||||
require(not rows(end, 'snapshot', 'systems', 'runtime', 'facilities', 'requests')
|
||||
and all(scalar(r, 'state') != 'ACTIVE' for r in rows(end, 'reservations'))
|
||||
and scalar(end, 'active_services') == 0, 'no reservation or orphan request remains')
|
||||
return {'paid_before_incident': True, 'duplicate_generations': 0}
|
||||
|
||||
|
||||
def destruction_raid(points, phases):
|
||||
before = points['before']
|
||||
n = scalar(before, 'inputs', 'boundary')
|
||||
@@ -333,7 +409,8 @@ def exit_order(points, phases):
|
||||
|
||||
|
||||
DERIVERS = {'S5C_DESTRUCTION_COMMAND': destruction_command, 'S5D_DESTRUCTION_RAID': destruction_raid,
|
||||
'S5D_IN_FLIGHT': destruction_in_flight, 'S5G_SHIFT_1080': shift_completion,
|
||||
'S5D_IN_FLIGHT': destruction_in_flight, 'S5D_PAID_BEFORE_INCIDENT': paid_before_incident,
|
||||
'S5G_SHIFT_1080': shift_completion,
|
||||
'S5H_PAUSED_MIDNIGHT': paused_midnight, 'S5E_MIDNIGHT': midnight_day, 'S5F_EXIT': exit_order}
|
||||
|
||||
|
||||
|
||||
+35
@@ -148,6 +148,41 @@ def main():
|
||||
return
|
||||
raise ValueError('mutation accepted: ' + label)
|
||||
|
||||
paid = 'S5D_PAID_BEFORE_INCIDENT'
|
||||
points, phases = cases[paid]
|
||||
end, boundary = points['held'], points['boundary']
|
||||
n = a.scalar(points['before'], 'inputs', 'boundary')
|
||||
def changed_array(node, members):
|
||||
start = 12 if node.raw[:4] == struct.pack('<I', 65564) else 8
|
||||
return node.raw[:start-4] + struct.pack('<I', len(members)) + b''.join(r.raw for r in members)
|
||||
sale = a.sales(end)[0]
|
||||
ledger = a.field(end, 'ledger')
|
||||
negative('paid-sale-removed', paid, end, ledger, changed_array(ledger, [r for r in ledger.value if r is not sale]))
|
||||
negative('paid-sale-duplicated', paid, end, ledger, changed_array(ledger, ledger.value + [sale]))
|
||||
receipt = next(r for r in a.rows(end, 'receipts') if a.scalar(r, 'id') == a.scalar(sale, 'transaction_id'))
|
||||
negative('paid-sale-after-incidents', paid, end, a.field(receipt, 'phase'), mutation.scalar(4, 'FACILITY_QUEUES'))
|
||||
pre = a.phase(phases, 'FACILITY_COMPLETION', n)
|
||||
negative('paid-destruction-before-completion', paid, pre, a.field(pre, 'facility', 'durability'), mutation.scalar(2, 0))
|
||||
negative('paid-primary-not-completed', paid, end, a.field(end, 'service', 'state'), mutation.scalar(4, 'ACTIVE'))
|
||||
negative('paid-secondary-charged', paid, end, a.field(end, 'wallets', a.SECOND), mutation.scalar(2, a.scalar(end, 'wallets', a.SECOND)-1))
|
||||
secondary = next(r for r in a.rows(end, 'snapshot', 'systems', 'runtime', 'facilities', 'service_history')
|
||||
if a.scalar(r, 'request_id') == a.SECOND_REQUEST)
|
||||
negative('paid-secondary-not-failed', paid, end, a.field(secondary, 'state'), mutation.scalar(4, 'ACTIVE'))
|
||||
negative('paid-secondary-failed-at-N', paid, end, a.field(secondary, 'completed_at'), mutation.scalar(2, n))
|
||||
reservation = next(r for r in a.rows(end, 'reservations') if a.scalar(r, 'requester_id') == a.SECOND_REQUEST)
|
||||
negative('paid-reservation-held', paid, end, a.field(reservation, 'state'), mutation.scalar(4, 'ACTIVE'))
|
||||
operations = a.field(end, 'snapshot', 'systems', 'runtime', 'inventory', 'idempotency_results')
|
||||
released = next(r for r in operations.value if a.scalar(r, 'action') == 'release'
|
||||
and a.scalar(r, 'result', 'reservation_id') == a.scalar(reservation, 'reservation_id'))
|
||||
negative('paid-double-release', paid, end, operations, changed_array(operations, operations.value + [released]))
|
||||
idem = a.field(end, 'snapshot', 'systems', 'runtime', 'economy', 'idempotency')
|
||||
key = 'service.payment.' + a.scalar(end, 'service', 'service_id')
|
||||
payment = next(r for r in idem.value if a.scalar(r, 'key') == key)
|
||||
negative('paid-idempotency-missing', paid, end, idem, changed_array(idem, [r for r in idem.value if r is not payment]))
|
||||
negative('paid-idempotency-duplicate', paid, end, idem, changed_array(idem, idem.value + [payment]))
|
||||
negative('paid-wrong-day', paid, end, a.field(sale, 'absolute_minute'), mutation.scalar(2, n+1440))
|
||||
negative('paid-AFTER-copy', paid, points['before'], points['before'], end.raw)
|
||||
|
||||
midnight = 'S5E_MIDNIGHT'
|
||||
points, phases = cases[midnight]
|
||||
n = a.scalar(points['before'], 'inputs', 'boundary')
|
||||
|
||||
@@ -100,7 +100,7 @@ def derive(root, writer_sha, reader_sha):
|
||||
writer = json.loads(raw.pin(root / "writer.json", writer_sha), object_pairs_hook=unique)
|
||||
reader = json.loads(raw.pin(root / "reader.json", reader_sha), object_pairs_hook=unique)
|
||||
require(writer["pid"] != reader["pid"] and writer["profile"] != reader["profile"], "independent reader required")
|
||||
expected = set(CASES) | {"S5C_DESTRUCTION_COMMAND", "S5D_DESTRUCTION_RAID", "S5D_IN_FLIGHT", "S5E_MIDNIGHT", "S5F_EXIT", "S5G_SHIFT_1080", "S5H_PAUSED_MIDNIGHT"}
|
||||
expected = set(CASES) | {"S5C_DESTRUCTION_COMMAND", "S5D_DESTRUCTION_RAID", "S5D_IN_FLIGHT", "S5D_PAID_BEFORE_INCIDENT", "S5E_MIDNIGHT", "S5F_EXIT", "S5G_SHIFT_1080", "S5H_PAUSED_MIDNIGHT"}
|
||||
historical_roster = set(CASES) | {"S5C_DESTRUCTION_COMMAND", "S5D_DESTRUCTION_RAID", "S5E_MIDNIGHT", "S5F_EXIT"}
|
||||
require(set(writer["branches"]) == set(reader["branches"]) and
|
||||
set(writer["branches"]) in (set(CASES), historical_roster, expected), "exact pair or full case table roster")
|
||||
|
||||
Reference in New Issue
Block a user