Merged
Conversation
There was a problem hiding this comment.
Pull request overview
This PR merges the tabula-rasa branch into main, representing a major rewrite that streamlines the NFP codebase. The refactor transitions from a monolithic architecture to a modular certificate-based approach, removes deprecated code, and improves the CLI interface for induction-head certification.
Changes:
- Removed deprecated files (old mixer/partition/reroute implementations, legacy IO, and soundness modules)
- Introduced new module-based organization with Core, Circuit, Model, and IO namespaces
- Added explicit certificate structures and parsing helpers for induction-head verification
- Streamlined CLI to focus on certificate checking with token verification support
Reviewed changes
Copilot reviewed 90 out of 162 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| Nfp/Reroute/Partition.lean | Removed deprecated partition/reroute infrastructure |
| Nfp/Reroute/Heat.lean | Removed deprecated heat/weighted reroute plan code |
| Nfp/Prob/Operations.lean | Added probability vector operations (pure, mix) |
| Nfp/Prob/Basic.lean | Introduced core probability vector structure |
| Nfp/Prob.lean | Refactored to aggregator for modular prob components |
| Nfp/PCC.lean | Removed deprecated PCC helpers |
| Nfp/Model/InductionPrompt.lean | Added induction prompt specifications (prev/active maps, token verification) |
| Nfp/Model/InductionHead.lean | Introduced exact induction-head input structures |
| Nfp/Model/InductionCircuit.lean | Added circuit-level induction specs |
| Nfp/Model/Gpt2.lean | Introduced GPT-2 slice structures |
| Nfp/Model.lean | New aggregator for model-specific data |
| Nfp/MixerLocalSystem.lean | Removed deprecated mixer-to-LocalSystem bridge |
| Nfp/Mixer/Operations.lean | Added modular mixer operations (push, comp, id) |
| Nfp/Mixer/Basic.lean | Introduced core mixer structure |
| Nfp/Mixer.lean | Refactored to aggregator for modular mixer components |
| Nfp/Linear/FinFold.lean | Added tail-recursive folds and rational sums |
| Nfp/Layers.lean | Removed large deprecated layer mixer implementations |
| Nfp/Influence.lean | Removed deprecated influence spec infrastructure |
| Nfp/Induction.lean | Removed deprecated TrueInductionHead formalization |
| Nfp/IO/Util.lean | Added shared IO parsing utilities |
| Nfp/IO/Parse/ValueRange/Shared.lean | Added value-range payload parsing |
| Nfp/IO/Parse/ValueRange/Cert.lean | Added value-range certificate parsing |
| Nfp/IO/Parse/ValueRange.lean | Aggregator for value-range parsing |
| Nfp/IO/Parse/SoftmaxMargin/Shared.lean | Added softmax-margin payload parsing |
| Nfp/IO/Parse/SoftmaxMargin/Cert.lean | Added softmax-margin certificate parsing |
| Nfp/IO/Parse/SoftmaxMargin.lean | Aggregator for softmax-margin parsing |
| Nfp/IO/Parse/Basic.lean | Added core parsing utilities |
| Nfp/IO/Parse.lean | Aggregator for parsing helpers |
| Nfp/IO/InductionHead/Tokens.lean | Added token list parsing for induction verification |
| Nfp/IO/InductionHead/Cert.lean | Added induction-head certificate parsing and checking |
| Nfp/IO/InductionHead.lean | Aggregator for induction-head IO |
| Nfp/IO/Checks.lean | Added certificate checking wrappers |
| Nfp/IO.lean | Refactored from monolithic loader to aggregator |
| Nfp/Core/Basic.lean | Introduced shared core definitions (Mass, ratRoundDown, ratToReal) |
| Nfp/Core.lean | Aggregator for core components |
| Nfp/Cli.lean | New minimal CLI surface for certificate checking |
| Nfp/Circuit/WellFormed.lean | Added well-formedness conditions |
| Nfp/Circuit/Typed.lean | Added typed circuit wrappers |
| Nfp/Circuit/Tensor.lean | Added tensor index aliases |
| Nfp/Circuit/Semantics.lean | Added circuit evaluation semantics |
| Nfp/Circuit/Layers/TransformerBlock.lean | Added transformer block wiring |
| Nfp/Circuit/Layers/Reshape.lean | Added reshape combinators |
| Nfp/Circuit/Layers/Induction.lean | Aggregator for induction layer components |
| Nfp/Circuit/Layers.lean | Aggregator for layer combinators |
| .gitattributes | Added beads merge configuration |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+3
to
+4
| module | ||
|
|
There was a problem hiding this comment.
Corrected spelling of 'module' (should likely be a comment directive or import, not bare keyword).
Suggested change
| module |
Nfp/IO/Parse/ValueRange/Cert.lean
Outdated
| public import Nfp.IO.Parse.ValueRange.Shared | ||
|
|
||
| /-! | ||
| Parse parsing helpers for value-range certificates. |
There was a problem hiding this comment.
Corrected spelling: 'Parse parsing' is redundant.
Suggested change
| Parse parsing helpers for value-range certificates. | |
| Parsing helpers for value-range certificates. |
Nfp/IO/Parse/SoftmaxMargin/Cert.lean
Outdated
| public import Nfp.IO.Parse.SoftmaxMargin.Shared | ||
|
|
||
| /-! | ||
| Parse parsing helpers for softmax-margin certificates. |
There was a problem hiding this comment.
Corrected spelling: 'Parse parsing' is redundant.
Suggested change
| Parse parsing helpers for softmax-margin certificates. | |
| Parsing helpers for softmax-margin certificates. |
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
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 PR merges the current tabula-rasa work into main.
Highlights:
Please review the changes and merge when ready.