Experiment with F* formally verified components generated via Claude#3236
Draft
Experiment with F* formally verified components generated via Claude#3236
Conversation
Mark all functions in NRadixSpec as [@@noextract_to "krml"] and remove inline_for_extraction annotations. This module serves as the ghost specification for the Pulse heap implementation. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…Spec (admitted) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Define the heap-level node type, tree pointer, find result, and the recursive is_tree slprop that links heap state to the NRadixSpec functional tree. Include ghost helper functions (elim/intro for leaf and node, case analysis) following the Pulse AVL tree pattern. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Implement heap allocation/deallocation for the verified radix tree, validating the Pulse + Box workflow with the is_tree ghost invariant. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Implement read-only tree traversal (find_walk, find, find_addr) with full proof that results equal the ghost spec's find_aux/find/find_addr. No admits required — all verification conditions discharged by Z3. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Implement verified insert_walk and insert functions that mutate the heap tree to add a network, proving the result matches NRadixSpec.insert_aux. All verification conditions discharged with no admits. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Update Makefile with Pulse include paths and shared NetworkTypes bundle - Restore inline_for_extraction on NRadixSpec functions called by NRadixPulse - Add KRML_HOST_MALLOC/FREE to krml_compat.h for Pulse Box allocation - Successfully extracts NRadixPulse.c/h with all tree operations Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Create a unified 'verified' static library from the extracted F*/Pulse C code, replacing the per-test library targets. Move add_subdirectory(verified) before add_subdirectory(lib) so collector_lib can link against it. Add missing NetworkTypes_ipnet struct definition to the extracted headers. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Replace the hand-written C++ radix tree with wrappers that forward to the formally verified NRadixPulse C library. The public API is unchanged except Insert is no longer const (tree_ is mutable to preserve const Find semantics). Phase 1 behavior changes: - Insert always returns true (verified code silently ignores duplicates) - GetAll walks the verified tree structure directly - IsAnyIPNetSubset uses GetAll + Find instead of parallel tree walk Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The collector's add_definitions for INTERESTING_SUBSYS contains commas that break C compilation of the extracted verified code. Use remove_definitions to isolate the verified library from these. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
NRadixPulse.try_insert calls find (to check for existing network at the same position) then insert. The C++ wrapper now correctly returns false on duplicate insert, matching the original C++ semantics. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Find(Address) checks if any network contains the address, but IsAnyIPNetSubset needs to check if any network fully contains another network. Find(IPNet) walks only to the query's prefix depth, giving the correct "is superset" semantics. Also simplify test_nradix.cpp to test properties directly rather than cross-comparing wrapper vs raw API. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Ignore .checked (F* cache) and .krml (Karamel intermediate) files. Extracted C and F* sources are kept. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
These existing modules define the pure types (address, ipnet) and classification functions (IsLocal, IsPublic, etc.) used by both NRadixSpec and NRadixPulse. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Skill guiding the process of adding new formally verified F*/Pulse components to the collector's verified library. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Reflects what we learned building the NRadix verified component: - Ghost-spec-as-invariant architecture (spec + Pulse + wrapper) - Pulse.Lib.Box for heap allocation (not algebraic recursive types) - option(box) pattern for nullable pointers - Karamel extraction conventions and known limitations - CMake integration with remove_definitions workaround - Lessons learned section Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## master #3236 +/- ##
==========================================
- Coverage 27.38% 26.82% -0.56%
==========================================
Files 95 95
Lines 5427 5383 -44
Branches 2548 2520 -28
==========================================
- Hits 1486 1444 -42
- Misses 3214 3216 +2
+ Partials 727 723 -4
Flags with carried forward coverage won't be shown. Click here to find out more. ☔ View full report in Codecov by Sentry. |
|
/retest collector-on-push |
2 similar comments
|
/retest collector-on-push |
|
/retest collector-on-push |
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.
Description
A detailed explanation of the changes in your PR.
Feel free to remove this section if it is overkill for your PR, and the title of your PR is sufficiently descriptive.
Checklist
Automated testing
If any of these don't apply, please comment below.
Testing Performed
TODO(replace-me)
Use this space to explain how you tested your PR, or, if you didn't test it, why you did not do so. (Valid reasons include "CI is sufficient" or "No testable changes")
In addition to reviewing your code, reviewers must also review your testing instructions, and make sure they are sufficient.
For more details, ref the Confluence page about this section.