allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
SilverSight/coq/CoreFormalism/Q16_16.glob
allaun 863da04f21 feat(avm-ports): port AVM ISA to all 12 scientific languages 
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)
2026-06-30 17:42:38 -05:00

263 lines
9.8 KiB
Text
Raw Permalink Blame History

DIGEST 674cb8319be2cff2e3564b20efcaccb5
FQ16_16
R72:77 Stdlib.ZArith.ZArith <> <> lib
R79:81 Stdlib.micromega.Lia <> <> lib
prf 91:117 <> le_neg2147483648_2147483647
R133:136 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not
prf 175:189 <> le_0_2147483647
R195:198 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not
prf 237:254 <> le_neg2147483648_0
R270:273 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not
prf 304:327 <> le_2147483647_2147483647
R342:345 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not
mod 386:391 <> Q16_16
def 430:440 Q16_16 q16_min_raw
R444:444 Corelib.Numbers.BinNums <> Z ind
def 475:485 Q16_16 q16_max_raw
R489:489 Corelib.Numbers.BinNums <> Z ind
def 519:527 Q16_16 q16_scale
R532:532 Corelib.Numbers.BinNums <> Z ind
def 558:565 Q16_16 in_range
R572:572 Corelib.Numbers.BinNums <> Z ind
binder 568:568 <> x:1
R605:608 Corelib.Init.Logic <> ::type_scope:x_'/\'_x not
R600:603 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not
R589:599 Q16_16 Q16_16 q16_min_raw def
R604:604 Q16_16 <> x:1 var
R610:613 Stdlib.ZArith.BinInt <> ::Z_scope:x_'<='_x not
R609:609 Q16_16 <> x:1 var
R614:624 Q16_16 Q16_16 q16_max_raw def
def 641:649 Q16_16 clamp_raw
R656:656 Corelib.Numbers.BinNums <> Z ind
binder 652:652 <> i:2
R661:661 Corelib.Numbers.BinNums <> Z ind
R673:680 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def
R694:694 Q16_16 <> i:2 var
R682:692 Q16_16 Q16_16 q16_max_raw def
R725:732 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def
R736:746 Q16_16 Q16_16 q16_min_raw def
R734:734 Q16_16 <> i:2 var
R774:774 Q16_16 <> i:2 var
R753:763 Q16_16 Q16_16 q16_min_raw def
R701:711 Q16_16 Q16_16 q16_max_raw def
prf 788:800 Q16_16 clamp_bounded
R807:807 Corelib.Numbers.BinNums <> Z ind
binder 803:803 <> x:3
R812:819 Q16_16 Q16_16 in_range def
R822:830 Q16_16 Q16_16 clamp_raw def
R832:832 Q16_16 <> x:3 var
R856:864 Q16_16 Q16_16 clamp_raw def
R867:874 Q16_16 Q16_16 in_range def
R887:894 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def
R896:906 Q16_16 Q16_16 q16_max_raw def
R887:894 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def
R896:906 Q16_16 Q16_16 q16_max_raw def
R936:946 Q16_16 Q16_16 q16_min_raw def
R949:959 Q16_16 Q16_16 q16_max_raw def
R976:1002 Q16_16 <> le_neg2147483648_2147483647 thm
R1012:1020 Stdlib.ZArith.BinInt Z le_refl thm
R976:1002 Q16_16 <> le_neg2147483648_2147483647 thm
R1012:1020 Stdlib.ZArith.BinInt Z le_refl thm
R1036:1043 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def
R1047:1057 Q16_16 Q16_16 q16_min_raw def
R1036:1043 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def
R1047:1057 Q16_16 Q16_16 q16_min_raw def
R1087:1097 Q16_16 Q16_16 q16_min_raw def
R1100:1110 Q16_16 Q16_16 q16_max_raw def
R1127:1135 Stdlib.ZArith.BinInt Z le_refl thm
R1145:1171 Q16_16 <> le_neg2147483648_2147483647 thm
R1127:1135 Stdlib.ZArith.BinInt Z le_refl thm
R1145:1171 Q16_16 <> le_neg2147483648_2147483647 thm
R1196:1203 Stdlib.ZArith.BinInt Z nlt_ge thm
R1196:1203 Stdlib.ZArith.BinInt Z nlt_ge thm
R1196:1203 Stdlib.ZArith.BinInt Z nlt_ge thm
prf 1236:1251 Q16_16 clamp_idempotent
R1258:1258 Corelib.Numbers.BinNums <> Z ind
binder 1254:1254 <> x:4
R1266:1273 Q16_16 Q16_16 in_range def
R1275:1275 Q16_16 <> x:4 var
binder 1262:1262 <> h:5
R1291:1293 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R1280:1288 Q16_16 Q16_16 clamp_raw def
R1290:1290 Q16_16 <> x:4 var
R1294:1294 Q16_16 <> x:4 var
R1346:1354 Q16_16 Q16_16 clamp_raw def
R1367:1374 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def
R1376:1386 Q16_16 Q16_16 q16_max_raw def
R1421:1430 Stdlib.ZArith.Zorder <> Zlt_not_le thm
R1367:1374 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def
R1376:1386 Q16_16 Q16_16 q16_max_raw def
R1421:1430 Stdlib.ZArith.Zorder <> Zlt_not_le thm
R1459:1466 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def
R1470:1480 Q16_16 Q16_16 q16_min_raw def
R1513:1522 Stdlib.ZArith.Zorder <> Zlt_not_le thm
R1459:1466 Stdlib.ZArith.ZArith_dec <> Z_lt_dec def
R1470:1480 Q16_16 Q16_16 q16_min_raw def
R1513:1522 Stdlib.ZArith.Zorder <> Zlt_not_le thm
def 1579:1582 Q16_16 zero
R1586:1586 Corelib.Numbers.BinNums <> Z ind
def 1607:1609 Q16_16 one
R1613:1613 Corelib.Numbers.BinNums <> Z ind
def 1638:1644 Q16_16 epsilon
R1648:1648 Corelib.Numbers.BinNums <> Z ind
def 1669:1672 Q16_16 half
R1676:1676 Corelib.Numbers.BinNums <> Z ind
def 1701:1704 Q16_16 pct1
R1710:1710 Corelib.Numbers.BinNums <> Z ind
def 1733:1737 Q16_16 pct70
R1742:1742 Corelib.Numbers.BinNums <> Z ind
def 1767:1771 Q16_16 pct30
R1776:1776 Corelib.Numbers.BinNums <> Z ind
def 1801:1805 Q16_16 one50
R1810:1810 Corelib.Numbers.BinNums <> Z ind
def 1836:1838 Q16_16 add
R1847:1847 Corelib.Numbers.BinNums <> Z ind
binder 1841:1841 <> a:6
binder 1843:1843 <> b:7
R1852:1852 Corelib.Numbers.BinNums <> Z ind
R1857:1865 Q16_16 Q16_16 clamp_raw def
R1869:1871 Stdlib.ZArith.BinInt <> ::Z_scope:x_'+'_x not
R1868:1868 Q16_16 <> a:6 var
R1872:1872 Q16_16 <> b:7 var
def 1889:1891 Q16_16 sub
R1900:1900 Corelib.Numbers.BinNums <> Z ind
binder 1894:1894 <> a:8
binder 1896:1896 <> b:9
R1905:1905 Corelib.Numbers.BinNums <> Z ind
R1910:1918 Q16_16 Q16_16 clamp_raw def
R1922:1924 Stdlib.ZArith.BinInt <> ::Z_scope:x_'-'_x not
R1921:1921 Q16_16 <> a:8 var
R1925:1925 Q16_16 <> b:9 var
def 1942:1944 Q16_16 neg
R1951:1951 Corelib.Numbers.BinNums <> Z ind
binder 1947:1947 <> a:10
R1956:1956 Corelib.Numbers.BinNums <> Z ind
R1961:1969 Q16_16 Q16_16 clamp_raw def
R1972:1972 Stdlib.ZArith.BinInt <> ::Z_scope:'-'_x not
R1973:1973 Q16_16 <> a:10 var
def 1990:1992 Q16_16 mul
R2001:2001 Corelib.Numbers.BinNums <> Z ind
binder 1995:1995 <> a:11
binder 1997:1997 <> b:12
R2006:2006 Corelib.Numbers.BinNums <> Z ind
R2011:2019 Q16_16 Q16_16 clamp_raw def
R2022:2026 Stdlib.ZArith.BinInt Z div def
R2030:2032 Stdlib.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R2029:2029 Q16_16 <> a:11 var
R2033:2033 Q16_16 <> b:12 var
R2036:2044 Q16_16 Q16_16 q16_scale def
def 2061:2063 Q16_16 div
R2072:2072 Corelib.Numbers.BinNums <> Z ind
binder 2066:2066 <> a:13
binder 2068:2068 <> b:14
R2077:2077 Corelib.Numbers.BinNums <> Z ind
R2089:2096 Stdlib.ZArith.BinInt Z eq_dec def
R2098:2098 Q16_16 <> b:14 var
R2117:2125 Q16_16 Q16_16 clamp_raw def
R2128:2132 Stdlib.ZArith.BinInt Z div def
R2136:2138 Stdlib.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R2135:2135 Q16_16 <> a:13 var
R2139:2147 Q16_16 Q16_16 q16_scale def
R2150:2150 Q16_16 <> b:14 var
R2107:2110 Q16_16 Q16_16 zero def
prf 2165:2172 Q16_16 add_comm
R2181:2181 Corelib.Numbers.BinNums <> Z ind
binder 2175:2175 <> a:15
binder 2177:2177 <> b:16
R2193:2195 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R2186:2188 Q16_16 Q16_16 add def
R2190:2190 Q16_16 <> a:15 var
R2192:2192 Q16_16 <> b:16 var
R2196:2198 Q16_16 Q16_16 add def
R2200:2200 Q16_16 <> b:16 var
R2202:2202 Q16_16 <> a:15 var
R2221:2223 Q16_16 Q16_16 add def
R2234:2243 Stdlib.ZArith.BinInt Z add_comm thm
R2234:2243 Stdlib.ZArith.BinInt Z add_comm thm
R2234:2243 Stdlib.ZArith.BinInt Z add_comm thm
prf 2275:2286 Q16_16 add_in_range
R2295:2295 Corelib.Numbers.BinNums <> Z ind
binder 2289:2289 <> a:17
binder 2291:2291 <> b:18
R2304:2311 Q16_16 Q16_16 in_range def
R2313:2313 Q16_16 <> a:17 var
binder 2299:2300 <> ha:19
R2322:2329 Q16_16 Q16_16 in_range def
R2331:2331 Q16_16 <> b:18 var
binder 2317:2318 <> hb:20
R2346:2353 Q16_16 Q16_16 in_range def
R2357:2359 Stdlib.ZArith.BinInt <> ::Z_scope:x_'+'_x not
R2356:2356 Q16_16 <> a:17 var
R2360:2360 Q16_16 <> b:18 var
binder 2339:2342 <> hsum:21
R2373:2375 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R2366:2368 Q16_16 Q16_16 add def
R2370:2370 Q16_16 <> a:17 var
R2372:2372 Q16_16 <> b:18 var
R2377:2379 Stdlib.ZArith.BinInt <> ::Z_scope:x_'+'_x not
R2376:2376 Q16_16 <> a:17 var
R2380:2380 Q16_16 <> b:18 var
R2403:2405 Q16_16 Q16_16 add def
R2416:2431 Q16_16 Q16_16 clamp_idempotent thm
R2416:2431 Q16_16 Q16_16 clamp_idempotent thm
R2416:2431 Q16_16 Q16_16 clamp_idempotent thm
R2416:2431 Q16_16 Q16_16 clamp_idempotent thm
prf 2461:2468 Q16_16 sub_self
R2475:2475 Corelib.Numbers.BinNums <> Z ind
binder 2471:2471 <> a:22
R2484:2491 Q16_16 Q16_16 in_range def
R2493:2493 Q16_16 <> a:22 var
binder 2479:2480 <> ha:23
R2505:2507 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R2498:2500 Q16_16 Q16_16 sub def
R2502:2502 Q16_16 <> a:22 var
R2504:2504 Q16_16 <> a:22 var
R2508:2511 Q16_16 Q16_16 zero def
R2534:2536 Q16_16 Q16_16 sub def
R2539:2542 Q16_16 Q16_16 zero def
R2553:2562 Stdlib.ZArith.BinInt Z sub_diag thm
R2553:2562 Stdlib.ZArith.BinInt Z sub_diag thm
R2553:2562 Stdlib.ZArith.BinInt Z sub_diag thm
R2575:2590 Q16_16 Q16_16 clamp_idempotent thm
R2600:2607 Q16_16 Q16_16 in_range def
R2617:2627 Q16_16 Q16_16 q16_min_raw def
R2630:2640 Q16_16 Q16_16 q16_max_raw def
R2575:2590 Q16_16 Q16_16 clamp_idempotent thm
R2661:2678 Q16_16 <> le_neg2147483648_0 thm
R2688:2702 Q16_16 <> le_0_2147483647 thm
R2661:2678 Q16_16 <> le_neg2147483648_0 thm
R2688:2702 Q16_16 <> le_0_2147483647 thm
prf 2724:2731 Q16_16 mul_comm
R2740:2740 Corelib.Numbers.BinNums <> Z ind
binder 2734:2734 <> a:24
binder 2736:2736 <> b:25
R2752:2754 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R2745:2747 Q16_16 Q16_16 mul def
R2749:2749 Q16_16 <> a:24 var
R2751:2751 Q16_16 <> b:25 var
R2755:2757 Q16_16 Q16_16 mul def
R2759:2759 Q16_16 <> b:25 var
R2761:2761 Q16_16 <> a:24 var
R2780:2782 Q16_16 Q16_16 mul def
R2793:2802 Stdlib.ZArith.BinInt Z mul_comm thm
R2793:2802 Stdlib.ZArith.BinInt Z mul_comm thm
R2793:2802 Stdlib.ZArith.BinInt Z mul_comm thm
prf 2834:2846 Q16_16 in_range_zero
R2850:2857 Q16_16 Q16_16 in_range def
R2878:2885 Q16_16 Q16_16 in_range def
R2888:2898 Q16_16 Q16_16 q16_min_raw def
R2901:2911 Q16_16 Q16_16 q16_max_raw def
R2928:2945 Q16_16 <> le_neg2147483648_0 thm
R2955:2969 Q16_16 <> le_0_2147483647 thm
R2928:2945 Q16_16 <> le_neg2147483648_0 thm
R2955:2969 Q16_16 <> le_0_2147483647 thm
prf 2989:3000 Q16_16 in_range_one
R3004:3011 Q16_16 Q16_16 in_range def
R3032:3039 Q16_16 Q16_16 in_range def
R3042:3052 Q16_16 Q16_16 q16_min_raw def
R3055:3065 Q16_16 Q16_16 q16_max_raw def
R3082:3099 Q16_16 <> le_neg2147483648_0 thm
R3109:3123 Q16_16 <> le_0_2147483647 thm
R3082:3099 Q16_16 <> le_neg2147483648_0 thm
R3109:3123 Q16_16 <> le_0_2147483647 thm
R3137:3142 Q16_16 Q16_16 <> mod
Reference in a new issue View git blame Copy permalink