Merged
Conversation
gabriel-barrett
approved these changes
Nov 21, 2025
johnchandlerburnham
pushed a commit
that referenced
this pull request
Dec 12, 2025
This patch implements (and changes) enough of the code base as a PoC of being able to provably bootstrap the precise Ixon whose hash is stated as an argument of the claim (as input of the Aiur entrypoint call). This is done by reading the bytes from the `IOBuffer`, deserializing it and then serializing and hashing the respective bytes. Deserialization followed by serialization was the chosen solution because serialization is, in principle, cheaper. Thus the deserialization can be tagged as `#[unconstrained]` for extra speed. Furthermore, the unconstrained tag is now more rigorous: an unconstrained function can no longer call a constrained function. As an extra, the IxVM code has been split into multiple smaller Aiur toplevels to enable parallel elaboration by Lean. --------- Co-authored-by: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
johnchandlerburnham
added a commit
that referenced
this pull request
Dec 13, 2025
* refactor module organization, env types, and add richer scc result * tmp rustfmt * rust, const sorting and expr compilation * compile_const * wip: compiler structure, but erroring * compiling Env in 11.32 seconds * clippy and warnings * manual stack management for compile_expr to avoid overflow * xclippy warnings * compilation in 6.65s, total pipeline in 16.8s * remove cons_list * ci: Add comparative benchmark report (#265) * feat: Add Json serde for Benchmark API * (WIP) Add comparison report and PR comment workflow * Add one-shot benches and markdown report * Export benchmark API in ix library * Add env var overrides for config settings * Finish report pretty-printer * Fix `bench.yml` * Scope permissions with app token * Fix security alert * Fixup * Start `Ixon` serde in Aiur (#268) This patch implements (and changes) enough of the code base as a PoC of being able to provably bootstrap the precise Ixon whose hash is stated as an argument of the claim (as input of the Aiur entrypoint call). This is done by reading the bytes from the `IOBuffer`, deserializing it and then serializing and hashing the respective bytes. Deserialization followed by serialization was the chosen solution because serialization is, in principle, cheaper. Thus the deserialization can be tagged as `#[unconstrained]` for extra speed. Furthermore, the unconstrained tag is now more rigorous: an unconstrained function can no longer call a constrained function. As an extra, the IxVM code has been split into multiple smaller Aiur toplevels to enable parallel elaboration by Lean. --------- Co-authored-by: Gabriel Barreto <gabriel.aquino.barreto@gmail.com> * chore: Clean up Benchmark API (#267) * chore: Test benchmark PR * Refactor blake3 bench to use Criterion * chore: Refactoring * More fixes * Lifted unconstrained restriction (#273) * lifted unconstrained restriction * filtered queries of multiplicity 0 * constrained inside unconstrained test * Progress on serialize and deserialize (#276) * Ixon.UVar * deserialize Ixon.EVar and Ixon.Blob * some fixes * small fix * progress on serialize * wip * fixes and deserialize for more cases * more fixes * removed stream input from `serialize` * uvar, evar * `u64_get_trimmed_le` rewritten --------- Co-authored-by: Arthur Paulino <arthurleonardo.ap@gmail.com> * IxVM file split (#278) * rust compiler (#263) * refactor module organization, env types, and add richer scc result * tmp rustfmt * rust, const sorting and expr compilation * compile_const * wip: compiler structure, but erroring * compiling Env in 11.32 seconds * clippy and warnings * manual stack management for compile_expr to avoid overflow * xclippy warnings * compilation in 6.65s, total pipeline in 16.8s * remove cons_list * review comments * Pointer pattern (#280) * Pointer pattern * elab new Pattern.pointer constructor * pointer match test --------- Co-authored-by: Arthur Paulino <arthurleonardo.ap@gmail.com> * decompilation pipeline working * fix failing condense.rs tests * parallelize decoding * xclippy warnings --------- Co-authored-by: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com> Co-authored-by: Arthur Paulino <arthurleonardo.ap@gmail.com> Co-authored-by: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This patch implements (and changes) enough of the code base as a PoC of being able to provably bootstrap the precise Ixon whose hash is stated as an argument of the claim (as input of the Aiur entrypoint call).
This is done by reading the bytes from the
IOBuffer, deserializing it and then serializing and hashing the respective bytes. Deserialization followed by serialization was the chosen solution because serialization is, in principle, cheaper. Thus the deserialization can be tagged as#[unconstrained]for extra speed.Furthermore, the unconstrained tag is now more rigorous: an unconstrained function can no longer call a constrained function.
As an extra, the IxVM code has been split into multiple smaller Aiur toplevels to enable parallel elaboration by Lean.