X-Lang logo
GitHub
Data Artifacts

Raw VTune CSVs and Lean/Alive2 Proof Scripts

The /data route indexes raw benchmark and proof artifacts directly from this repository. Use the Open Raw buttons to open files from the repository raw source.

VTune CSVs

144

Lean Proofs

14

Alive2 Scripts

14

VTune Raw CSV Exports

CSV artifacts under benchmarks/full/**/vtune* including uarch, hotspots, memory-access, and summary exports.

benchmark data
  • benchmarks/full/become/benchmark/vtune_reports_become/C++ iterative_O3_uarch.csvOpen Raw
  • benchmarks/full/become/benchmark/vtune_reports_become/X-Lang become_O3_uarch.csvOpen Raw
  • benchmarks/full/become/benchmark/vtune_reports_become/X-Lang iterative_O3_uarch.csvOpen Raw
  • benchmarks/full/become/vtune_results/r_baseline/summary_export.csvOpen Raw
  • benchmarks/full/become/vtune_results/r_baseline_uarch/summary_export.csvOpen Raw
  • benchmarks/full/become/vtune_results/r_tco/summary_export.csvOpen Raw
  • benchmarks/full/become/vtune_results/r_tco_uarch/summary_export.csvOpen Raw
  • benchmarks/full/invariant/bench/cpp/vtune_results/bounded_vec_forced_hotspots.result/bounded_vec_forced_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/invariant/bench/cpp/vtune_results/bounded_vec_forced_hotspots.result/bounded_vec_forced_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/invariant/bench/cpp/vtune_results/bounded_vec_forced_memory-access.result/bounded_vec_forced_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/invariant/bench/cpp/vtune_results/bounded_vec_forced_uarch.result/bounded_vec_forced_uarch_summary_report.csvOpen Raw
  • benchmarks/full/invariant/bench/cpp/vtune_results/bounded_vec_optimised_hotspots.result/bounded_vec_optimised_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/invariant/bench/cpp/vtune_results/bounded_vec_optimised_hotspots.result/bounded_vec_optimised_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/invariant/bench/cpp/vtune_results/bounded_vec_optimised_memory-access.result/bounded_vec_optimised_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/invariant/bench/cpp/vtune_results/bounded_vec_optimised_uarch.result/bounded_vec_optimised_uarch_summary_report.csvOpen Raw
  • benchmarks/full/invariant/bench/cpp/vtune_summary.csvOpen Raw
  • benchmarks/full/invariant/bench/vtune_results/bounded_vec_invariant_optimized_hotspots.result/bounded_vec_invariant_optimized_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/invariant/bench/vtune_results/bounded_vec_invariant_optimized_hotspots.result/bounded_vec_invariant_optimized_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/invariant/bench/vtune_results/bounded_vec_invariant_optimized_memory-access.result/bounded_vec_invariant_optimized_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/invariant/bench/vtune_results/bounded_vec_invariant_optimized_uarch.result/bounded_vec_invariant_optimized_uarch_summary_report.csvOpen Raw
  • benchmarks/full/invariant/bench/vtune_results/bounded_vec_redundant_check_hotspots.result/bounded_vec_redundant_check_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/invariant/bench/vtune_results/bounded_vec_redundant_check_hotspots.result/bounded_vec_redundant_check_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/invariant/bench/vtune_results/bounded_vec_redundant_check_memory-access.result/bounded_vec_redundant_check_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/invariant/bench/vtune_results/bounded_vec_redundant_check_uarch.result/bounded_vec_redundant_check_uarch_summary_report.csvOpen Raw
  • benchmarks/full/invariant/bench/vtune_summary.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd2d_poly_aos_hotspots.result/fdtd2d_poly_aos_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd2d_poly_aos_hotspots.result/fdtd2d_poly_aos_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd2d_poly_aos_memory-access.result/fdtd2d_poly_aos_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd2d_poly_aos_uarch.result/fdtd2d_poly_aos_uarch_summary_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd2d_poly_soa_hotspots.result/fdtd2d_poly_soa_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd2d_poly_soa_hotspots.result/fdtd2d_poly_soa_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd2d_poly_soa_memory-access.result/fdtd2d_poly_soa_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd2d_poly_soa_uarch.result/fdtd2d_poly_soa_uarch_summary_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd_aos_hotspots.result/fdtd_aos_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd_aos_hotspots.result/fdtd_aos_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd_aos_memory-access.result/fdtd_aos_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd_aos_uarch.result/fdtd_aos_uarch_summary_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd_soa_hotspots.result/fdtd_soa_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd_soa_hotspots.result/fdtd_soa_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd_soa_memory-access.result/fdtd_soa_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_results/fdtd_soa_uarch.result/fdtd_soa_uarch_summary_report.csvOpen Raw
  • benchmarks/full/layout/bench/vtune_summary.csvOpen Raw
  • benchmarks/full/memoise/bench/vtune_cpp_results/fib_memo_hotspots_report.csvOpen Raw
  • benchmarks/full/memoise/bench/vtune_cpp_results/fib_normal_hotspots_report.csvOpen Raw
  • benchmarks/full/multi/vtune/collision_visitor_o3_hotspots.csvOpen Raw
  • benchmarks/full/multi/vtune/collision_visitor_o3_hw_events.csvOpen Raw
  • benchmarks/full/multi/vtune/collision_visitor_o3_hw_events_full.csvOpen Raw
  • benchmarks/full/multi/vtune/vtune_cpp_c_summary_O3.csvOpen Raw
  • benchmarks/full/multi/vtune/vtune_reports copy/C Manual_O3_uarch.csvOpen Raw
  • benchmarks/full/multi/vtune/vtune_reports copy/C++ Manual_O3_uarch.csvOpen Raw
  • benchmarks/full/multi/vtune/vtune_reports copy/C++ Visitor_O3_uarch.csvOpen Raw
  • benchmarks/full/multi/vtune/vtune_reports copy/X-Lang Manual_O3_uarch.csvOpen Raw
  • benchmarks/full/multi/vtune/vtune_reports copy/X-Lang Multi_O3_uarch.csvOpen Raw
  • benchmarks/full/multi/vtune/vtune_reports/C Manual_O3_uarch.csvOpen Raw
  • benchmarks/full/multi/vtune/vtune_reports/C++ Manual_O3_uarch.csvOpen Raw
  • benchmarks/full/multi/vtune/vtune_reports/C++ Visitor_O3_uarch.csvOpen Raw
  • benchmarks/full/multi/vtune/vtune_reports/X-Lang Manual_O3_uarch.csvOpen Raw
  • benchmarks/full/multi/vtune/vtune_reports/X-Lang Multi_O3_uarch.csvOpen Raw
  • benchmarks/full/parallel/a/vtune_results/grayscale_parallel_hotspots.result/grayscale_parallel_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/parallel/a/vtune_results/grayscale_parallel_hotspots.result/grayscale_parallel_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/parallel/a/vtune_results/grayscale_parallel_memory-access.result/grayscale_parallel_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/parallel/a/vtune_results/grayscale_parallel_uarch.result/grayscale_parallel_uarch_summary_report.csvOpen Raw
  • benchmarks/full/parallel/a/vtune_results/grayscale_sequential_hotspots.result/grayscale_sequential_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/parallel/a/vtune_results/grayscale_sequential_hotspots.result/grayscale_sequential_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/parallel/a/vtune_results/grayscale_sequential_memory-access.result/grayscale_sequential_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/parallel/a/vtune_results/grayscale_sequential_uarch.result/grayscale_sequential_uarch_summary_report.csvOpen Raw
  • benchmarks/full/parallel/a/vtune_summary.csvOpen Raw
  • benchmarks/full/parallel/vtune_results/grayscale_parallel_8_hotspots.result/grayscale_parallel_8_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/parallel/vtune_results/grayscale_parallel_8_hotspots.result/grayscale_parallel_8_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/parallel/vtune_results/grayscale_parallel_8_memory-access.result/grayscale_parallel_8_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/parallel/vtune_results/grayscale_parallel_8_uarch.result/grayscale_parallel_8_uarch_summary_report.csvOpen Raw
  • benchmarks/full/parallel/vtune_results/grayscale_sequential_built_hotspots.result/grayscale_sequential_built_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/parallel/vtune_results/grayscale_sequential_built_hotspots.result/grayscale_sequential_built_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/parallel/vtune_results/grayscale_sequential_built_memory-access.result/grayscale_sequential_built_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/parallel/vtune_results/grayscale_sequential_built_uarch.result/grayscale_sequential_built_uarch_summary_report.csvOpen Raw
  • benchmarks/full/parallel/vtune_summary.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/opaque_cpp_hotspots.result/opaque_cpp_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/opaque_cpp_hotspots.result/opaque_cpp_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/opaque_cpp_memory-access.result/opaque_cpp_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/opaque_cpp_uarch.result/opaque_cpp_uarch_summary_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/opaque_hotspots.result/opaque_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/opaque_hotspots.result/opaque_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/opaque_memory-access.result/opaque_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/opaque_uarch.result/opaque_uarch_summary_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/pure_cpp_hotspots.result/pure_cpp_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/pure_cpp_hotspots.result/pure_cpp_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/pure_cpp_memory-access.result/pure_cpp_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/pure_cpp_uarch.result/pure_cpp_uarch_summary_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/pure_hotspots.result/pure_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/pure_hotspots.result/pure_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/pure_memory-access.result/pure_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_results/pure_uarch.result/pure_uarch_summary_report.csvOpen Raw
  • benchmarks/full/pure/bench/vtune_summary.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_normal_cpp_hotspots.result/regex_normal_cpp_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_normal_cpp_hotspots.result/regex_normal_cpp_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_normal_cpp_memory-access.result/regex_normal_cpp_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_normal_cpp_uarch.result/regex_normal_cpp_uarch_summary_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_normal_hotspots.result/regex_normal_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_normal_hotspots.result/regex_normal_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_normal_memory-access.result/regex_normal_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_normal_uarch.result/regex_normal_uarch_summary_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_static_cpp_hotspots.result/regex_static_cpp_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_static_cpp_hotspots.result/regex_static_cpp_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_static_cpp_memory-access.result/regex_static_cpp_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_static_cpp_uarch.result/regex_static_cpp_uarch_summary_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_static_hotspots.result/regex_static_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_static_hotspots.result/regex_static_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_static_memory-access.result/regex_static_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_results/regex_static_uarch.result/regex_static_uarch_summary_report.csvOpen Raw
  • benchmarks/full/static/bench/vtune_summary.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/fast_hotspots.result/fast_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/fast_hotspots.result/fast_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/fast_memory-access.result/fast_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/fast_uarch.result/fast_uarch_summary_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/nothrows_cpp_hotspots.result/nothrows_cpp_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/nothrows_cpp_hotspots.result/nothrows_cpp_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/nothrows_cpp_memory-access.result/nothrows_cpp_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/nothrows_cpp_uarch.result/nothrows_cpp_uarch_summary_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/slow_ilp_hotspots.result/slow_ilp_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/slow_ilp_hotspots.result/slow_ilp_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/slow_ilp_memory-access.result/slow_ilp_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/slow_ilp_uarch.result/slow_ilp_uarch_summary_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/throws_cpp_hotspots.result/throws_cpp_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/throws_cpp_hotspots.result/throws_cpp_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/throws_cpp_memory-access.result/throws_cpp_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_results/throws_cpp_uarch.result/throws_cpp_uarch_summary_report.csvOpen Raw
  • benchmarks/full/throws/bench/new/vtune_summary.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/aliased_hotspots.result/aliased_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/aliased_hotspots.result/aliased_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/aliased_memory-access.result/aliased_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/aliased_uarch.result/aliased_uarch_summary_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/gemm_normal_hotspots.result/gemm_normal_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/gemm_normal_hotspots.result/gemm_normal_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/gemm_normal_memory-access.result/gemm_normal_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/gemm_normal_uarch.result/gemm_normal_uarch_summary_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/gemm_unique_hotspots.result/gemm_unique_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/gemm_unique_hotspots.result/gemm_unique_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/gemm_unique_memory-access.result/gemm_unique_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/gemm_unique_uarch.result/gemm_unique_uarch_summary_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/restricted_hotspots.result/restricted_hotspots_hotspots_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/restricted_hotspots.result/restricted_hotspots_summary_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/restricted_memory-access.result/restricted_memory-access_summary_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_results/restricted_uarch.result/restricted_uarch_summary_report.csvOpen Raw
  • benchmarks/full/unique/bench/vtune_summary.csvOpen Raw

Lean Proof Scripts

First-party Lean theorem files under crates/x-proofs-lean (excluding vendored .lake dependencies).

formal methods
  • crates/x-proofs-lean/Main.leanOpen Raw
  • crates/x-proofs-lean/XProofs.leanOpen Raw
  • crates/x-proofs-lean/XProofs/Advisor.leanOpen Raw
  • crates/x-proofs-lean/XProofs/Basic.leanOpen Raw
  • crates/x-proofs-lean/XProofs/Become.leanOpen Raw
  • crates/x-proofs-lean/XProofs/Invariant.leanOpen Raw
  • crates/x-proofs-lean/XProofs/Layout.leanOpen Raw
  • crates/x-proofs-lean/XProofs/Memoise.leanOpen Raw
  • crates/x-proofs-lean/XProofs/Multi.leanOpen Raw
  • crates/x-proofs-lean/XProofs/Parallel.leanOpen Raw
  • crates/x-proofs-lean/XProofs/Pure.leanOpen Raw
  • crates/x-proofs-lean/XProofs/Static.leanOpen Raw
  • crates/x-proofs-lean/XProofs/Throws.leanOpen Raw
  • crates/x-proofs-lean/XProofs/Unique.leanOpen Raw

Alive2 Scripts

Alive2 translation-validation scripts from crates/x-proofs-alive (.tv and related script formats).

translation validation
  • crates/x-proofs-alive/become.tvOpen Raw
  • crates/x-proofs-alive/done/become.tvOpen Raw
  • crates/x-proofs-alive/done/invariant.tvOpen Raw
  • crates/x-proofs-alive/done/layout.tvOpen Raw
  • crates/x-proofs-alive/done/memoise.tvOpen Raw
  • crates/x-proofs-alive/done/multi.tvOpen Raw
  • crates/x-proofs-alive/done/parallel.tvOpen Raw
  • crates/x-proofs-alive/done/pure.tvOpen Raw
  • crates/x-proofs-alive/done/static.tvOpen Raw
  • crates/x-proofs-alive/done/throws.tvOpen Raw
  • crates/x-proofs-alive/done/unique.tvOpen Raw
  • crates/x-proofs-alive/invariant.tvOpen Raw
  • crates/x-proofs-alive/throws.tvOpen Raw
  • crates/x-proofs-alive/unique.tvOpen Raw

Route Contract

This page links only these artifact classes: CSV files in VTune-related directories, Lean .lean scripts in crates/x-proofs-lean, and Alive2 script files in crates/x-proofs-alive.