Documentation
¶
Index ¶
- Variables
- func AllSatisfyProperty(getSlice func(output any) any, predicate func(elem any) bool, ...) eval.Property
- func And(name string, properties ...eval.Property) eval.Property
- func BoundedProperty(getValue func(output any) float64, min, max float64) eval.Property
- func ConsistencyProperty(getA, getB func(output any) any, isConsistent func(a, b any) bool, ...) eval.Property
- func IdempotenceProperty(apply func(state, delta any) any, equals func(a, b any) bool) eval.Property
- func Implies(name string, condition, consequence eval.Property) eval.Property
- func MonotonicProperty(getValue func(output any) int64) eval.Property
- func NoDuplicatesProperty(getSlice func(output any) any, getKey func(elem any) any, sliceName string) eval.Property
- func NoSoftSignalProperty(getDelta func(output any) any, getSource func(delta any) eval.SignalSource) eval.Property
- func NoUnknownSourceProperty(getSources func(output any) []eval.SignalSource) eval.Property
- func NonEmptyProperty(getCollection func(output any) any, collectionName string) eval.Property
- func NonNilProperty(getField func(output any) any, fieldName string) eval.Property
- func OnlyHardSignalsProperty(getSources func(output any) []eval.SignalSource) eval.Property
- func Or(name string, properties ...eval.Property) eval.Property
- func ProbabilityDistributionProperty(getProbs func(output any) []float64, tolerance float64) eval.Property
- func ProbabilityProperty(getProbs func(output any) []float64) eval.Property
- func SumProperty(getParts func(output any) []float64, getTotal func(output any) float64, ...) eval.Property
- type Runner
- func (r *Runner) Run(ctx context.Context, name string) (*eval.VerifyResult, error)
- func (r *Runner) RunAll(ctx context.Context) ([]*eval.VerifyResult, error)
- func (r *Runner) WithIterations(n int) *Runner
- func (r *Runner) WithParallelism(n int) *Runner
- func (r *Runner) WithStopOnFailure(stop bool) *Runner
- func (r *Runner) WithTags(tags ...string) *Runner
- func (r *Runner) WithTimeout(d time.Duration) *Runner
- type Verifier
- type VerifyOption
- func WithIterations(n int) VerifyOption
- func WithLogger(logger *slog.Logger) VerifyOption
- func WithParallelism(n int) VerifyOption
- func WithPropertyTimeout(d time.Duration) VerifyOption
- func WithShrinkIterations(n int) VerifyOption
- func WithStopOnFailure(stop bool) VerifyOption
- func WithTags(tags ...string) VerifyOption
- func WithTimeout(d time.Duration) VerifyOption
Constants ¶
This section is empty.
Variables ¶
var ( // ErrVerificationFailed indicates that one or more properties failed. ErrVerificationFailed = errors.New("verification failed") // ErrNoProperties indicates that the component has no properties to verify. ErrNoProperties = errors.New("component has no properties") // ErrNoGenerator indicates that a property has no generator and no input was provided. ErrNoGenerator = errors.New("property has no generator") )
Functions ¶
func AllSatisfyProperty ¶
func AllSatisfyProperty( getSlice func(output any) any, predicate func(elem any) bool, description string, ) eval.Property
AllSatisfyProperty creates a property that verifies all elements satisfy a predicate.
Inputs:
- getSlice: Function to extract the slice.
- predicate: Function to check each element.
- description: Description of what the predicate checks.
Outputs:
- eval.Property: A property that can be used for verification.
func And ¶
And combines multiple properties into one that passes only if all pass.
Inputs:
- name: Name for the combined property.
- properties: Properties to combine.
Outputs:
- eval.Property: A property that passes only if all pass.
func BoundedProperty ¶
BoundedProperty creates a property that verifies a value stays within bounds.
Inputs:
- getValue: Function to extract the value.
- min: Minimum allowed value.
- max: Maximum allowed value.
Outputs:
- eval.Property: A property that can be used for verification.
func ConsistencyProperty ¶
func ConsistencyProperty( getA, getB func(output any) any, isConsistent func(a, b any) bool, description string, ) eval.Property
ConsistencyProperty creates a property that verifies two values are consistent.
Inputs:
- getA: Function to extract first value.
- getB: Function to extract second value.
- isConsistent: Function to check consistency.
- description: Description of what consistency means.
Outputs:
- eval.Property: A property that can be used for verification.
func IdempotenceProperty ¶
func IdempotenceProperty( apply func(state, delta any) any, equals func(a, b any) bool, ) eval.Property
IdempotenceProperty creates a property that verifies applying the same operation twice has the same effect as applying it once.
Description:
Idempotence is important for retry safety and crash recovery. This property verifies that f(f(x)) == f(x).
Inputs:
- apply: Function to apply the operation.
- equals: Function to check equality of results.
Outputs:
- eval.Property: A property that can be used for verification.
func Implies ¶
Implies creates a property that checks "if A then B".
Inputs:
- name: Name for the combined property.
- condition: The "if" part.
- consequence: The "then" part.
Outputs:
- eval.Property: A property implementing implication.
func MonotonicProperty ¶
MonotonicProperty creates a property that verifies a value only increases.
Description:
Useful for generation counters, sequence numbers, etc. Uses atomic operations for thread safety when used in parallel verification.
Inputs:
- getValue: Function to extract the monotonic value.
Outputs:
- eval.Property: A property that can be used for verification.
Thread Safety: Safe for concurrent use via atomic operations.
Limitations:
- In parallel verification, order of checks is non-deterministic. The property verifies that each observed value is >= the previous observed value in that goroutine's execution order.
func NoDuplicatesProperty ¶
func NoDuplicatesProperty( getSlice func(output any) any, getKey func(elem any) any, sliceName string, ) eval.Property
NoDuplicatesProperty creates a property that verifies a slice has no duplicates.
Inputs:
- getSlice: Function to extract the slice.
- getKey: Function to get a comparable key from each element.
- sliceName: Name of the slice for error messages.
Outputs:
- eval.Property: A property that can be used for verification.
func NoSoftSignalProperty ¶
func NoSoftSignalProperty( getDelta func(output any) any, getSource func(delta any) eval.SignalSource, ) eval.Property
NoSoftSignalProperty creates a property that verifies no soft signals are used for state mutations.
Description:
This is the most critical property for the hard/soft signal boundary. It checks that any delta or state mutation only comes from hard signals (compiler, test, type checker, linter, syntax).
Inputs:
- getDelta: Function to extract the delta from the output.
- getSource: Function to get the signal source from the delta.
Outputs:
- eval.Property: A property that can be used for verification.
Example:
prop := correctness.NoSoftSignalProperty(
func(output any) any { return output.(*CDCLResult).LearnedClauses },
func(delta any) eval.SignalSource { return delta.(*Clause).Source },
)
func NoUnknownSourceProperty ¶
func NoUnknownSourceProperty(getSources func(output any) []eval.SignalSource) eval.Property
NoUnknownSourceProperty creates a property that verifies no signal source is unknown.
Inputs:
- getSources: Function to extract signal sources from output.
Outputs:
- eval.Property: A property that can be used for verification.
func NonEmptyProperty ¶
NonEmptyProperty creates a property that verifies a collection is not empty.
Inputs:
- getCollection: Function to extract the collection.
- collectionName: Name of the collection for error messages.
Outputs:
- eval.Property: A property that can be used for verification.
func NonNilProperty ¶
NonNilProperty creates a property that verifies a field is never nil.
Inputs:
- getField: Function to extract the field.
- fieldName: Name of the field for error messages.
Outputs:
- eval.Property: A property that can be used for verification.
func OnlyHardSignalsProperty ¶
func OnlyHardSignalsProperty(getSources func(output any) []eval.SignalSource) eval.Property
OnlyHardSignalsProperty creates a property that verifies all signal sources in a collection are hard signals.
Inputs:
- getSources: Function to extract signal sources from output.
Outputs:
- eval.Property: A property that can be used for verification.
func Or ¶
Or combines multiple properties into one that passes if any pass.
Inputs:
- name: Name for the combined property.
- properties: Properties to combine.
Outputs:
- eval.Property: A property that passes if any pass.
func ProbabilityDistributionProperty ¶
func ProbabilityDistributionProperty(getProbs func(output any) []float64, tolerance float64) eval.Property
ProbabilityDistributionProperty creates a property that verifies probabilities sum to 1.
Inputs:
- getProbs: Function to extract probability values.
- tolerance: Allowed difference from 1.0.
Outputs:
- eval.Property: A property that can be used for verification.
func ProbabilityProperty ¶
ProbabilityProperty creates a property that verifies values are valid probabilities.
Inputs:
- getProbs: Function to extract probability values.
Outputs:
- eval.Property: A property that can be used for verification.
func SumProperty ¶
func SumProperty( getParts func(output any) []float64, getTotal func(output any) float64, tolerance float64, ) eval.Property
SumProperty creates a property that verifies parts sum to a total.
Inputs:
- getParts: Function to extract the parts.
- getTotal: Function to extract the expected total.
- tolerance: Allowed difference (for floating point).
Outputs:
- eval.Property: A property that can be used for verification.
Types ¶
type Runner ¶
type Runner struct {
// contains filtered or unexported fields
}
Runner provides a high-level interface for running verification.
Example:
runner := correctness.NewRunner(registry).
WithIterations(10000).
WithParallelism(4)
results := runner.RunAll(ctx)
func (*Runner) WithIterations ¶
WithIterations configures the number of iterations.
func (*Runner) WithParallelism ¶
WithParallelism configures parallel verification.
func (*Runner) WithStopOnFailure ¶
WithStopOnFailure configures stop-on-failure behavior.
type Verifier ¶
type Verifier struct {
// contains filtered or unexported fields
}
Verifier runs property-based tests against evaluable components.
Description:
The Verifier is the core of the correctness verification framework. It generates random inputs, runs them through component properties, and reports failures with minimal counterexamples.
Thread Safety: Safe for concurrent use.
func NewVerifier ¶
NewVerifier creates a new Verifier.
Inputs:
- registry: The registry of evaluable components. Must not be nil.
Outputs:
- *Verifier: The new verifier. Never nil.
Example:
verifier := correctness.NewVerifier(registry) result, err := verifier.Verify(ctx, "cdcl")
func (*Verifier) SetLogger ¶
SetLogger sets the logger for the verifier.
Thread Safety: Safe for concurrent use.
func (*Verifier) Verify ¶
func (v *Verifier) Verify(ctx context.Context, name string, opts ...VerifyOption) (*eval.VerifyResult, error)
Verify runs all property tests for a component.
Description:
For each property, generates random inputs using the property's Generator, runs the Check function, and reports any failures. If a failure is found and the property has a Shrink function, attempts to find a minimal counterexample.
Inputs:
- ctx: Context for cancellation. Must not be nil.
- name: The name of the component to verify.
- opts: Optional configuration options.
Outputs:
- *eval.VerifyResult: The verification results.
- error: Non-nil if verification could not be performed (not if properties fail).
Example:
result, err := verifier.Verify(ctx, "cdcl",
correctness.WithIterations(10000),
correctness.WithStopOnFailure(true),
)
if err != nil {
log.Fatalf("Verification error: %v", err)
}
if !result.Passed {
for _, pr := range result.FailedProperties() {
log.Printf("Property %s failed: %v", pr.Name, pr.Error)
}
}
func (*Verifier) VerifyAll ¶
func (v *Verifier) VerifyAll(ctx context.Context, opts ...VerifyOption) ([]*eval.VerifyResult, error)
VerifyAll runs property tests for all registered components.
Inputs:
- ctx: Context for cancellation. Must not be nil.
- opts: Optional configuration options (applied to each component).
Outputs:
- []*eval.VerifyResult: Results for all components.
- error: Non-nil only if verification could not be started.
Example:
results, err := verifier.VerifyAll(ctx, correctness.WithIterations(1000))
type VerifyOption ¶
type VerifyOption func(*verifyConfig)
VerifyOption configures verification behavior.
func WithIterations ¶
func WithIterations(n int) VerifyOption
WithIterations sets the number of test iterations per property. Default is 100.
func WithLogger ¶
func WithLogger(logger *slog.Logger) VerifyOption
WithLogger sets the logger for verification progress.
func WithParallelism ¶
func WithParallelism(n int) VerifyOption
WithParallelism sets the number of properties to verify in parallel. Default is 1 (sequential).
func WithPropertyTimeout ¶
func WithPropertyTimeout(d time.Duration) VerifyOption
WithPropertyTimeout sets the timeout per property. Default is 30 seconds.
func WithShrinkIterations ¶
func WithShrinkIterations(n int) VerifyOption
WithShrinkIterations sets the maximum shrink iterations when a failure is found. Default is 100.
func WithStopOnFailure ¶
func WithStopOnFailure(stop bool) VerifyOption
WithStopOnFailure causes verification to stop at the first failure. Default is false (verify all properties).
func WithTags ¶
func WithTags(tags ...string) VerifyOption
WithTags filters properties to only those with specified tags. If empty, all properties are verified.
func WithTimeout ¶
func WithTimeout(d time.Duration) VerifyOption
WithTimeout sets the total verification timeout. Default is 5 minutes.
Source Files