{"ok":true,"service":"telemetry.thomas.md","segregated_store":true,"store_dir":"/srv/telemetry-hub","streams":{"certified-research":1,"lean-native":7,"turbo-lean":12},"blobs_count":22,"recent":{"certified-research":[{"query":"query IntrospectionQuery{__schema{queryType{name} types{name} directives{name}}}","event_id":"4714fb0d1a4d349534f2ae8c8e5fe502","received_at":"2026-10-21T21:22:17.558774+00:00"}],"lean-native":[{"schema":"lean-native.telemetry.v1","event_id":"2491bc31b8adf7d291e87fc31fc59390","timestamp_ns":7205284512126985,"context":{"lean_native_version":"0.5.0","module_name":"LeanNative.Benchmarks.Canonical","target":"x86_64"},"decl":{"name":"dot_product_u64","structural_hash":"41bc2950a7ac572d","lnir_raw_blob":"blake3:ef19e1a577c46461f25860ebcf165e645bd61f3bf720439b0cb602d50e052cc6","lnir_canonical_debruijn_blob":"blake3:c3bcff840207ea56f14c6e9448a360c5f12b45108cba80aa46c2d5faca9ac71f","features":{"n_instr":5,"n_blocks":2,"n_loops":1,"max_loop_depth":1,"width_histogram":{"u64":2,"u256":0,"bool":0}}},"decision":{"step_idx":0,"pass_or_rule":"builtin:loop-vectorize","theorem_or_rule":"LeanNative.Proofs.LoopOptProofs.hoistExclusivity_sound","pass_history":[],"before_ir_blob":"blake3:ef19e1a577c46461f25860ebcf165e645bd61f3bf720439b0cb602d50e052cc6","after_ir_blob":"blake3:4a5ed61816b5b593dbdd632b5525eab01bb0e8bc86063688b2256b96a9352f81","after_debruijn_blob":"blake3:9b5c7586433635fa9a64f8b12ac715864a2e819b23a4d865f65d113d7448de4b","proposer":{"kind":"builtin_verified","notes":"Analyzed and annotated 2 SIMD/data-parallel loop/borrow regions (!llvm.loop.vectorize.enable)"}},"validation":{"symbolic_tv":{"status":"passed","unroll_bound":4,"samples":64,"samples_ok":64,"ub_refines":true,"domain_equiv":true,"poison_refines":true,"sym_ret_equiv":true,"mem_writes_equiv":true},"kernel_check":{"status":"accepted","evidence_kind":"reflective","theorem_ref":"LeanNative.Proofs.LoopOptProofs.hoistExclusivity_sound","sorry_count":0}},"cost_model":{"cost_before":0,"cost_after":0},"rl_outcome":{"accepted_into_pipeline":true,"rejection_stage":null,"reward_components":{"cost_delta":0,"kernel_verified":1.0,"tv_passed":1.0}},"received_at":"2026-10-21T21:23:22.253245+00:00"},{"schema":"lean-native.telemetry.v1","event_id":"0201ca6114fb50477a107f2e590096ef","timestamp_ns":7205284288507210,"context":{"lean_native_version":"0.5.0","module_name":"LeanNative.Benchmarks.Canonical","target":"x86_64"},"decl":{"name":"collatz_steps","structural_hash":"2964232c3b082238","lnir_raw_blob":"blake3:850bf1d4386ef2e7bf3237d400ddfbcb3787f325c4b84716c2d570af9a0c5e83","lnir_canonical_debruijn_blob":"blake3:1ea8b2bfe2389d719121aaabdbbfae93ce6d618794874ce7abf30d7f31bf7dd6","features":{"n_instr":9,"n_blocks":3,"n_loops":1,"max_loop_depth":1,"width_histogram":{"u64":7,"u256":0,"bool":0}}},"decision":{"step_idx":0,"pass_or_rule":"builtin:algebraic-peephole","theorem_or_rule":"LeanNative.Proofs.PeepholeProofs.rewriteScalarPeephole_sound","pass_history":[],"before_ir_blob":"blake3:850bf1d4386ef2e7bf3237d400ddfbcb3787f325c4b84716c2d570af9a0c5e83","after_ir_blob":"blake3:b6815b9486b9dd77dcf0334b9be6290e37424915ba3df89e04fe11a78d105462","after_debruijn_blob":"blake3:2fbaadcbed2aa11e183c8cc26f0cf6fcb88d30875968eead5b04903aadc1ddbd","proposer":{"kind":"builtin_verified","notes":"Strength reduction (*2^k -> <<<k, /2^k -> >>>k, %2^k -> &&&(2^k-1)), identity folding, constant branch elimination, and EVM SSTORE->SLOAD forwarding (storageStore_load_same_sound)"}},"validation":{"symbolic_tv":{"status":"passed","unroll_bound":4,"samples":64,"samples_ok":64,"ub_refines":true,"domain_equiv":true,"poison_refines":true,"sym_ret_equiv":true,"mem_writes_equiv":true},"kernel_check":{"status":"accepted","evidence_kind":"reflective","theorem_ref":"LeanNative.Proofs.PeepholeProofs.rewriteScalarPeephole_sound","sorry_count":0}},"cost_model":{"cost_before":31,"cost_after":4},"rl_outcome":{"accepted_into_pipeline":true,"rejection_stage":null,"reward_components":{"cost_delta":27,"kernel_verified":1.0,"tv_passed":1.0}},"received_at":"2026-10-21T21:23:22.305792+00:00"},{"schema":"lean-native.telemetry.v1","event_id":"f125d31f731350e53bbd082327f4e647","timestamp_ns":7205284288507210,"context":{"lean_native_version":"0.5.0","module_name":"LeanNative.Benchmarks.Canonical","target":"x86_64"},"decl":{"name":"tuple_accum_sum","structural_hash":"f2eefdb7429b5e57","lnir_raw_blob":"blake3:25548469f186980c9956befded94f22b5687d64f7d101c0d97c891a14fdcc27b","lnir_canonical_debruijn_blob":"blake3:d5813bad9b71afa8ad6b62e495488c940632f9b7ee51b401145818fa3adf201d","features":{"n_instr":10,"n_blocks":3,"n_loops":1,"max_loop_depth":1,"width_histogram":{"u64":7,"u256":0,"bool":0}}},"decision":{"step_idx":1,"pass_or_rule":"builtin:unbox-tuple-sroa","theorem_or_rule":"LeanNative.Proofs.LoopOptProofs.unboxTupleProj_sound","pass_history":["builtin:algebraic-peephole"],"before_ir_blob":"blake3:25548469f186980c9956befded94f22b5687d64f7d101c0d97c891a14fdcc27b","after_ir_blob":"blake3:623c3fb337731d7c44ad7db1f6f25d194a79a4bc6bdb70aba61be56cd200dabd","after_debruijn_blob":"blake3:54e5a9f63a7f65f4f3437080f5f222be544361ef380d3c76fde770a106883c33","proposer":{"kind":"builtin_verified","notes":"Forwards projTuple through SSA mkTuple alias map and eliminates dead tuple allocations"}},"validation":{"symbolic_tv":{"status":"passed","unroll_bound":4,"samples":64,"samples_ok":64,"ub_refines":true,"domain_equiv":true,"poison_refines":true,"sym_ret_equiv":true,"mem_writes_equiv":true},"kernel_check":{"status":"accepted","evidence_kind":"reflective","theorem_ref":"LeanNative.Proofs.LoopOptProofs.unboxTupleProj_sound","sorry_count":0}},"cost_model":{"cost_before":3,"cost_after":3},"rl_outcome":{"accepted_into_pipeline":true,"rejection_stage":null,"reward_components":{"cost_delta":0,"kernel_verified":1.0,"tv_passed":1.0}},"received_at":"2026-10-21T21:23:22.311638+00:00"},{"schema":"lean-native.telemetry.v1","event_id":"52fefa6fa662cb682f165d6b114622a9","timestamp_ns":7205284288507210,"context":{"lean_native_version":"0.5.0","module_name":"LeanNative.Benchmarks.Canonical","target":"x86_64"},"decl":{"name":"collatz_steps","structural_hash":"8c77c18b5606bec9","lnir_raw_blob":"blake3:b6815b9486b9dd77dcf0334b9be6290e37424915ba3df89e04fe11a78d105462","lnir_canonical_debruijn_blob":"blake3:2fbaadcbed2aa11e183c8cc26f0cf6fcb88d30875968eead5b04903aadc1ddbd","features":{"n_instr":9,"n_blocks":3,"n_loops":1,"max_loop_depth":1,"width_histogram":{"u64":7,"u256":0,"bool":0}}},"decision":{"step_idx":1,"pass_or_rule":"adversarial:unsound-alu-corruptor","theorem_or_rule":"UNTRUSTED_PR_CANDIDATE","pass_history":["builtin:algebraic-peephole"],"before_ir_blob":"blake3:b6815b9486b9dd77dcf0334b9be6290e37424915ba3df89e04fe11a78d105462","after_ir_blob":"blake3:d9481a19bd68dd078fd3e00256509840904f2d86759a35e7f2712b561bb557be","after_debruijn_blob":"blake3:aa10d26a1ff0950606c0aa69e4d7c7460bd3690d414a8409e449e4bf9428da3a","proposer":{"kind":"adversarial_untrusted","notes":"Intentionally unsound ALU corruption to test Law 1 rejection gate"}},"validation":{"symbolic_tv":{"status":"failed","unroll_bound":4,"samples":64,"samples_ok":0,"ub_refines":true,"domain_equiv":true,"poison_refines":true,"sym_ret_equiv":false,"mem_writes_equiv":true},"kernel_check":{"status":"rejected","evidence_kind":"bounded_only","theorem_ref":"UNTRUSTED_PR_CANDIDATE","sorry_count":0}},"cost_model":{"cost_before":4,"cost_after":4},"rl_outcome":{"accepted_into_pipeline":false,"rejection_stage":"symbolic_tv","reward_components":{"cost_delta":0,"kernel_verified":0.0,"tv_passed":-1.0}},"received_at":"2026-10-21T21:23:22.457259+00:00"},{"schema":"lean-native.telemetry.v1","event_id":"cd9edbc266da77e8668cb5dde662f27b","timestamp_ns":7205284288507210,"context":{"lean_native_version":"0.5.0","module_name":"LeanNative.Benchmarks.Canonical","target":"x86_64"},"decl":{"name":"tuple_accum_sum","structural_hash":"ee89c2307756e77b","lnir_raw_blob":"blake3:623c3fb337731d7c44ad7db1f6f25d194a79a4bc6bdb70aba61be56cd200dabd","lnir_canonical_debruijn_blob":"blake3:54e5a9f63a7f65f4f3437080f5f222be544361ef380d3c76fde770a106883c33","features":{"n_instr":9,"n_blocks":3,"n_loops":1,"max_loop_depth":1,"width_histogram":{"u64":7,"u256":0,"bool":0}}},"decision":{"step_idx":2,"pass_or_rule":"adversarial:unsound-alu-corruptor","theorem_or_rule":"UNTRUSTED_PR_CANDIDATE","pass_history":["builtin:algebraic-peephole","builtin:unbox-tuple-sroa"],"before_ir_blob":"blake3:623c3fb337731d7c44ad7db1f6f25d194a79a4bc6bdb70aba61be56cd200dabd","after_ir_blob":"blake3:7aa8a92588a45c4ff84d50831c2bbae0337dcdf0607d11b8026feff5967b83e4","after_debruijn_blob":"blake3:64957145407cf0982b51ddf31e34b27549fd14e20f277abe599c2a87633f44bc","proposer":{"kind":"adversarial_untrusted","notes":"Intentionally unsound ALU corruption to test Law 1 rejection gate"}},"validation":{"symbolic_tv":{"status":"failed","unroll_bound":4,"samples":64,"samples_ok":0,"ub_refines":true,"domain_equiv":true,"poison_refines":true,"sym_ret_equiv":false,"mem_writes_equiv":true},"kernel_check":{"status":"rejected","evidence_kind":"bounded_only","theorem_ref":"UNTRUSTED_PR_CANDIDATE","sorry_count":0}},"cost_model":{"cost_before":3,"cost_after":3},"rl_outcome":{"accepted_into_pipeline":false,"rejection_stage":"symbolic_tv","reward_components":{"cost_delta":0,"kernel_verified":0.0,"tv_passed":-1.0}},"received_at":"2026-10-21T21:23:23.475181+00:00"}],"turbo-lean":[{"accelerator_name":null,"accelerator_rewrite":false,"cache_hit":false,"compact_output_bytes":187,"decl_name":"buggy_de_morgan","elapsed_ms":0.212,"heartbeats":0,"raw_output_bytes":6000,"schema":"turbo-lean.telemetry.v1","stage1_tpu_ms":0.212,"stage1_tpu_reject":true,"stage2_zygote_ms":0.0,"tool_name":"turbo_fast_check","winning_tactic_hint":null,"zygote_verified":false,"event_id":"94f6fd1b3c9d61b7bc16a57a863f905c","received_at":"2026-10-21T21:27:56.702631+00:00"},{"accelerator_name":null,"accelerator_rewrite":false,"cache_hit":false,"compact_output_bytes":187,"decl_name":"buggy_de_morgan","elapsed_ms":0.186,"heartbeats":0,"raw_output_bytes":6000,"schema":"turbo-lean.telemetry.v1","stage1_tpu_ms":0.186,"stage1_tpu_reject":true,"stage2_zygote_ms":0.0,"tool_name":"turbo_fast_check","winning_tactic_hint":null,"zygote_verified":false,"event_id":"6e92d0cd75ec669ca63f9c9f4b051dce","received_at":"2026-10-21T21:27:56.702631+00:00"},{"accelerator_name":null,"accelerator_rewrite":false,"cache_hit":false,"compact_output_bytes":187,"decl_name":"buggy_de_morgan","elapsed_ms":0.197,"heartbeats":0,"raw_output_bytes":6000,"schema":"turbo-lean.telemetry.v1","stage1_tpu_ms":0.197,"stage1_tpu_reject":true,"stage2_zygote_ms":0.0,"tool_name":"turbo_fast_check","winning_tactic_hint":null,"zygote_verified":false,"event_id":"8c60dbfc1fe6dde0016b1e434dbd62ea","received_at":"2026-10-21T21:27:56.702631+00:00"},{"accelerator_name":null,"accelerator_rewrite":false,"cache_hit":false,"compact_output_bytes":187,"decl_name":"buggy_de_morgan","elapsed_ms":0.972,"heartbeats":0,"raw_output_bytes":6000,"schema":"turbo-lean.telemetry.v1","stage1_tpu_ms":0.972,"stage1_tpu_reject":true,"stage2_zygote_ms":0.0,"tool_name":"turbo_fast_check","winning_tactic_hint":null,"zygote_verified":false,"event_id":"f5fb84706b8f145f1d04f4d1a044a44f","received_at":"2026-10-21T21:27:56.702631+00:00"},{"accelerator_name":null,"accelerator_rewrite":false,"cache_hit":false,"compact_output_bytes":187,"decl_name":"buggy_de_morgan","elapsed_ms":0.208,"heartbeats":0,"raw_output_bytes":6000,"schema":"turbo-lean.telemetry.v1","stage1_tpu_ms":0.208,"stage1_tpu_reject":true,"stage2_zygote_ms":0.0,"tool_name":"turbo_fast_check","winning_tactic_hint":null,"zygote_verified":false,"event_id":"68fb6752388fb35463dae9aa6496fdbc","received_at":"2026-10-21T21:27:56.702631+00:00"}]}}