james/span
Watch
1
0
Fork
You've already forked span
 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
Verified branch relaxing assembler in Isabelle/HOL with provably minimal bytecode layouts
6 commits 1 branch 0 tags 1.4 MiB
  • Isabelle 71.2%
  • Python 19.3%
  • Standard ML 8%
  • Makefile 1.1%
  • Shell 0.4%
Find a file
Exact
Repository files (latest commit first)
Filename Latest commit message Latest commit date
james 868a68649c
 Merge pull request #1 from ecstasygg/improvements 
prove decoder canonicality, verify tail recursive frontend workers and make binary output atomic
2026-10-31 17:43:59 +00:00
cli fix(cli): publish binary output atomically and preserve raw input 2026-10-31 13:00:00 +00:00
examples initial commit 2026-10-31 06:50:40 +00:00
media initial commit 2026-10-31 06:50:40 +00:00
src perf(cli): compile binary output and assembly report once 2026-10-31 11:55:00 +00:00
tests fix(cli): publish binary output atomically and preserve raw input 2026-10-31 13:00:00 +00:00
.gitignore initial commit 2026-10-31 06:50:40 +00:00
Encoding.thy initial commit 2026-10-31 06:50:40 +00:00
Machine.thy initial commit 2026-10-31 06:50:40 +00:00
Makefile initial commit 2026-10-31 06:50:40 +00:00
README.md Merge pull request #1 from ecstasygg/improvements 2026-10-31 17:43:59 +00:00
Relax.thy initial commit 2026-10-31 06:50:40 +00:00
ROOT initial commit 2026-10-31 06:50:40 +00:00
span initial commit 2026-10-31 06:50:40 +00:00

README.md

Span implements a branch relaxing assembler in Isabelle/HOL, with proofs of termination, minimum layout size and execution correspondence for a bytecode machine with signed 8-bit and 16-bit relative branches

Correctness

An overflowing short branch must be wide in every valid assignment. Relaxation computes the least widening set terminating on the number of remaining short branches. A final range check decides whether any valid layout exists

Encoding proves byte bounds and decoder inversion and Execution correspondence relates source execution S and bytecode execution B through relocation R for every fuel bound (including suspended states)

Minimality assumes fixed instruction order and excludes alignment directives while the machine uses a natural valued accumulator and biased little endian branch payloads. The execution theorem starts from resolved instructions and excludes the SML compiler, runtime and OS I/O