Skip to content

Stabilize load/compile module#2

Merged
BoyeGuillaume merged 56 commits intomasterfrom
devel
Jan 31, 2026
Merged

Stabilize load/compile module#2
BoyeGuillaume merged 56 commits intomasterfrom
devel

Conversation

@BoyeGuillaume
Copy link
Copy Markdown
Owner

@BoyeGuillaume BoyeGuillaume commented Jan 31, 2026

  • Add loading / compiling of module to custom IR
  • Add IR compression through ZSTD
  • Add type checker
  • Fix bugs with compilation
  • Add C/C++ interop with the cffi crate (and cbindgen)
  • Start working toward the theorem derivation prototype
  • Improve internal storage of functions and modules

@BoyeGuillaume
Add compilation to intermediate binary
e202eba
@BoyeGuillaume
Transition to borsh for source storage and add zstd
13bc85f
@BoyeGuillaume
Refactor plugin registration macros and add formal verification module
b3229a5
@BoyeGuillaume
Rename specification -> theorems for consistency
193ea6b
@BoyeGuillaume
Add design decisions: ProofView and TerminationScope for future refer…
3c6ad0d 
…nece
@BoyeGuillaume
Convert Function to Arc<Function> in module for external ref
a95575e
@BoyeGuillaume
Add default to Function and derived_from field
8891350
@BoyeGuillaume
Starting working on introduction of new meta-analysis instruction
4cc5309
@BoyeGuillaume
BREAKING: Add correct parsing disambiguous using newline as 'breaker'
a50637e
@BoyeGuillaume
Add fast_boxed!
21fb4f6
@BoyeGuillaume
Small update was made
6779e99
@BoyeGuillaume
Convert funcana to Arc
d622572
@BoyeGuillaume
Fix use Arc
5423286
@BoyeGuillaume
Add ability to load module from bincode
c49d0cd 
TODO: Add handle to modules
@BoyeGuillaume
Add slotmap dependency and refactor module management to use SlotMap
af29483
@BoyeGuillaume
Add check on instance on python library
0cdd319
@BoyeGuillaume
Remove unsafe that was unecessary
b3b1828
@BoyeGuillaume
Add cffi interface for C/C++ API
6e6d2db
@BoyeGuillaume
Update the bump-version script
549e66c
@BoyeGuillaume
Add makefile that was ignored by CMake build
7998d92
@BoyeGuillaume
Rename from simple.c to sample.c
56cf851 
to be coherent with python example
@BoyeGuillaume
Add compilation to the C API
e41a8dd
@BoyeGuillaume
Forgot about libc dependency
239c34c
@BoyeGuillaume
Add hyLoadModule and hyDestroyModule as well as some warning when not…
3dcafa7 
… correctly destroyed
@BoyeGuillaume
Modify license comment generation
9ccd4fd
@BoyeGuillaume
Remove unsafe that was useless
14514d9
@BoyeGuillaume
Update documentation and add utlity function
9527130
@BoyeGuillaume
Update roadmap to reflect real one
278df30
@BoyeGuillaume
Add Cargo.lock
b8abbf4
@BoyeGuillaume
Update the sample.c script
b5345e6
@BoyeGuillaume
Add legacy no-zstd feature that does not compress sourced IR
2650581
@BoyeGuillaume
Remove printf in sample.c
dbaaaba
@BoyeGuillaume
Update example.func to use trap instead of returning bs
2e9f492
@BoyeGuillaume
Remove old theorem derivation
93bd716
@BoyeGuillaume
Add report in docs/
f092395
@BoyeGuillaume
rename from theorem deirvation proof to attach fn
062bf67
@BoyeGuillaume
Add capability to remove element from AttachedFunction
13ea456
@BoyeGuillaume
Add attached function tests
e710c75
@BoyeGuillaume
Update the theorem inference to derivaiotn strategy
6578032
@BoyeGuillaume
Update the documentation for the docs
f3e6439
@BoyeGuillaume
Remove old and legacy documentation
4acad8f 
Notice we did not remove formalism.typ yet because some useful
information is still written in there
@BoyeGuillaume
Add dashmap to make it sync + send
a7d1661
@BoyeGuillaume
Start implementation of the Axiomatic Strategy
a091002
@BoyeGuillaume
Add dedup optimisation to AttachedFunction and derive struct
e24c57b
@BoyeGuillaume
Start implementing clippy code cleaning
bc3998e
@BoyeGuillaume
Fix clippy issue and fmt throughout the code
ffc22b9
@BoyeGuillaume
Fix issue with cffi
16ae213
@BoyeGuillaume
Add fetch-depth for Ci (required to have info about build)
1e94289
@BoyeGuillaume
Forgot about this workflow
8fc481f
@BoyeGuillaume
Add CI for all branch
98193f6
@BoyeGuillaume
Update CI to remove verbose
9026a54
@BoyeGuillaume
Add type checking capability on the underlying IR
93ecd06
@BoyeGuillaume
Add tests for typechecking and fix bugs
3a2948e
@BoyeGuillaume
Remove warning in tests
71ffd9e
@BoyeGuillaume
Add CFFI artifacts CI for C shared library construction
9878a2a
@BoyeGuillaume
Bump version to 0.1.2
96833a4
@BoyeGuillaume BoyeGuillaume merged commit 267d6bf into master Jan 31, 2026
19 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@BoyeGuillaume