[ENH] Add a tool to reason through the state space of bootstrap.

[rescrv]

Description of changes

The space of cases I have to handle:

panic(BenignRace, AlreadyInitialized, Uninitialized) -> cannot double-initialize manifest
panic(BenignRace, AlreadyInitialized, Failure) -> cannot double-initialize manifest
panic(BenignRace, AlreadyInitialized, Success) -> cannot double-initialize manifest
panic(Success, AlreadyInitialized, Uninitialized) -> cannot double-initialize manifest
panic(Success, AlreadyInitialized, Failure) -> cannot double-initialize manifest
panic(Success, AlreadyInitialized, Success) -> cannot double-initialize manifest

panic(BenignRace, Uninitialized, Failure) -> failed to install recovered manifest
panic(BenignRace, Success, Failure) -> failed to install recovered manifest
panic(Success, Uninitialized, Failure) -> failed to install recovered manifest
panic(Success, Success, Failure) -> failed to install recovered manifest

panic(BenignRace, Uninitialized, Uninitialized) -> cannot have manifest become uninitialized
panic(BenignRace, Success, Uninitialized) -> cannot have manifest become uninitialized
panic(Success, Uninitialized, Uninitialized) -> cannot have manifest become uninitialized
panic(Success, Success, Uninitialized) -> cannot have manifest become uninitialized

Committing so I don't lose it.

Test plan

This is a planning tool. It doesn't need testing as it's part of a testing effort.

Documentation Changes

No docs here.

[github-actions]

Reviewer Checklist

Please leverage this checklist to ensure your code review is thorough before approving

Testing, Bugs, Errors, Logs, Documentation

• Can you think of any use case in which the code does not behave as intended? Have they been tested?
• Can you think of any inputs or external events that could break the code? Is user input validated and safe? Have they been tested?
• If appropriate, are there adequate property based tests?
• If appropriate, are there adequate unit tests?
• Should any logging, debugging, tracing information be added or removed?
• Are error messages user-friendly?
• Have all documentation changes needed been made?
• Have all non-obvious changes been commented?

System Compatibility

• Are there any potential impacts on other parts of the system or backward compatibility?
• Does this change intersect with any items on our roadmap, and if so, is there a plan for fitting them together?

Quality

• Is this code of a unexpectedly high quality (Readability, Modularity, Intuitiveness)

[propel-code-bot]

Adding Log Sealing Feature to Chroma's WAL System

This PR adds a log sealing mechanism that prevents further writes to a collection once it's sealed. The implementation spans Go and Rust services, adding database schema changes, new API fields, and client-side handling of sealed logs. It also includes a state space reasoning tool for the WAL bootstrap process.

Key Changes:
• Added is_sealed column to collection table with migration
• Added log_is_sealed field to PushLogsResponse message in protobuf
• Updated log service to handle and propagate sealed state
• Created a state space reasoning tool for bootstrap process

Affected Areas:
• Go log repository and service implementation
• Rust log client handling of sealed logs
• Database schema and migrations
• Protocol buffer definitions

This summary was automatically generated by @propel-code-bot

[propel-code-bot]

[BestPractice]

Consider adding #[derive(PartialEq, Eq)] to all enum types since they're being compared with matches!. This improves code readability and future-proofs the enums if you need to use equality checks elsewhere.

[propel-code-bot]

[BestPractice]

The Disposition enum would benefit from adding #[derive(Debug)] to improve debugging if needed. Since it contains other Debug-derived types, this would be straightforward.

[Copilot]

Pull Request Overview

Adds a new example tool that exhaustively explores all combinations of fragment, initialization, and recovery states during bootstrap, classifying each as good, dropped, panicked, or raised.

• Introduces three enums (FragmentState, InitializeManifest, RecoverManifest) and a Disposition enum
• Implements rules (happy_paths, conflict_on_fragment, error_paths, unconditionally_raise) to categorize each state triple
• Adds a main that iterates through all states and applies rules, printing panics and raises

Comments suppressed due to low confidence (1)

rust/wal3/examples/wal3-bootstrap-reasoner.rs:102

• [nitpick] Function error_paths emits panic dispositions; consider renaming it to panic_paths or similar to more accurately reflect its behavior.

fn error_paths(fs: FragmentState, im: InitializeManifest, rm: RecoverManifest) -> Disposition {

[Copilot]

Invalid use of named formatting placeholders without supplying the corresponding arguments. Consider using positional placeholders with arguments, e.g. println!("panic({:?}, {:?}, {:?}) -> {}", fs, im, rm, reason);.

Suggested change

	println!("panic({fs:?}, {im:?}, {rm:?}) -> {reason}");
	break;
	}
	Disposition::Drop(_, _, _, _) => {
	break;
	}
	Disposition::Raise(reason, fs, im, rm) => {
	println!("raise({fs:?}, {im:?}, {rm:?}) -> {reason}");
	println!("panic({:?}, {:?}, {:?}) -> {}", fs, im, rm, reason);
	break;
	}
	Disposition::Drop(_, _, _, _) => {
	break;
	}
	Disposition::Raise(reason, fs, im, rm) => {
	println!("raise({:?}, {:?}, {:?}) -> {}", fs, im, rm, reason);

[Copilot]

Invalid use of named formatting placeholders without supplying the corresponding arguments. Consider using positional placeholders with arguments, e.g. println!("raise({:?}, {:?}, {:?}) -> {}", fs, im, rm, reason);.

Suggested change

	println!("raise({fs:?}, {im:?}, {rm:?}) -> {reason}");
	println!("raise({:?}, {:?}, {:?}) -> {}", fs, im, rm, reason);