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/avm.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

446 lines
16 KiB
Text
Raw Permalink Blame History

DIGEST 3a6af8bd9f0880063607a37ee751b817
Favm
R54:59 Stdlib.ZArith.ZArith <> <> lib
R61:64 Stdlib.Lists.List <> <> lib
mod 101:103 <> AVM
def 119:127 AVM q16_scale
R131:131 Corelib.Numbers.BinNums <> Z ind
ind 156:160 AVM AvmTy
constr 171:175 AVM Q0_16
constr 179:184 AVM Q16_16
constr 188:191 AVM Bool
scheme 156:160 AVM AvmTy_rect
scheme 156:160 AVM AvmTy_ind
scheme 156:160 AVM AvmTy_rec
scheme 156:160 AVM AvmTy_sind
ind 207:212 AVM AvmVal
constr 223:225 AVM Vq0
constr 237:240 AVM Vq16
constr 252:256 AVM Vbool
R232:232 Corelib.Numbers.BinNums <> Z ind
binder 228:228 <> x:5
R247:247 Corelib.Numbers.BinNums <> Z ind
binder 243:243 <> x:6
R263:266 Corelib.Init.Datatypes <> bool ind
binder 259:259 <> b:7
scheme 207:212 AVM AvmVal_rect
scheme 207:212 AVM AvmVal_ind
scheme 207:212 AVM AvmVal_rec
scheme 207:212 AVM AvmVal_sind
ind 283:286 AVM Prim
constr 301:306 AVM AddQ16
constr 310:315 AVM SubQ16
constr 319:324 AVM MulQ16
constr 328:333 AVM DivQ16
constr 337:341 AVM LtQ16
constr 345:349 AVM EqQ16
constr 353:355 AVM And
constr 359:360 AVM Or
constr 364:366 AVM Not
scheme 283:286 AVM Prim_rect
scheme 283:286 AVM Prim_ind
scheme 283:286 AVM Prim_rec
scheme 283:286 AVM Prim_sind
ind 382:386 AVM Instr
constr 401:408 AVM Push_q16
constr 420:428 AVM Push_bool
constr 443:445 AVM Pop
constr 449:451 AVM Dup
constr 455:458 AVM Swap
constr 464:467 AVM Load
constr 481:485 AVM Store
constr 499:502 AVM Jump
constr 516:522 AVM Jump_if
constr 538:544 AVM Prim_op
constr 559:562 AVM Halt
R415:415 Corelib.Numbers.BinNums <> Z ind
binder 411:411 <> x:12
R435:438 Corelib.Init.Datatypes <> bool ind
binder 431:431 <> b:13
R474:476 Corelib.Init.Datatypes <> nat ind
binder 470:470 <> i:14
R492:494 Corelib.Init.Datatypes <> nat ind
binder 488:488 <> i:15
R509:511 Corelib.Init.Datatypes <> nat ind
binder 505:505 <> t:16
R529:531 Corelib.Init.Datatypes <> nat ind
binder 525:525 <> t:17
R551:554 avm AVM Prim ind
binder 547:547 <> p:18
scheme 382:386 AVM Instr_rect
scheme 382:386 AVM Instr_ind
scheme 382:386 AVM Instr_rec
scheme 382:386 AVM Instr_sind
rec 575:579 AVM State
proj 604:605 AVM pc
proj 614:618 AVM stack
proj 635:640 AVM locals
proj 666:671 AVM halted
R609:611 Corelib.Init.Datatypes <> nat ind
R622:625 Corelib.Init.Datatypes <> list ind
R627:632 avm AVM AvmVal ind
R644:647 Corelib.Init.Datatypes <> list ind
R650:655 Corelib.Init.Datatypes <> option ind
R657:662 avm AVM AvmVal ind
R675:678 Corelib.Init.Datatypes <> bool ind
def 699:709 AVM empty_state
R713:717 avm AVM State rec
R722:728 avm AVM mkState constr
R732:734 Corelib.Init.Datatypes <> nil constr
R736:738 Corelib.Init.Datatypes <> nil constr
R740:744 Corelib.Init.Datatypes <> false constr
def 761:769 AVM get_local
R776:780 avm AVM State rec
binder 772:772 <> s:24
R788:790 Corelib.Init.Datatypes <> nat ind
binder 784:784 <> i:25
R795:800 Corelib.Init.Datatypes <> option ind
R802:807 avm AVM AvmVal ind
R822:835 Stdlib.Lists.List <> nth_error def
R848:848 avm <> i:25 var
R840:845 avm AVM locals proj
R837:837 avm <> s:24 var
R861:864 Corelib.Init.Datatypes <> Some constr
R867:870 Corelib.Init.Datatypes <> Some constr
R878:881 Corelib.Init.Datatypes <> Some constr
R892:895 Corelib.Init.Datatypes <> None constr
def 920:926 AVM q16_mul
R935:935 Corelib.Numbers.BinNums <> Z ind
binder 929:929 <> a:26
binder 931:931 <> b:27
R940:940 Corelib.Numbers.BinNums <> Z ind
R945:949 Stdlib.ZArith.BinInt Z div def
R953:955 Stdlib.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R952:952 avm <> a:26 var
R956:956 avm <> b:27 var
R959:967 avm AVM q16_scale def
def 983:989 AVM q16_div
R998:998 Corelib.Numbers.BinNums <> Z ind
binder 992:992 <> a:28
binder 994:994 <> b:29
R1003:1003 Corelib.Numbers.BinNums <> Z ind
R1015:1019 Stdlib.ZArith.BinInt Z eqb def
R1021:1021 avm <> b:29 var
R1045:1049 Stdlib.ZArith.BinInt Z div def
R1053:1055 Stdlib.ZArith.BinInt <> ::Z_scope:x_'*'_x not
R1052:1052 avm <> a:28 var
R1056:1064 avm AVM q16_scale def
R1067:1067 avm <> b:29 var
R1030:1038 avm AVM q16_scale def
def 1084:1092 AVM exec_prim
R1099:1102 avm AVM Prim ind
binder 1095:1095 <> p:30
R1112:1117 Corelib.Init.Datatypes <> option ind
R1119:1124 avm AVM AvmVal ind
binder 1106:1106 <> a:31
binder 1108:1108 <> b:32
R1129:1134 Corelib.Init.Datatypes <> option ind
R1136:1141 avm AVM AvmVal ind
R1162:1162 avm <> b:32 var
R1159:1159 avm <> a:31 var
R1156:1156 avm <> p:30 var
R1175:1180 avm AVM AddQ16 constr
R1183:1186 Corelib.Init.Datatypes <> Some constr
R1189:1192 avm AVM Vq16 constr
R1198:1201 Corelib.Init.Datatypes <> Some constr
R1204:1207 avm AVM Vq16 constr
R1215:1218 Corelib.Init.Datatypes <> Some constr
R1221:1224 avm AVM Vq16 constr
R1228:1230 Stdlib.ZArith.BinInt <> ::Z_scope:x_'+'_x not
R1241:1246 avm AVM SubQ16 constr
R1249:1252 Corelib.Init.Datatypes <> Some constr
R1255:1258 avm AVM Vq16 constr
R1264:1267 Corelib.Init.Datatypes <> Some constr
R1270:1273 avm AVM Vq16 constr
R1281:1284 Corelib.Init.Datatypes <> Some constr
R1287:1290 avm AVM Vq16 constr
R1294:1296 Stdlib.ZArith.BinInt <> ::Z_scope:x_'-'_x not
R1307:1312 avm AVM MulQ16 constr
R1315:1318 Corelib.Init.Datatypes <> Some constr
R1321:1324 avm AVM Vq16 constr
R1330:1333 Corelib.Init.Datatypes <> Some constr
R1336:1339 avm AVM Vq16 constr
R1347:1350 Corelib.Init.Datatypes <> Some constr
R1353:1356 avm AVM Vq16 constr
R1359:1365 avm AVM q16_mul def
R1379:1384 avm AVM DivQ16 constr
R1387:1390 Corelib.Init.Datatypes <> Some constr
R1393:1396 avm AVM Vq16 constr
R1402:1405 Corelib.Init.Datatypes <> Some constr
R1408:1411 avm AVM Vq16 constr
R1419:1422 Corelib.Init.Datatypes <> Some constr
R1425:1428 avm AVM Vq16 constr
R1431:1437 avm AVM q16_div def
R1451:1455 avm AVM LtQ16 constr
R1458:1461 Corelib.Init.Datatypes <> Some constr
R1464:1467 avm AVM Vq16 constr
R1473:1476 Corelib.Init.Datatypes <> Some constr
R1479:1482 avm AVM Vq16 constr
R1490:1493 Corelib.Init.Datatypes <> Some constr
R1496:1500 avm AVM Vbool constr
R1503:1507 Stdlib.ZArith.BinInt Z ltb def
R1521:1525 avm AVM EqQ16 constr
R1528:1531 Corelib.Init.Datatypes <> Some constr
R1534:1537 avm AVM Vq16 constr
R1543:1546 Corelib.Init.Datatypes <> Some constr
R1549:1552 avm AVM Vq16 constr
R1560:1563 Corelib.Init.Datatypes <> Some constr
R1566:1570 avm AVM Vbool constr
R1573:1577 Stdlib.ZArith.BinInt Z eqb def
R1591:1593 avm AVM And constr
R1596:1599 Corelib.Init.Datatypes <> Some constr
R1602:1606 avm AVM Vbool constr
R1612:1615 Corelib.Init.Datatypes <> Some constr
R1618:1622 avm AVM Vbool constr
R1630:1633 Corelib.Init.Datatypes <> Some constr
R1636:1640 avm AVM Vbool constr
R1644:1647 Corelib.Init.Datatypes <> ::bool_scope:x_'&&'_x not
R1658:1659 avm AVM Or constr
R1662:1665 Corelib.Init.Datatypes <> Some constr
R1668:1672 avm AVM Vbool constr
R1678:1681 Corelib.Init.Datatypes <> Some constr
R1684:1688 avm AVM Vbool constr
R1696:1699 Corelib.Init.Datatypes <> Some constr
R1702:1706 avm AVM Vbool constr
R1710:1713 Corelib.Init.Datatypes <> ::bool_scope:x_'||'_x not
R1724:1726 avm AVM Not constr
R1729:1732 Corelib.Init.Datatypes <> Some constr
R1735:1739 avm AVM Vbool constr
R1745:1748 Corelib.Init.Datatypes <> None constr
R1753:1756 Corelib.Init.Datatypes <> Some constr
R1759:1763 avm AVM Vbool constr
R1766:1769 Corelib.Init.Datatypes <> negb def
R1792:1795 Corelib.Init.Datatypes <> None constr
def 1820:1823 AVM step
R1830:1834 avm AVM State rec
binder 1826:1826 <> s:36
R1845:1848 Corelib.Init.Datatypes <> list ind
R1850:1854 avm AVM Instr ind
binder 1838:1841 <> prog:37
R1859:1864 Corelib.Init.Datatypes <> option ind
R1866:1870 avm AVM State rec
R1885:1890 avm AVM halted proj
R1882:1882 avm <> s:36 var
R1918:1931 Stdlib.Lists.List <> nth_error def
R1941:1942 avm AVM pc proj
R1938:1938 avm <> s:36 var
R1933:1936 avm <> prog:37 var
R1956:1959 Corelib.Init.Datatypes <> None constr
R1964:1967 Corelib.Init.Datatypes <> Some constr
R1970:1976 avm AVM mkState constr
R1981:1982 avm AVM pc proj
R1978:1978 avm <> s:36 var
R1988:1992 avm AVM stack proj
R1985:1985 avm <> s:36 var
R1998:2003 avm AVM locals proj
R1995:1995 avm <> s:36 var
R2006:2009 Corelib.Init.Datatypes <> true constr
R2018:2021 Corelib.Init.Datatypes <> Some constr
R2052:2052 Corelib.Init.Datatypes <> S constr
R2057:2058 avm AVM pc proj
R2054:2054 avm <> s:36 var
binder 2042:2047 <> new_pc:38
binder 2079:2079 <> v:39
R2084:2087 Corelib.Init.Datatypes <> Some constr
R2090:2096 avm AVM mkState constr
R2098:2103 avm <> new_pc:38 var
R2107:2110 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R2106:2106 avm <> v:39 var
R2114:2118 avm AVM stack proj
R2111:2111 avm <> s:36 var
R2125:2130 avm AVM locals proj
R2122:2122 avm <> s:36 var
R2133:2137 Corelib.Init.Datatypes <> false constr
binder 2074:2077 <> push:40
R2174:2181 avm AVM Push_q16 constr
R2188:2191 avm <> push:40 var
R2194:2197 avm AVM Vq16 constr
R2210:2218 avm AVM Push_bool constr
R2225:2228 avm <> push:40 var
R2231:2235 avm AVM Vbool constr
R2248:2250 avm AVM Pop constr
R2272:2276 avm AVM stack proj
R2269:2269 avm <> s:36 var
R2295:2298 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R2307:2310 Corelib.Init.Datatypes <> Some constr
R2313:2319 avm AVM mkState constr
R2321:2326 avm <> new_pc:38 var
R2336:2341 avm AVM locals proj
R2333:2333 avm <> s:36 var
R2344:2348 Corelib.Init.Datatypes <> false constr
R2361:2363 Corelib.Init.Datatypes <> nil constr
R2368:2371 Corelib.Init.Datatypes <> None constr
R2393:2395 avm AVM Dup constr
R2417:2421 avm AVM stack proj
R2414:2414 avm <> s:36 var
R2440:2443 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R2449:2452 avm <> push:40 var
R2458:2460 Corelib.Init.Datatypes <> nil constr
R2465:2468 Corelib.Init.Datatypes <> None constr
R2490:2493 avm AVM Swap constr
R2515:2519 avm AVM stack proj
R2512:2512 avm <> s:36 var
R2538:2541 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R2543:2546 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R2555:2558 Corelib.Init.Datatypes <> Some constr
R2561:2567 avm AVM mkState constr
R2569:2574 avm <> new_pc:38 var
R2578:2581 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R2583:2586 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R2596:2601 avm AVM locals proj
R2593:2593 avm <> s:36 var
R2604:2608 Corelib.Init.Datatypes <> false constr
R2626:2629 Corelib.Init.Datatypes <> None constr
R2651:2654 avm AVM Load constr
R2675:2683 avm AVM get_local def
R2685:2685 avm <> s:36 var
R2704:2707 Corelib.Init.Datatypes <> Some constr
R2714:2717 avm <> push:40 var
R2723:2726 Corelib.Init.Datatypes <> None constr
R2731:2734 Corelib.Init.Datatypes <> None constr
R2756:2760 avm AVM Store constr
R2784:2788 avm AVM stack proj
R2781:2781 avm <> s:36 var
R2807:2810 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R2829:2832 Corelib.Init.Datatypes <> Some constr
R2835:2841 avm AVM mkState constr
R2843:2848 avm <> new_pc:38 var
R2892:2895 Corelib.Init.Datatypes <> ::list_scope:x_'++'_x not
R2868:2878 Stdlib.Lists.List <> firstn abbrev
R2885:2890 avm AVM locals proj
R2882:2882 avm <> s:36 var
R2902:2905 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R2896:2899 Corelib.Init.Datatypes <> Some constr
R2906:2915 Stdlib.Lists.List <> skipn abbrev
R2926:2931 avm AVM locals proj
R2923:2923 avm <> s:36 var
R2918:2918 Corelib.Init.Datatypes <> S constr
R2935:2939 Corelib.Init.Datatypes <> false constr
R2952:2954 Corelib.Init.Datatypes <> nil constr
R2959:2962 Corelib.Init.Datatypes <> None constr
R2984:2987 avm AVM Jump constr
R2994:2997 Corelib.Init.Datatypes <> Some constr
R3000:3006 avm AVM mkState constr
R3013:3017 avm AVM stack proj
R3010:3010 avm <> s:36 var
R3023:3028 avm AVM locals proj
R3020:3020 avm <> s:36 var
R3031:3035 Corelib.Init.Datatypes <> false constr
R3046:3052 avm AVM Jump_if constr
R3076:3080 avm AVM stack proj
R3073:3073 avm <> s:36 var
R3108:3111 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R3098:3102 avm AVM Vbool constr
R3104:3107 Corelib.Init.Datatypes <> true constr
R3120:3123 Corelib.Init.Datatypes <> Some constr
R3126:3132 avm AVM mkState constr
R3144:3149 avm AVM locals proj
R3141:3141 avm <> s:36 var
R3152:3156 Corelib.Init.Datatypes <> false constr
R3180:3183 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R3169:3173 avm AVM Vbool constr
R3175:3179 Corelib.Init.Datatypes <> false constr
R3192:3195 Corelib.Init.Datatypes <> Some constr
R3198:3204 avm AVM mkState constr
R3206:3211 avm <> new_pc:38 var
R3221:3226 avm AVM locals proj
R3218:3218 avm <> s:36 var
R3229:3233 Corelib.Init.Datatypes <> false constr
R3247:3250 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R3256:3259 Corelib.Init.Datatypes <> None constr
R3263:3265 Corelib.Init.Datatypes <> nil constr
R3270:3273 Corelib.Init.Datatypes <> None constr
R3295:3301 avm AVM Prim_op constr
R3340:3342 avm AVM Not constr
R3366:3370 avm AVM stack proj
R3363:3363 avm <> s:36 var
R3391:3394 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R3421:3429 avm AVM exec_prim def
R3434:3437 Corelib.Init.Datatypes <> Some constr
R3442:3445 Corelib.Init.Datatypes <> None constr
R3466:3469 Corelib.Init.Datatypes <> Some constr
R3476:3479 Corelib.Init.Datatypes <> Some constr
R3482:3488 avm AVM mkState constr
R3490:3495 avm <> new_pc:38 var
R3499:3502 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R3512:3517 avm AVM locals proj
R3509:3509 avm <> s:36 var
R3520:3524 Corelib.Init.Datatypes <> false constr
R3541:3544 Corelib.Init.Datatypes <> None constr
R3549:3552 Corelib.Init.Datatypes <> None constr
R3582:3584 Corelib.Init.Datatypes <> nil constr
R3589:3592 Corelib.Init.Datatypes <> None constr
R3642:3646 avm AVM stack proj
R3639:3639 avm <> s:36 var
R3667:3670 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R3672:3675 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R3702:3710 avm AVM exec_prim def
R3715:3718 Corelib.Init.Datatypes <> Some constr
R3724:3727 Corelib.Init.Datatypes <> Some constr
R3751:3754 Corelib.Init.Datatypes <> Some constr
R3761:3764 Corelib.Init.Datatypes <> Some constr
R3767:3773 avm AVM mkState constr
R3775:3780 avm <> new_pc:38 var
R3784:3787 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not
R3797:3802 avm AVM locals proj
R3794:3794 avm <> s:36 var
R3805:3809 Corelib.Init.Datatypes <> false constr
R3826:3829 Corelib.Init.Datatypes <> None constr
R3834:3837 Corelib.Init.Datatypes <> None constr
R3872:3875 Corelib.Init.Datatypes <> None constr
R3912:3915 avm AVM Halt constr
R3920:3923 Corelib.Init.Datatypes <> Some constr
R3926:3932 avm AVM mkState constr
R3937:3938 avm AVM pc proj
R3934:3934 avm <> s:36 var
R3944:3948 avm AVM stack proj
R3941:3941 avm <> s:36 var
R3954:3959 avm AVM locals proj
R3951:3951 avm <> s:36 var
R3962:3965 Corelib.Init.Datatypes <> true constr
R1898:1901 Corelib.Init.Datatypes <> None constr
def 3999:4001 AVM run
R4008:4012 avm AVM State rec
binder 4004:4004 <> s:43
R4023:4026 Corelib.Init.Datatypes <> list ind
R4028:4032 avm AVM Instr ind
binder 4016:4019 <> prog:44
R4043:4045 Corelib.Init.Datatypes <> nat ind
binder 4036:4039 <> fuel:45
R4064:4069 Corelib.Init.Datatypes <> option ind
R4071:4075 avm AVM State rec
R4090:4093 avm <> fuel:45 var
R4106:4106 Corelib.Init.Datatypes <> O constr
R4111:4114 Corelib.Init.Datatypes <> Some constr
R4116:4116 avm <> s:43 var
R4124:4124 Corelib.Init.Datatypes <> S constr
R4143:4148 avm AVM halted proj
R4140:4140 avm <> s:43 var
R4180:4183 avm AVM step def
R4185:4185 avm <> s:43 var
R4187:4190 avm <> prog:44 var
R4205:4208 Corelib.Init.Datatypes <> None constr
R4213:4216 Corelib.Init.Datatypes <> None constr
R4220:4223 Corelib.Init.Datatypes <> Some constr
R4231:4233 avm <> run:46 def
R4238:4241 avm <> prog:44 var
R4156:4159 Corelib.Init.Datatypes <> Some constr
R4161:4161 avm <> s:43 var
prf 4273:4283 AVM step_halted
R4290:4294 avm AVM State rec
binder 4286:4286 <> s:48
R4305:4308 Corelib.Init.Datatypes <> list ind
R4310:4314 avm AVM Instr ind
binder 4298:4301 <> prog:49
R4332:4334 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R4325:4330 avm AVM halted proj
R4322:4322 avm <> s:48 var
R4335:4338 Corelib.Init.Datatypes <> true constr
binder 4318:4318 <> h:50
R4358:4360 Corelib.Init.Logic <> ::type_scope:x_'='_x not
R4347:4350 avm AVM step def
R4352:4352 avm <> s:48 var
R4354:4357 avm <> prog:49 var
R4361:4364 Corelib.Init.Datatypes <> None constr
R4383:4386 avm AVM step def
R4423:4425 avm AVM <> mod
Reference in a new issue View git blame Copy permalink