feat(specs): add a [-proof-manifest] flag, emit a .json - #8

Open

clementblaudeau wants to merge 23 commits into

automatic-theorem-dev-rebasedfrom

export-list-of-obligations

Commits on Jun 2, 2026

feat: auto-generate @[spec] mvcgen lemmas from @[step] theorems (#1)

abentkamp
and
claude
committed
bdb9fa9

Commits on Jun 3, 2026

Core models option (#2)

maximebuyse
and
abentkamp
authored
8d2077c

Commits on Jun 4, 2026

Core models option update (#6)

maximebuyse
and
abentkamp
authored
157c25e

Commits on Jun 16, 2026

feat: add a module to represent specs coming from the source
clementblaudeau
committed
a203805
feat: add a flag for triggering spec gathering.
clementblaudeau
committed
f8bd140
feat(utils): Add a parser for Hax Attributes
clementblaudeau
committed
213940e
feat(extract): structure for extracting specs
clementblaudeau
committed
adc09ec
feat(hax-specs): producer for hax pre/post
clementblaudeau
committed
4aded81
feat(hax-specs): Add extraction for hax-specs
clementblaudeau
committed
b8260d3
feat(hax-specs): add a pre-pass to filter unwanted items
clementblaudeau
committed
bee3d85
test(hax-specs): add hax_specs pre/post test
clementblaudeau
committed
3e7b98f
feat(split-specs-proofs): Split specs from proof obligations
clementblaudeau
committed
4becdc5
feat(split-spec-proofs): extract proof obligations
clementblaudeau
committed
4946ee4
feat(hax-specs): emit "open Std.Do" when in mvcgen mode
clementblaudeau
committed
13b6ef9
refactor(hax-specs): improve comments
clementblaudeau
committed
47d5e03
feat(hax-specs): make config access more regular
clementblaudeau
committed
23b38c3
feat(hax-specs): add spec-dependent imports
clementblaudeau
committed
e4d642d
refactor(hax-specs): rename internal functions
clementblaudeau
committed
c4c1887
refactor: make pattern-matching explicit
clementblaudeau
committed
e7e1458
refactor: emit specs/obligations based on booleans
clementblaudeau
committed
ec09b92
doc: add comment
clementblaudeau
committed
6be6db8
test: update snapshot
clementblaudeau
committed
63c2591
feat(specs): add a [-proof-manifest] flag, emit a .json
clementblaudeau
committed
af6348e