downstream from https://github.com/SkyLabsAI/auto/pull/461

[simon-skylabs]

No description provided.

[skylabs-ai-ci]

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/brick-libcpp/	simon/only-provable-simp-prop	f442396	04a0552	main	8c403ee	#179
fmdeps/auto/	simon/only-provable-simp-prop	6356177	a58abcd	main	222147a	#461

Passive Repos

Repo	Job Branch	Job Commit
./	main	d0ca455
fmdeps/BRiCk/	main	837f50d
fmdeps/auto-docs/	main	9914064
bluerock/NOVA/	skylabs-proof	948378b
bluerock/bhv/	skylabs-main	3506c0b
fmdeps/ci/	main	c25c8df
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
vendored/rocq/	skylabs-master	bef7df5
fmdeps/rocq-agent-toolkit/	main	1e0e853
vendored/rocq-elpi/	skylabs-master	7dee592
vendored/rocq-equations/	skylabs-main	9cf8471
vendored/rocq-iris/	skylabs-master	a7af9f7
vendored/rocq-lsp/	skylabs-main	64ef78a
vendored/rocq-stdlib/	skylabs-master	00897b3
vendored/rocq-stdpp/	skylabs-master	0c5e505
fmdeps/skylabs-fm/	main	ff17057
vendored/vsrocq/	skylabs-main	ee79e7a

Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	0	${\color{red}15}$	0	15
Warnings	92	0	${\color{green}1}$	91

Performance

Relative	Master	MR	Change	Filename
-1.56%	199075.6	195963.8	-3111.8	total
-1.66%	3301.6	-	-3301.6	├ disappeared files (22)
+0.10%	195774.0	195963.8	+189.8	└ common files
+0.00%	53308.1	53308.1	+0.0	├ translation units
+0.13%	142465.9	142655.8	+189.8	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-34.75%	93.5	61.0	-32.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v
-27.04%	330.2	240.9	-89.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_main_proof.v
-17.10%	77.5	64.3	-13.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/array_string_init/main_cpp_proof.v
-16.48%	280.9	234.6	-46.3	fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_zip.v
-16.38%	273.3	228.5	-44.8	fmdeps/auto/brick_groundtruth/examples/loopcorpus/SubArrays.v
-16.38%	272.3	227.7	-44.6	fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays.v
-15.99%	273.3	229.6	-43.7	fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_While.v
-12.50%	52.7	46.1	-6.6	fmdeps/auto/brick_groundtruth/examples/loopcorpus/IntegerDivide_WhileTrueWithBreak.v
-11.41%	261.2	231.4	-29.8	fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_WhileTrueWithBreak.v
-10.23%	220.2	197.7	-22.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_main_proof.v
-9.83%	469.8	423.6	-46.2	fmdeps/auto/brick_groundtruth/examples/loopsynth/downward_loop.v
-8.20%	155.3	142.6	-12.7	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v
-7.95%	162.6	149.6	-12.9	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v
-6.54%	56.4	52.7	-3.7	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_f0_proof.v
-6.09%	849.8	798.0	-51.8	fmdeps/auto/brick_groundtruth/examples/loopsynth/za18_2.v
-4.17%	121.1	116.1	-5.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_main_proof.v
-3.94%	61.7	59.3	-2.4	bluerock/NOVA/build-proof/proof/pd_hpp_spec/triples.v
-1.88%	53.9	52.9	-1.0	fmdeps/auto/rocq-skylabs-auto-core/theories/internal/syntactic_bi.v
-1.60%	1579.0	1553.8	-25.2	fmdeps/auto/brick_groundtruth/examples/loopcorpus/MultipleLoops.v
-0.80%	738.1	732.2	-5.9	fmdeps/auto/brick_groundtruth/examples/loopsynth/Exp1_0_failure.v
-0.31%	467.0	465.5	-1.5	bluerock/NOVA/build-proof/proof/arch/memattr_hpp_proof.v
+0.17%	644.9	646.0	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/call_cpp_proof.v
+0.25%	408.6	409.6	+1.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/arith_cpp_proof.v
+0.35%	301.8	302.8	+1.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/read_write_proof.v
+1.14%	153.8	155.6	+1.8	fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v
+1.17%	513.7	519.7	+6.0	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v
+1.32%	848.3	859.4	+11.2	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/compare/test_cpp_proof.v
+1.36%	818.7	829.8	+11.2	fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/compare/test_cpp_proof.v
+1.60%	88.0	89.4	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_main_proof.v
+1.66%	98.8	100.4	+1.6	fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy_While.v
+1.79%	78.0	79.3	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/primitive_initialization.v
+2.07%	100.2	102.2	+2.1	fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy_DownwardForLoop.v
+2.10%	64.1	65.5	+1.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/read_prim/read_cpp_proof.v
+2.12%	79.3	81.0	+1.7	fmdeps/auto-docs/content/demo/forward_list_v1/test_cpp_proof.v
+2.20%	98.4	100.6	+2.2	fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy.v
+2.30%	54.0	55.3	+1.2	fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayZeroInitialization_DoWhile.v
+2.43%	79.4	81.4	+1.9	fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/pair_hpp_spec.v
+2.63%	87.4	89.7	+2.3	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/initializer_list/test_cpp_proof.v
+2.69%	104.0	106.8	+2.8	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/compound_assignment_increments.v
+2.95%	158.5	163.2	+4.7	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v
+2.96%	98.4	101.3	+2.9	fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy_WhileTrueWithBreak.v
+3.18%	32.3	33.3	+1.0	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/implicit_array_initialization.v
+3.21%	47.4	48.9	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/inits/main_cpp_spec.v
+3.24%	179.1	185.0	+5.8	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v
+3.25%	591.9	611.1	+19.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/test1_proof.v
+3.44%	99.9	103.3	+3.4	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/guard_recursive_cpp_proof.v
+3.47%	77.3	79.9	+2.7	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_main_proof.v
+4.04%	53.2	55.3	+2.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/if_switch_initializers.v
+4.13%	25.5	26.6	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/lazy/tactics/normalize.v
+4.20%	24.6	25.6	+1.0	fmdeps/auto-docs/content/docs/class_reps/alt.v
+4.34%	57.3	59.8	+2.5	fmdeps/auto/brick_groundtruth/examples/loopcorpus/DynamicArrayInitialization_DownwardForLoop.v
+4.49%	233.9	244.4	+10.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep_spec.v
+4.53%	30.3	31.7	+1.4	fmdeps/auto/brick_groundtruth/examples/loopcorpus/SumLocalArrayUsingRangeloop.v
+4.63%	279.4	292.3	+12.9	fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith_bug.v
+4.70%	25.4	26.6	+1.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/cpp_spec/template.v
+4.73%	37.0	38.8	+1.8	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_rounding_mode.v
+4.74%	24.9	26.1	+1.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/sub_const.v
+4.82%	24.1	25.2	+1.2	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/semaphore/test_cpp_proof.v
+5.13%	45.5	47.8	+2.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v
+5.17%	35.3	37.1	+1.8	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/control_logical_forms.v
+5.24%	60.8	64.0	+3.2	fmdeps/auto/brick_groundtruth/examples/loopcorpus/DynamicArrayInitialization.v
+5.39%	60.4	63.7	+3.3	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/memory/test_cpp_proof.v
+5.72%	32.4	34.3	+1.9	fmdeps/auto/rocq-skylabs-auto-cpp/tests/aggregate_arrays/proof.v
+5.84%	29.6	31.4	+1.7	fmdeps/auto/brick_groundtruth/examples/loopcorpus/test_ssridents.v
+5.85%	34.1	36.1	+2.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_f0_proof.v
+5.97%	18.7	19.8	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f2_proof.v
+6.14%	27.0	28.7	+1.7	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f3_proof.v
+6.35%	22.7	24.1	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v
+6.41%	98.8	105.1	+6.3	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/destructuring_declarations.v
+6.45%	50.7	54.0	+3.3	fmdeps/auto/brick_groundtruth/examples/loopcorpus/SumUpToN.v
+6.51%	36.0	38.3	+2.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f0_proof.v
+6.69%	71.6	76.3	+4.8	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v
+6.77%	63.5	67.8	+4.3	fmdeps/auto/brick_groundtruth/examples/loopcorpus/IntegerDivide.v
+6.96%	22.5	24.1	+1.6	fmdeps/auto/rocq-skylabs-auto-cpp/tests/virtual/virtual_cpp_proof.v
+7.06%	76.5	81.9	+5.4	fmdeps/auto-docs/content/demo/linked_list/linked_list_cpp_proof.v
+7.19%	60.6	64.9	+4.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/wp_lval_op_assign_variants.v
+7.38%	19.9	21.4	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f1_proof.v
+7.43%	44.7	48.0	+3.3	fmdeps/auto/brick_groundtruth/examples/loopcorpus/SumUpToN_WhileTrueWithBreak.v
+7.58%	15.2	16.4	+1.2	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/iostream_trace/pred.v
+7.63%	41.0	44.1	+3.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/anyR_proof.v
+7.92%	29.5	31.9	+2.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/factor.v
+7.97%	29.2	31.6	+2.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v
+8.15%	20.4	22.1	+1.7	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f2_proof.v
+8.81%	27.1	29.5	+2.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v
+8.81%	809.5	880.8	+71.3	fmdeps/auto/brick_groundtruth/examples/loopcorpus/identityloop.v
+8.99%	23.5	25.7	+2.1	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/shared_mutex/test_cpp_proof.v
+9.21%	44.9	49.0	+4.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/control_flow/main_cpp_spec.v
+9.28%	49.0	53.5	+4.5	fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayZeroInitialization.v
+9.32%	28.4	31.0	+2.6	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/nullptr_reads.v
+9.61%	36.2	39.7	+3.5	fmdeps/auto-docs/content/docs/functions/verification.v
+9.70%	19.9	21.8	+1.9	fmdeps/auto/rocq-skylabs-auto-cpp/tests/normalization/test.v
+9.78%	84.3	92.6	+8.2	fmdeps/auto/brick_groundtruth/examples/loopcorpus/CountPositives.v
+9.81%	32.0	35.2	+3.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_f0_proof.v
+10.09%	47.6	52.4	+4.8	fmdeps/auto/brick_groundtruth/examples/loopcorpus/Power_WhileTrueWithBreak.v
+10.31%	48.6	53.6	+5.0	fmdeps/auto/brick_groundtruth/examples/loopcorpus/Factorial.v
+10.64%	63.4	70.1	+6.7	fmdeps/auto/brick_groundtruth/examples/loopcorpus/ReverseArray.v
+11.30%	20.1	22.4	+2.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_f0_proof.v
+11.67%	20.6	23.0	+2.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f1_proof.v
+12.02%	8.8	9.9	+1.1	fmdeps/auto/rocq-skylabs-plib/theories/plist_bigop.v
+12.08%	20.3	22.7	+2.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f1_proof.v
+12.31%	36.4	40.8	+4.5	fmdeps/auto-docs/content/docs/control_flow/if.v
+12.71%	15.4	17.3	+2.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_f1_proof.v
+12.74%	106.2	119.8	+13.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/basic.v
+13.09%	26.0	29.4	+3.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/verify/template_specialization.v
+13.21%	154.8	175.3	+20.5	fmdeps/auto/brick_groundtruth/examples/loopsynth/replicate_example_0.v
+13.39%	777.3	881.4	+104.1	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/array/test_cpp_proof.v
+13.58%	16.8	19.1	+2.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg.v
+14.07%	49.1	56.0	+6.9	fmdeps/auto/brick_groundtruth/examples/loopcorpus/Power.v
+15.22%	28.2	32.5	+4.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f0_proof.v
+17.01%	16.4	19.2	+2.8	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/two_dimensional_arrays.v
+17.18%	16.5	19.4	+2.8	fmdeps/auto/rocq-skylabs-auto-cpp/tests/return_void/main_cpp_proof.v
+19.25%	14.9	17.7	+2.9	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f2_proof.v
+20.81%	15.1	18.2	+3.1	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/semaphore/proof/release.v
+25.91%	4.7	5.9	+1.2	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/diff.v
+26.80%	4.0	5.0	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/theories/cpp/spec/ltac2.v
+28.37%	30.6	39.2	+8.7	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f1_proof.v
+29.20%	27.2	35.1	+7.9	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f0_proof.v
+29.65%	3.5	4.6	+1.0	fmdeps/auto/rocq-skylabs-simp/theories/classes/util.v
+29.70%	3.5	4.6	+1.0	fmdeps/auto/rocq-skylabs-simp/theories/classes/simp_prop.v
+29.92%	4.0	5.3	+1.2	fmdeps/auto/rocq-skylabs-auto-core/examples/classes/bwd.v
+30.47%	32.7	42.6	+10.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v
+33.24%	4.1	5.5	+1.4	fmdeps/auto/rocq-skylabs-auto-core/theories/internal/stdlib.v
+33.49%	3.5	4.7	+1.2	fmdeps/auto/rocq-skylabs-auto-core/examples/classes/fwd.v
+34.54%	63.9	86.0	+22.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f2_proof.v
+36.32%	3.3	4.5	+1.2	fmdeps/auto/rocq-skylabs-auto-core/theories/internal/lib/guard.v
+36.84%	3.5	4.8	+1.3	fmdeps/auto/rocq-skylabs-auto-core/theories/hints/classes/factoring.v
+38.21%	3.1	4.3	+1.2	fmdeps/auto/rocq-skylabs-auto-core/theories/internal/lib/learn.v
+38.37%	10.5	14.5	+4.0	fmdeps/auto/rocq-skylabs-auto-core/tests/warnings.v
+38.52%	3.1	4.3	+1.2	fmdeps/auto/rocq-skylabs-auto-core/tests/learn.v
+39.00%	3.0	4.2	+1.2	fmdeps/auto/rocq-skylabs-auto-core/theories/internal/ltac2/telescopes.v
+39.79%	3.4	4.8	+1.4	fmdeps/auto/rocq-skylabs-plib/theories/make.v
+41.87%	3.1	4.4	+1.3	fmdeps/auto/rocq-skylabs-auto-core/theories/hints/classes/bwd.v
+41.91%	3.1	4.4	+1.3	fmdeps/auto/rocq-skylabs-auto-core/theories/hints/classes/fwd.v
+46.97%	131.5	193.3	+61.8	fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/unit_tests.v
-1.56%	199075.6	195963.8	-3111.8	total
-1.66%	3301.6	-	-3301.6	├ disappeared files (22)
+0.10%	195774.0	195963.8	+189.8	└ common files
+0.00%	53308.1	53308.1	+0.0	├ translation units
+0.13%	142465.9	142655.8	+189.8	└ proofs and tests