sots-re/verify/results/compare/mf-after.md

2.3 KiB

tracecmp report: mf-after-compare.jsonl

  • build: mf-45bdf7d-dirty-20260908T0721Z started: 2026-09-08T07:31:45Z inline_max: 256
  • calls: 45 compared: 45 diverged: 0 invalid records: 0 warnings: 0
  • coverage: 45 guarded call(s), 42 undeclared write(s) in 15 call(s); 0 hook(s) unstated, 0 contradicted
hook calls modes compared diverged errors
Game::StrategyServer::MoveFleet 45 compare:45 45 0 0

coverage

hook verdict compared regions guards undeclared writes unmodelled
Game::StrategyServer::MoveFleet partial pos, prev_pos, rng, ship[0].range, ship[1].range, ship[2].range, +7 fleet 42 in 15 call(s) 6

Game::StrategyServer::MoveFleet — not checked by this run

  • (high) on arrival: dispatches SEFleetArrived and runs one of three arrival handlers by destination kind (enter system / join fleet / stop at point) — declared input boundary -- an arriving call is expected to differ in all of it, and none of it is declared, so the compare says nothing about arrivals [guard:fleet sees the fleet's own words; the event and the system do not]
  • (high) on departure: cancels every still-acting ship (with a log line each) and calls ServerSystem::FleetDeparts, which rewrites the system's ownership bits — writes through pointers to ships and to the system
  • (medium) the tanker top-up refuels other ships in the fleet — the per-ship range regions would show it, but ours does not model it, so a fleet with a tanker diverges for a known reason
  • (medium) a node-line waypoint's step comes from the stutter profile — NodeLineStep / BuildStutterSegments are written and unit-tested but not wired in; the hook steps every waypoint type as speed x dt, so a node-line leg is knowingly mis-stepped and only its type is recorded [declared gap: docs/B4.md]
  • (medium) a missed probabilistic jump scatters the fleet in a random direction — the direction is a second draw whose mapping is not modelled; ours leaves the position alone and reports the scatter distance, so the generator region diverges by one word on a miss
  • (medium) the route revalidation and the waypoint list itself — declared input boundary; the waypoint vector is not a region
  • guard hits in compare mode: fleet+0xa0:4, fleet+0xdc:1, fleet+0x10c:1, fleet+0xcc:1, fleet+0xdb:2, fleet+0xe0:26