Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
88 commits
Select commit Hold shift + click to select a range
6e672dd
WIP: ix hash command
johnchandlerburnham Mar 15, 2025
8271d54
make Proof serialize as an Ixon Const
johnchandlerburnham Mar 17, 2025
d34dc40
broken: connect canonicalizer to Ix.Meta
johnchandlerburnham Mar 17, 2025
4b3cfbe
fix: Nix devShell & light refactor (#55)
samuelburnham Mar 18, 2025
216bee1
Merge branch 'main' of github.com:argumentcomputer/ix into jcb/ix-cli
johnchandlerburnham Mar 25, 2025
5938727
ix store cli command
johnchandlerburnham Mar 25, 2025
52431bf
WIP: store command and new IxM structure
johnchandlerburnham Mar 28, 2025
e6a212c
megacommit implementing Ix commitment API
johnchandlerburnham Apr 14, 2025
63faf25
Merge branch 'main' of github.com:argumentcomputer/ix into jcb/ix-cli
johnchandlerburnham Apr 14, 2025
35d1311
fixup merge
johnchandlerburnham Apr 14, 2025
685f565
fixup merge 2
johnchandlerburnham Apr 14, 2025
93309c8
ix prove check command
johnchandlerburnham Apr 14, 2025
c9b3565
Merge branch 'main' of github.com:argumentcomputer/ix into jcb/ix-cli
johnchandlerburnham Apr 20, 2025
b90fd9b
implement ix prove CLI and simplify metaprogramming
johnchandlerburnham Apr 20, 2025
221f352
provecmd examples
johnchandlerburnham Apr 20, 2025
5aa0fc4
cleanup repo
johnchandlerburnham Apr 21, 2025
ed79280
simplify ZKVoting example app
johnchandlerburnham Apr 21, 2025
f8d7176
Merge branch 'main' of github.com:argumentcomputer/ix into jcb/ix-cli
johnchandlerburnham Apr 22, 2025
5e806e7
remove IO from the compiler core
johnchandlerburnham Apr 23, 2025
37c5779
add level params to Ix IR to support decompilation
johnchandlerburnham Apr 25, 2025
802650e
refactor Ix IR to support decompilation
johnchandlerburnham May 2, 2025
3de279e
implement decompilation mutdefs, compilation of mixed mutdefs, and te…
johnchandlerburnham May 3, 2025
e0973fe
wip
johnchandlerburnham May 16, 2025
6bb0129
decompilation roundtrip of Ix get_env working
johnchandlerburnham May 16, 2025
7e94095
WIP: new mutual definition changes
johnchandlerburnham May 23, 2025
8322be7
roundtrip compilation decompilation tests now passing
johnchandlerburnham May 23, 2025
347268b
add count to roundtrip
johnchandlerburnham May 23, 2025
efd6dbe
Merge branch 'main' of github.com:argumentcomputer/ix into jcb/ix-tests
johnchandlerburnham May 23, 2025
32f85d3
fixup merge
johnchandlerburnham May 23, 2025
7ebf0ee
fixup merge
johnchandlerburnham May 23, 2025
2c5d0db
fixup merge test
johnchandlerburnham May 23, 2025
a341cd3
Merge branch 'main' of github.com:argumentcomputer/ix into jcb/ix-tests
johnchandlerburnham May 24, 2025
87fc22d
remove style guide
johnchandlerburnham May 24, 2025
c3141e4
Merge branch 'main' of github.com:argumentcomputer/ix into jcb/ix-tests
johnchandlerburnham Jul 17, 2025
f4129dc
merge
johnchandlerburnham Jul 17, 2025
75405a0
Aiur2 prove/verify (#183)
arthurpaulino Jul 24, 2025
5c1a9c4
Remove binius (#185)
arthurpaulino Jul 24, 2025
104d546
Bench (#186)
arthurpaulino Jul 25, 2025
fc3eaa8
initial ixon serialization framework
johnchandlerburnham Aug 6, 2025
3b57c87
rustfmt
johnchandlerburnham Aug 6, 2025
a13133e
ixon univ/expr roundtrip
johnchandlerburnham Aug 11, 2025
7cc124f
Merge branch 'main' of github.com:argumentcomputer/ix into jcb/ix-vm
johnchandlerburnham Aug 11, 2025
bcd28d3
new ixon format passing proptest roundtrip
johnchandlerburnham Aug 15, 2025
a5ad9ea
remove old files
johnchandlerburnham Aug 15, 2025
6da9f7a
implement Ixon v2 in Lean
johnchandlerburnham Aug 22, 2025
da561e5
Ixon reconstruction in Rust from Lean pointers
arthurpaulino Aug 27, 2025
42f882c
use standard formatting
arthurpaulino Sep 3, 2025
e904b6d
Merge branch 'main' into jcb/ix-vm
arthurpaulino Sep 3, 2025
c720d38
fix Ixon Lean serialization
johnchandlerburnham Sep 3, 2025
4129fb8
WIP: Lean -> Rust round-trip serialization test
johnchandlerburnham Sep 3, 2025
160489f
fix FFI
arthurpaulino Sep 4, 2025
6ae63ff
WIP: synchronized Lean and Rust implementations, failing on metadata …
johnchandlerburnham Sep 11, 2025
5fa0c6f
fix FFI for ReducibilityHints::Regular
arthurpaulino Sep 11, 2025
b900a8f
WIP: improved performance of mutual def sorting, but compilation stil…
johnchandlerburnham Sep 19, 2025
ee44897
very WIP compiler rewrite
johnchandlerburnham Oct 3, 2025
3e78ae1
compiler refactored
johnchandlerburnham Oct 6, 2025
63b5e0c
proptest for `Ixon` serde
arthurpaulino Oct 6, 2025
1b3b6e9
try reverting caches to RBMap
johnchandlerburnham Oct 7, 2025
6df502d
bitblast now compiling
johnchandlerburnham Oct 7, 2025
2e54234
full compilation of Lean->Ixon, but slow
johnchandlerburnham Oct 9, 2025
b9ed33b
Tarjan's SCC algorithm for mutuals, so we can compile Recursors
johnchandlerburnham Oct 13, 2025
bd52874
simplify mutual compilation, remove IR
johnchandlerburnham Oct 15, 2025
c38a0e7
compile unsafe Lean?
johnchandlerburnham Oct 16, 2025
a999ecb
decompilation wip
johnchandlerburnham Oct 22, 2025
cf72c4b
decompilation progress, but failing on _cstage2
johnchandlerburnham Oct 22, 2025
f5ac204
preprocessing GroundM step, but CondenseM breaking
johnchandlerburnham Oct 23, 2025
e8454c4
fix CondenseM, GroundM breaking
johnchandlerburnham Oct 23, 2025
b1559e4
wip
johnchandlerburnham Oct 23, 2025
bf56368
GroundM and CondenseM working
johnchandlerburnham Oct 24, 2025
e886d17
CompileM/DecompileM roundtrip provisionally working up to 5% of get_env!
johnchandlerburnham Oct 24, 2025
e8d9b6e
wip
johnchandlerburnham Oct 24, 2025
03ab015
Merge branch 'main' of github.com:argumentcomputer/ix into jcb/ix-vm
johnchandlerburnham Oct 27, 2025
dff99c9
Merge branch 'main' of github.com:argumentcomputer/ix into jcb/ix-vm
johnchandlerburnham Oct 27, 2025
d7405d1
fixup for comments and clippy
johnchandlerburnham Oct 27, 2025
9e5a66f
disable aiur benchmarks due to Ixon format change
johnchandlerburnham Oct 27, 2025
be93efa
xclippy warnings
johnchandlerburnham Oct 27, 2025
3c25eb2
disable Cli test suite
johnchandlerburnham Oct 27, 2025
1cb92b9
Merge branch 'main' of github.com:argumentcomputer/ix into jcb/ixon-rs
johnchandlerburnham Oct 27, 2025
1f88638
metadata type
johnchandlerburnham Oct 28, 2025
ef821df
ixon serialization w/o testing
johnchandlerburnham Oct 28, 2025
ef21680
ixon serialization testing
johnchandlerburnham Oct 28, 2025
df51972
Merge branch 'main' of github.com:argumentcomputer/ix into jcb/ixon-rs
johnchandlerburnham Oct 28, 2025
782bcdc
clippy
johnchandlerburnham Oct 28, 2025
b9a0824
chore: Update benchmarks and Nix build (#245)
samuelburnham Oct 28, 2025
e93bb85
clippy
johnchandlerburnham Oct 28, 2025
e449f96
Merge branch 'jcb/ixon-rs' of github.com:argumentcomputer/ix into jcb…
johnchandlerburnham Oct 28, 2025
435275b
rustfmt
johnchandlerburnham Oct 28, 2025
9889705
remove meta.rs
johnchandlerburnham Oct 28, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion Ix/Ixon.lean
Original file line number Diff line number Diff line change
Expand Up @@ -474,7 +474,6 @@ structure Inductive where
nested : Nat
type : Address
ctors : List Constructor
--recrs : List Recursor
deriving BEq, Repr, Inhabited, Ord, Hashable

instance : Serialize Inductive where
Expand Down
Loading