{"id":6981,"job_id":13764,"problem_id":6,"lane_id":35,"type":"explore","user_id":90,"model":"muse-spark","provider":"unknown","report_md":"# Smallest collision: the padding wall holds at L = 56..60 on three paths; feasible floor stays L = 63\n\nJob 13764, explore, smallest-collision. Improvement claim: none. No\ncandidate scoring 13 or above was found, so nothing goes to the\nresults page. No pair below 128 bytes was found.\n\n## Hypothesis\n\nThe whole-block limit is enforced by the padding bits in m15 against\nthe round-1 path conditions, not by tunnel width: at L <= 60 no\npadding-feasible completion exists on rows Q1..Q16, so the feasible\nfloor on a given path is L = 63 (126 B) unless the path is dead\nthere too. If the wall is real, a ladder over L = 56..60 should come\nback all UNSAT on every path, while the L = 63 control on a known\nlive path stays SAT under the same harness.\n\n## Experiment\n\nPadsat ladder with tools/r298/padscan.py (z3 QF_BV, steps 0..15,\npath conditions on rows Q1..Q16, equal-length padding of member a),\nXF differential dm5 = +2^10, dm10 = +2^31, 300 s cap per instance,\none core. Three paths: c0083 (178 conditions), B2 (221 conditions),\nX_connected_best (189 conditions). Five L values each (56..60),\nplus a resolution run for X at L = 63, which an earlier ladder had\nleft unknown at a 240 s cap.\n\n## Results\n\nAll 15 ladder instances UNSAT, each in 0.59-2.32 s except B2 at\nL = 60 (20.43 s). No instance came near the 300 s cap.\n\n| path | L=56 | L=57 | L=58 | L=59 | L=60 |\n|---|---|---|---|---|---|\n| c0083 | UNSAT 0.59 s | UNSAT 0.66 s | UNSAT 0.69 s | UNSAT 1.09 s | UNSAT 1.60 s |\n| B2 | UNSAT 1.78 s | UNSAT 1.91 s | UNSAT 2.09 s | UNSAT 2.32 s | UNSAT 20.43 s |\n| X_connected_best | UNSAT 1.47 s | UNSAT 1.58 s | UNSAT 1.51 s | UNSAT 1.70 s | UNSAT 1.67 s |\n\nX at L = 63 resolves the old unknown: UNSAT in 1.17 s.\n\nControl: c0083 at L = 63 is SAT in 3.92 s under the identical\nharness. The model was verified independently by direct integer\nsteps: 512 row conditions checked, 0 mismatches; m15 top byte\n0x80 as required for L = 63; manual single-block digest equals\nhashlib.md5 (bafaf4468684194831c58c0f6f903e03).\n\n## What it means\n\nCombined with the earlier ladders (L = 61/62/63: c0083 SAT only at\n63, B2 UNSAT at 61/62/63, X UNSAT at 61/62 and now 63), the map on\nrows 1..16 is complete for these three paths: the only feasible L\nin 56..63 is 63 on c0083. The wall at L <= 60 is confirmed on all\nthree paths, and L = 61/62 are dead on all three as well. So on\nrows 1..16 the block boundary is a padding wall: shortening below\n126 B needs a path whose conditions leave m15 free enough, not\njust a wider tunnel.\n\nThe live sub-128 hopes stay the return 4373 paths 12121 (126 B)\nand 31561 (124 B), which passed the stricter rows 1..24 plus\ntunnel test. This job does not re-test them: the connect input\nsets behind them are not available locally, and the local\npadscan covers rows 1..16 only. Next steps: a connect run with\nQcondstart 25 and the Q9 objective on the 4373 route once its\ninput sets are on hand, or gxr pilots on path 12121 (the parallel\nmeasure job in this cycle covers the gxr pilots).\n","patch":null,"cpu_hours":0,"hashes":{},"author_rung":null,"status":"recorded","final_rung":"recorded","created_at":"2026-11-05T14:43:44.050Z","repo_url":null,"commit":null,"cites":null,"tokens":{"log":"summary","input":0,"models":{},"output":0,"source":"none","entries":0,"cache_read":0,"cache_write":0,"observed_models":[]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe\n\nTo repeat, on one core:\n\n1. Restore z3 (pip install z3-solver) if a VM reset wiped it.\n2. Run the ladder from the work dir root:\n   PYTHONPATH=tools/r298/job8641 python3 tools/r298/padscan.py\n   runs/job-13764/work/padscan_l56_60.jsonl 0 1 300 \"5:10,10:31\"\n   \"56 57 58 59 60\" tools/r300/cand_t13_c0083.txt\n   tools/r296/paths-best_B2_c18.txt\n   tools/r298/X_connected_best_prefix.txt\n3. Run the X at L = 63 resolution the same way with \"63\" and only\n   the X prefix file.\n4. Control: c0083 at L = 63 the same way; it should be SAT in a\n   few seconds. Verify the model with verify_control.py (direct\n   integer steps, hashlib cross-check).\n5. Read the verdicts from the JSON lines: result, solve_s, and\n   conds_Q1_Q16 per (path, L).","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":"high","also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":0},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":null,"research_route_id":null,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":null,"run_id":null,"triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"paper_exposition":null,"research_evidence":null,"transcript_mode":"summary","known_work":null,"work_disposition":null,"applicability_assessment":null,"negative_result":null,"first_indexed_at":null,"index_held_at":null,"index_ok":null,"index_reason":null,"handle":"sundayweaver","job_brief":"What limits collision length to whole blocks in known attacks, and is there a route below 128 bytes in total?","review_deferred":false,"in_triage":false,"triage":[],"lean_statement_binding":null,"lean_execution_binding":null,"lean_scientific_identity":null,"lean_execution_identity":null,"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[],"cited_by":[],"route_dependents":[],"research_url":null,"transcript_url":"/projects/md5/return/6981/transcript","files":[],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"report_sha256":"52be5454ae99e38d08e125f90016f433d3c617293ec01ffa34df19cb44cc45b1","next_step_sha256":null,"research_authority":{"witness_status":null,"research_status":"recorded","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}