Transitive dependencies for floating point

[gmalecha-at-skylabs]

Downstream of SkyLabsAI/BRiCk#163

[skylabs-ai-ci]

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Base branch	Base commit	PR
fmdeps/brick-libcpp/	float-support	5aa93f2	main	2db67b0	#65
fmdeps/BRiCk/	float-support	26d942a	main	094eace	#163
fmdeps/auto/	float-support	e60e36c	main	3abb4b4	#239
fmdeps/fm-tools/	float-support	11018a4	main	fb160a9 ( ⚠️ needs rebase)	-
psi/data/	float-support	943730b	main	76acc2f ( ⚠️ needs rebase)	-
fmdeps/skylabs-fm/	float-support	0b444d2	main	06f1cd3	#268

Passive Repos

Repo	Job Branch	Job Commit
./	main	7d2ee30
fmdeps/auto-docs/	main	d4c3641
bluerock/NOVA/	skylabs-proof	dc3d314
bluerock/bhv/	skylabs-main	a803e73
fmdeps/ci/	main	e54841c
vendored/elpi/	skylabs-master	aa4475f
vendored/flocq/	skylabs-master	cf9cc84
psi/protos/	main	8fe3e7c
psi/backend/	main	0b5fea6
psi/ide/	main	6b596cf
vendored/rocq/	skylabs-master	2ede3c9
fmdeps/rocq-agent-toolkit/	main	3eed23a
vendored/rocq-elpi/	skylabs-master	103a742
vendored/rocq-equations/	skylabs-main	a8c4832
vendored/rocq-ext-lib/	skylabs-master	94a6630
vendored/rocq-iris/	skylabs-master	3ad4ddd
vendored/rocq-lsp/	skylabs-main	a8b7272
vendored/rocq-stdlib/	skylabs-master	bc07423
vendored/rocq-stdpp/	skylabs-master	e01d802
vendored/vsrocq/	skylabs-main	5b4527e

Performance

Relative	Master	MR	Change	Filename
+1.22%	127618.5	129173.0	+1554.6	total
+0.49%	-	633.2	+633.2	├ newly appeared files (5)
+0.72%	128539.8	127618.5	+921.3	└ common files
+1.39%	23117.2	22800.3	+316.9	├ translation units
+0.58%	105422.6	104818.2	+604.4	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-7.62%	32.7	30.2	-2.5	bluerock/bhv/lib/vrl/proof/vrl/dataplane_hpp_spec.v
-7.09%	35.2	32.7	-2.5	bluerock/bhv/apps/vmm/lib/vmi_interface/proof/vmi_interface_hpp_spec.v
-6.21%	40.7	38.2	-2.5	bluerock/bhv/lib/vrl/proof/vrl/port_list_hints.v
-3.35%	81.6	78.9	-2.7	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/base_startup_handler.v
-0.60%	192.5	191.4	-1.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v
-0.40%	393.0	391.4	-1.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/extract_frame_header.v
-0.38%	380.3	378.8	-1.4	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_sm.v
-0.35%	546.3	544.4	-1.9	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_pd.v
-0.27%	554.8	553.3	-1.5	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sc.v
-0.14%	726.6	725.6	-1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v
+0.11%	1699.0	1701.0	+1.9	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_glue.v
+0.13%	781.1	782.1	+1.1	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_proof.v
+0.15%	895.1	896.4	+1.3	fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/atomic/test_cpp_proof.v
+0.15%	1693.3	1695.9	+2.6	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/reset.v
+0.18%	650.5	651.7	+1.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/misc.v
+0.21%	538.4	539.6	+1.1	bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/ready_queues.v
+0.23%	485.3	486.4	+1.1	bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_cpp_proof.v
+0.30%	348.1	349.2	+1.0	bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/proof.v
+0.33%	464.6	466.1	+1.5	bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_private.v
+0.38%	475.2	477.0	+1.8	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/msr_framework.v
+0.38%	358.0	359.4	+1.4	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort.v
+0.41%	527.2	529.4	+2.1	bluerock/bhv/lib/drivers/serial/pl011/proof/pl011_cpp_proof.v
+0.43%	415.4	417.1	+1.8	bluerock/bhv/apps/vmm/lib/board/include/x86/board_impl_hpp.v
+0.44%	972.9	977.2	+4.3	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_cpp_proof.v
+0.56%	225.3	226.6	+1.3	bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_read_console_id.v
+0.58%	190.7	191.8	+1.1	bluerock/bhv/zeta/apps/msc/include/msc/aarch64_hp_hpp.v
+0.64%	169.9	171.0	+1.1	bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_other.v
+0.68%	156.9	158.0	+1.1	bluerock/bhv/zeta/lib/nova/proof/safe_proof/safe_proof.v
+0.71%	201.7	203.1	+1.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/hints.v
+0.77%	575.9	580.4	+4.5	bluerock/bhv/apps/vmm/src/aarch64_main_cpp.v
+0.90%	129.3	130.5	+1.2	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/cpu_hpp_properties.v
+0.93%	229.6	231.7	+2.1	bluerock/bhv/apps/umx/proof/main_cpp_proof/user_handler.v
+0.99%	339.6	343.0	+3.4	bluerock/bhv/apps/vmm/lib/board/include/model/aarch64_board_common_hpp.v
+1.01%	426.7	431.0	+4.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/arith_cpp_proof.v
+1.21%	85.0	86.1	+1.0	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/switch.v
+1.25%	80.1	81.1	+1.0	bluerock/bhv/zeta/lib/cxx/proof/sys/mutex_hpp_proof.v
+1.31%	317.9	322.0	+4.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/read_write_proof.v
+1.43%	245.6	249.1	+3.5	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/TO_UPSTREAM.v
+1.68%	78.3	79.6	+1.3	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/primitive_initialization.v
+1.70%	65.4	66.5	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/prepost_loops.v
+1.75%	57.9	58.9	+1.0	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/genv_tu.v
+2.37%	71.7	73.4	+1.7	fmdeps/auto/rocq-skylabs-auto-cpp/theories/base_logic/lib/rinv.v
+2.59%	40.8	41.8	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/lazy/auto_frac/hints.v
+2.79%	39.0	40.0	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/theories/lib/pred_utils.v
+2.87%	48.6	50.0	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/pretty/my_pretty_internals.v
+2.89%	42.7	44.0	+1.2	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/templates/verif/pattern.v
+2.98%	373.1	384.3	+11.1	fmdeps/auto/rocq-skylabs-cpp-stdlib/theories/vector/inc_vector_cpp.v
+3.00%	37.4	38.5	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/layout.v
+3.81%	48.3	50.1	+1.8	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/operators.v
+3.87%	61.7	64.1	+2.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v
+6.47%	20.5	21.9	+1.3	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/ptrs/valid.v
+8.06%	13.9	15.0	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/prim.v
+9.06%	12.4	13.6	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/lazy/auto_frac/tmp_classy_reify.v
+11.10%	14.8	16.4	+1.6	bluerock/bhv/apps/vswitch/proof/model/vswitch/defs.v
+11.25%	14.3	15.9	+1.6	bluerock/NOVA/build-proof/proof/mtd_hpp_spec.v
+11.73%	15.0	16.7	+1.8	bluerock/bhv/apps/vswitch/lib/util/proof/trace_hpp_spec.v
+12.15%	14.4	16.1	+1.7	bluerock/NOVA/build-proof/proof/kobject_hpp_spec/subclass.v
+12.24%	14.1	15.8	+1.7	bluerock/bhv/zeta/lib/fdt/proof/as_hpp_spec.v
+12.28%	12.4	13.9	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/has_type.v
+12.46%	11.7	13.1	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/dataclass_tests.v
+14.70%	18.9	21.7	+2.8	bluerock/NOVA/build-proof/proof/pd_hpp_spec/prelude.v
+81.88%	32.4	58.9	+26.5	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/cast.v
+1.22%	127618.5	129173.0	+1554.6	total
+0.49%	-	633.2	+633.2	├ newly appeared files (5)
+0.72%	128539.8	127618.5	+921.3	└ common files
+1.39%	23117.2	22800.3	+316.9	├ translation units
+0.58%	105422.6	104818.2	+604.4	└ proofs and tests