mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
863da04f21
Lean (reference), Python, Rust, C, C++, Go, Julia, R, Scala, Fortran, Coq, Octave — all implementing the same AVM ISA v1 specification. Every port implements: - Full type universe: Q0_16, Q16_16, Bool - 11 primitives with floor division (Lean Int.ediv), V6 signed comparison, symmetric clamping [-2147483647, 2147483647] - 12 instruction opcodes with stack depth limit (1024) - Fuel-bounded run loop - Error handling (stack under/overflow, type mismatch, div-by-zero, jump OOB)
62 lines
1.9 KiB
TeX
62 lines
1.9 KiB
TeX
COQAUX1 674cb8319be2cff2e3564b20efcaccb5 /home/allaun/SilverSight/coq/CoreFormalism/Q16_16.v
|
|
0 0 VernacProof "tac:no using:no"
|
|
164 168 proof_build_time "0.001"
|
|
0 0 le_neg2147483648_2147483647 "0.001"
|
|
159 163 context_used ""
|
|
164 168 proof_check_time "0.000"
|
|
0 0 VernacProof "tac:no using:no"
|
|
226 230 proof_build_time "0.000"
|
|
0 0 le_0_2147483647 "0.000"
|
|
221 225 context_used ""
|
|
226 230 proof_check_time "0.000"
|
|
0 0 VernacProof "tac:no using:no"
|
|
292 296 proof_build_time "0.000"
|
|
0 0 le_neg2147483648_0 "0.000"
|
|
287 291 context_used ""
|
|
292 296 proof_check_time "0.000"
|
|
0 0 VernacProof "tac:no using:no"
|
|
373 377 proof_build_time "0.000"
|
|
0 0 le_2147483647_2147483647 "0.000"
|
|
368 372 context_used ""
|
|
373 377 proof_check_time "0.000"
|
|
0 0 VernacProof "tac:no using:no"
|
|
1220 1224 proof_build_time "0.002"
|
|
0 0 clamp_bounded "0.002"
|
|
1183 1217 context_used ""
|
|
1220 1224 proof_check_time "0.001"
|
|
0 0 VernacProof "tac:no using:no"
|
|
1560 1564 proof_build_time "0.001"
|
|
0 0 clamp_idempotent "0.001"
|
|
1545 1557 context_used ""
|
|
1560 1564 proof_check_time "0.000"
|
|
0 0 VernacProof "tac:no using:no"
|
|
2259 2263 proof_build_time "0.000"
|
|
0 0 add_comm "0.000"
|
|
2214 2258 context_used ""
|
|
2259 2263 proof_check_time "0.000"
|
|
0 0 VernacProof "tac:no using:no"
|
|
2445 2449 proof_build_time "0.000"
|
|
0 0 add_in_range "0.000"
|
|
2396 2442 context_used ""
|
|
2445 2449 proof_check_time "0.000"
|
|
0 0 VernacProof "tac:no using:no"
|
|
2708 2712 proof_build_time "0.001"
|
|
0 0 sub_self "0.001"
|
|
2647 2705 context_used ""
|
|
2708 2712 proof_check_time "0.000"
|
|
0 0 VernacProof "tac:no using:no"
|
|
2818 2822 proof_build_time "0.000"
|
|
0 0 mul_comm "0.000"
|
|
2773 2817 context_used ""
|
|
2818 2822 proof_check_time "0.000"
|
|
0 0 VernacProof "tac:no using:no"
|
|
2973 2977 proof_build_time "0.000"
|
|
0 0 in_range_zero "0.000"
|
|
2914 2972 context_used ""
|
|
2973 2977 proof_check_time "0.000"
|
|
0 0 VernacProof "tac:no using:no"
|
|
3127 3131 proof_build_time "0.000"
|
|
0 0 in_range_one "0.000"
|
|
3068 3126 context_used ""
|
|
3127 3131 proof_check_time "0.000"
|
|
0 0 vo_compile_time "0.140"
|