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/AVMIsa/q16_16.glob
allaun f6cbddcbf2 feat(tests): Python AVM port rewrite + test harness, Go test harness 
Python port rewritten to match spec:
- Added Q0_16, PUSH_Q0, PUSH_BOOL as separate opcodes
- Added V6 comparison (lt_q16_v6)
- Added floor division (Lean Int.ediv)
- Added stack depth limit (AVM_MAX_STACK = 1024)
- Added type checking in exec_prim
- All 10 tests passing

Go AVM port: added test_avm_test.go with 8 test cases

Milestone: Python → ✅, Go → 🔄
2026-06-30 17:56:09 -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