~james/remy

☆ 1

History of src/Frontend.thy on main

7cb596d931 feat(x86): prove emitted instruction execution and return-frame consumptionVerified ~james
james · 12 days ago
b58768f9b4 feat(branches): compile conditionals to validated forward jumpsVerified ~james
james · 12 days ago
edf26390ae feat(allocator): retain intermediates in registers and spill nested valuesVerified ~james
james · 12 days ago
31d281ada8 feat(checker): validate native stack and register effectsVerified ~james
james · 23 days ago
5ccdadce3e feat(cli): disassemble emitted native instruction blocksVerified ~james
james · 26 days ago
cd894bac28 perf(native): eliminate adjacent stack transfers with verified movesVerified ~james
james · 1 months ago
75a5217580 feat(frontend): parameterise checked compiler resource limitsVerified ~james
james · 1 months ago
33c6eac26d fix(frontend): distinguish syntax failures from resource limitsVerified ~james
james · 1 months ago
9a908c16a9 feat(frontend): report token offsets for parse failuresVerified ~james
james · 1 months ago
a0e486f13b feat(frontend): support semicolon line commentsVerified ~james
james · 1 months ago
76eb8c0c10 feat(frontend): accept digits after identifier prefixesVerified ~james
james · 1 months ago
21d77cf288 feat(frontend): parse bounded hexadecimal word literalsVerified ~james
james · 1 months ago
7d99400a08 feat(frontend): prove parsed expressions preserve lexical scopeVerified ~james
james · 1 months ago
72b2edbe20 feat(compiler): prove exact peak stack demandVerified ~james
james · 2 months ago
3ac5bae085 feat(compiler): add verified pixel compiler and templeos runnerVerified ~james
james · 2 months ago