From a45ba76d8e1bcdf62c5a18018b625276d2909271 Mon Sep 17 00:00:00 2001 From: PJ Date: Sun, 16 Aug 2026 17:45:41 +0530 Subject: [PATCH] feat(oracle-reduction): replay stored traces under four reduced oracles re-evaluates each trace offline under the full engine, a crash-only detector, a single-state check and a single-step property triple, and reports what each refutes: the oracles vary while the traces stay fixed, which separates a defect an oracle cannot express from one an explorer never reached. a disagreement with the verdicts a run recorded exits nonzero rather than being counted as a finding. --- cmd/internal-tools/oracle-reduction/load.go | 223 +++++++ .../oracle-reduction/load_test.go | 162 ++++++ cmd/internal-tools/oracle-reduction/main.go | 312 ++++++++++ cmd/internal-tools/oracle-reduction/oracle.go | 549 ++++++++++++++++++ .../oracle-reduction/oracle_test.go | 433 ++++++++++++++ cmd/internal-tools/oracle-reduction/reduce.go | 281 +++++++++ .../oracle-reduction/reduce_test.go | 222 +++++++ 7 files changed, 2182 insertions(+) create mode 100644 cmd/internal-tools/oracle-reduction/load.go create mode 100644 cmd/internal-tools/oracle-reduction/load_test.go create mode 100644 cmd/internal-tools/oracle-reduction/main.go create mode 100644 cmd/internal-tools/oracle-reduction/oracle.go create mode 100644 cmd/internal-tools/oracle-reduction/oracle_test.go create mode 100644 cmd/internal-tools/oracle-reduction/reduce.go create mode 100644 cmd/internal-tools/oracle-reduction/reduce_test.go diff --git a/cmd/internal-tools/oracle-reduction/load.go b/cmd/internal-tools/oracle-reduction/load.go new file mode 100644 index 0000000..69358a8 --- /dev/null +++ b/cmd/internal-tools/oracle-reduction/load.go @@ -0,0 +1,223 @@ +package main + +import ( + "bufio" + "encoding/json" + "fmt" + "os" + "path/filepath" + "sort" + + "github.com/priyanshujain/sanderling/internal/trace" + "github.com/priyanshujain/sanderling/internal/verifier" +) + +const maxStepBytes = 64 * 1024 * 1024 + +// loadedRun is one run directory: its meta, the steps in file order, and the +// synthetic end-of-run record the runner writes when Finalize convicted a +// liveness obligation. +type loadedRun struct { + Directory string + Meta trace.Meta + Steps []trace.Step + Finalize *trace.Step +} + +// loadRun reads a run directory and refuses anything E3 cannot replay. A step +// written before the format change carries no element depths, so its hierarchy +// decodes with a nil root and every selector resolves to nothing: the refusal +// has to name the version rather than let the replay report an empty screen. +func loadRun(directory string) (loadedRun, error) { + metaBody, err := os.ReadFile(filepath.Join(directory, "meta.json")) + if err != nil { + return loadedRun{}, fmt.Errorf("read meta: %w", err) + } + var meta trace.Meta + if err := json.Unmarshal(metaBody, &meta); err != nil { + return loadedRun{}, fmt.Errorf("decode meta: %w", err) + } + + file, err := os.Open(filepath.Join(directory, "trace.jsonl")) + if err != nil { + return loadedRun{}, fmt.Errorf("open trace: %w", err) + } + defer file.Close() + + run := loadedRun{Directory: directory, Meta: meta} + scanner := bufio.NewScanner(file) + scanner.Buffer(make([]byte, 0, 1024*1024), maxStepBytes) + line := 0 + for scanner.Scan() { + line++ + if len(scanner.Bytes()) == 0 { + continue + } + var step trace.Step + if err := json.Unmarshal(scanner.Bytes(), &step); err != nil { + return loadedRun{}, fmt.Errorf( + "decode step on line %d: %w", + line, + err, + ) + } + if step.TraceVersion != trace.TraceVersion { + return loadedRun{}, fmt.Errorf( + "step %d is trace_version %d, and E3 replays version %d only: "+ + "an older step stores no element depths, so its hierarchy decodes "+ + "with a nil root and every selector resolves to nothing on replay", + step.Index, step.TraceVersion, trace.TraceVersion) + } + run.Steps = append(run.Steps, step) + } + if err := scanner.Err(); err != nil { + return loadedRun{}, fmt.Errorf("read trace: %w", err) + } + if len(run.Steps) == 0 { + return loadedRun{}, fmt.Errorf("trace has no steps") + } + if last := run.Steps[len(run.Steps)-1]; len(run.Steps) > 1 && + last.Hierarchy == nil && + len(last.Violations) > 0 { + run.Finalize = &last + run.Steps = run.Steps[:len(run.Steps)-1] + } + if meta.Seed == 0 { + return loadedRun{}, fmt.Errorf( + "meta records no seed, so the run's bundle cannot be reproduced", + ) + } + return run, nil +} + +// finalizeIndex is the step index the runner gives its end-of-run record: one +// past the last step it wrote. +func (r loadedRun) finalizeIndex() int { + return r.Steps[len(r.Steps)-1].Index + 1 +} + +// extractorFold reconstructs every extractor's value at each step from the +// recorded per-step diffs. A run's trace stores what changed, so the value an +// extractor held at a step is the last change at or before it; an extractor +// that never changed held JSON null throughout, which is what an unwritten +// diff means. +func extractorFold( + steps []trace.Step, + names []string, +) ([]map[int]json.RawMessage, error) { + index := make(map[string]int, len(names)) + for position, name := range names { + index[name] = position + } + current := make(map[int]json.RawMessage, len(names)) + for position := range names { + current[position] = json.RawMessage("null") + } + folded := make([]map[int]json.RawMessage, len(steps)) + for step := range steps { + for name, change := range steps[step].ExtractorChanges { + position, ok := index[name] + if !ok { + return nil, fmt.Errorf( + "step %d records extractor %q, which the spec does not register; "+ + "the trace and the spec are not the same bundle", + steps[step].Index, + name, + ) + } + current[position] = change.Curr + } + snapshot := make(map[int]json.RawMessage, len(current)) + for position, value := range current { + snapshot[position] = value + } + folded[step] = snapshot + } + return folded, nil +} + +// lastActionFor rebuilds the action the runner had applied before the next +// step observed. An action the runner chose but never dispatched left +// state.lastAction null, and the recorded skip reason is what says so. +func lastActionFor(step trace.Step) *verifier.Action { + if step.NextAction == nil || step.ActionSkipped != "" { + return nil + } + recorded := *step.NextAction + action := verifier.Action{ + Kind: verifier.ActionKind(recorded.Kind), + On: recorded.Selector, + Text: recorded.Text, + X: recorded.X, + Y: recorded.Y, + FromX: recorded.FromX, + FromY: recorded.FromY, + ToX: recorded.ToX, + ToY: recorded.ToY, + Key: recorded.Key, + DurationMillis: recorded.DurationMillis, + } + return &action +} + +func traceLogs(entries []trace.LogEntry) []verifier.LogEntry { + if len(entries) == 0 { + return nil + } + logs := make([]verifier.LogEntry, 0, len(entries)) + for _, entry := range entries { + logs = append(logs, verifier.LogEntry{ + UnixMillis: entry.UnixMillis, + Level: entry.Level, + Tag: entry.Tag, + Message: entry.Message, + }) + } + return logs +} + +func traceExceptions(entries []trace.Exception) []verifier.Exception { + if len(entries) == 0 { + return nil + } + exceptions := make([]verifier.Exception, 0, len(entries)) + for _, entry := range entries { + exceptions = append(exceptions, verifier.Exception{ + Class: entry.Class, + Message: entry.Message, + StackTrace: entry.StackTrace, + UnixMillis: entry.UnixMillis, + }) + } + return exceptions +} + +// discoverRuns finds every run directory at or below root, a run directory +// being one holding both meta.json and trace.jsonl. +func discoverRuns(root string) ([]string, error) { + var directories []string + err := filepath.Walk( + root, + func(path string, info os.FileInfo, err error) error { + if err != nil { + return err + } + if !info.IsDir() { + return nil + } + if _, statErr := os.Stat(filepath.Join(path, "trace.jsonl")); statErr != nil { + return nil + } + if _, statErr := os.Stat(filepath.Join(path, "meta.json")); statErr != nil { + return nil + } + directories = append(directories, path) + return nil + }, + ) + if err != nil { + return nil, err + } + sort.Strings(directories) + return directories, nil +} diff --git a/cmd/internal-tools/oracle-reduction/load_test.go b/cmd/internal-tools/oracle-reduction/load_test.go new file mode 100644 index 0000000..7ddea11 --- /dev/null +++ b/cmd/internal-tools/oracle-reduction/load_test.go @@ -0,0 +1,162 @@ +package main + +import ( + "encoding/json" + "os" + "path/filepath" + "strings" + "testing" + + "github.com/priyanshujain/sanderling/internal/trace" + "github.com/priyanshujain/sanderling/internal/verifier" +) + +func writeRunFiles(t *testing.T, directory, meta string, steps ...string) { + t.Helper() + if err := os.WriteFile(filepath.Join(directory, "meta.json"), []byte(meta), 0o644); err != nil { + t.Fatal(err) + } + body := strings.Join(steps, "\n") + "\n" + if err := os.WriteFile(filepath.Join(directory, "trace.jsonl"), []byte(body), 0o644); err != nil { + t.Fatal(err) + } +} + +func TestLoadRunRefusesAStepFromBeforeTheFormatChange(t *testing.T) { + directory := t.TempDir() + writeRunFiles( + t, + directory, + `{"seed": 3}`, + `{"step":1,"timestamp":"2026-08-15T12:00:00Z"}`, + ) + + _, err := loadRun(directory) + + if err == nil { + t.Fatal("a version-0 step must be refused") + } + if !strings.Contains(err.Error(), "trace_version 0") || + !strings.Contains(err.Error(), "depths") { + t.Errorf( + "the refusal must name the version and why it cannot replay: %v", + err, + ) + } +} + +func TestLoadRunRefusesARunWithNoSeed(t *testing.T) { + directory := t.TempDir() + writeRunFiles( + t, + directory, + `{}`, + `{"step":1,"trace_version":1,"timestamp":"2026-08-15T12:00:00Z"}`, + ) + + _, err := loadRun(directory) + + if err == nil || !strings.Contains(err.Error(), "seed") { + t.Errorf("a run without a seed cannot be bundled as it was: %v", err) + } +} + +func TestLoadRunSplitsOffTheEndOfRunRecord(t *testing.T) { + directory := t.TempDir() + writeRunFiles( + t, + directory, + `{"seed": 3}`, + `{"step":1,"trace_version":1,"timestamp":"2026-08-15T12:00:00Z","hierarchy":{"elements":[],"depths":[]}}`, + `{"step":2,"trace_version":1,"timestamp":"2026-08-15T12:00:01Z","violations":["reachable"]}`, + ) + + run, err := loadRun(directory) + if err != nil { + t.Fatal(err) + } + + if len(run.Steps) != 1 { + t.Fatalf("observation steps: got %d, want 1", len(run.Steps)) + } + if run.Finalize == nil || run.Finalize.Index != 2 { + t.Fatalf("finalize record: %+v", run.Finalize) + } + if run.finalizeIndex() != 2 { + t.Errorf("finalize index: got %d, want 2", run.finalizeIndex()) + } +} + +func TestExtractorFoldCarriesAValueForwardUntilItChanges(t *testing.T) { + steps := []trace.Step{ + {Index: 1, ExtractorChanges: map[string]trace.ExtractorChange{ + "count": { + Prev: json.RawMessage("null"), + Curr: json.RawMessage("1"), + }, + }}, + {Index: 2}, + {Index: 3, ExtractorChanges: map[string]trace.ExtractorChange{ + "count": {Prev: json.RawMessage("1"), Curr: json.RawMessage("4")}, + }}, + } + + folded, err := extractorFold(steps, []string{"count", "unseen"}) + if err != nil { + t.Fatal(err) + } + + want := []string{"1", "1", "4"} + for position, expected := range want { + if got := string(folded[position][0]); got != expected { + t.Errorf( + "count at step %d: got %s, want %s", + position+1, + got, + expected, + ) + } + if got := string(folded[position][1]); got != "null" { + t.Errorf( + "an extractor that never changed must fold to null, got %s", + got, + ) + } + } +} + +func TestExtractorFoldRefusesAValueTheSpecCannotPlace(t *testing.T) { + steps := []trace.Step{ + {Index: 1, ExtractorChanges: map[string]trace.ExtractorChange{ + "gone": {Curr: json.RawMessage("1")}, + }}, + } + + _, err := extractorFold(steps, []string{"count"}) + + if err == nil || !strings.Contains(err.Error(), "gone") { + t.Errorf("an unplaceable extractor value must be refused: %v", err) + } +} + +func TestLastActionIsEmptyWhenTheRunnerNeverDispatchedIt(t *testing.T) { + dispatched := trace.Step{ + NextAction: &trace.Action{Kind: "Tap", Selector: "id:save", X: 4, Y: 5}, + } + skipped := trace.Step{ + NextAction: &trace.Action{Kind: "Tap", Selector: "id:save"}, + ActionSkipped: foregroundLossReason, + } + + action := lastActionFor(dispatched) + if action == nil || action.Kind != verifier.ActionKindTap || + action.On != "id:save" || + action.X != 4 { + t.Fatalf("dispatched action: %+v", action) + } + if lastActionFor(skipped) != nil { + t.Error( + "an action the runner threw away never reached state.lastAction", + ) + } +} diff --git a/cmd/internal-tools/oracle-reduction/main.go b/cmd/internal-tools/oracle-reduction/main.go new file mode 100644 index 0000000..8e5b00f --- /dev/null +++ b/cmd/internal-tools/oracle-reduction/main.go @@ -0,0 +1,312 @@ +// Command oracle-reduction re-evaluates stored traces offline under four +// oracles and reports what each one refutes: the full engine, a crash-only +// detector, a single-state check, and a single-step property triple. The +// oracles vary while the traces stay fixed, which is what separates a defect an +// oracle cannot express from one an explorer never reached. +// +// The offline engine has to reproduce the verdicts each run recorded. A +// disagreement is a bug here or a gap in the trace, so it is reported as a +// mismatch and exits nonzero rather than being counted as a finding. +package main + +import ( + "encoding/json" + "flag" + "fmt" + "io" + "os" + "sort" + "strings" + + "github.com/priyanshujain/sanderling/internal/testrun" +) + +const usage = `oracle-reduction replays stored traces under reduced oracles. + +Usage: + oracle-reduction --runs [--output ] [--spec ] + +--runs is scanned recursively; every directory holding meta.json and +trace.jsonl is one trace. Each trace's spec is bundled from the path its +meta.json records unless --spec overrides it. + +Exit status is 2 when the offline engine disagreed with any run's recorded +verdicts, which blocks the experiment rather than reporting the difference as +noise. + +A reduced oracle whose rewrite no longer states a property reports +cannot_express for it rather than a verdict, and the property is temporal-only +when the other reductions also fail to state or refute it. A property whose +window is longer than the two observations a triple spans is reported with +single_step_truncates_window, which is the form that decides it. +` + +type config struct { + runsRoot string + outputPath string + specPath string + // hostExtractors re-runs the spec's extractor getters over each stored + // hierarchy instead of replaying the values a web run's page computed. It + // asks a different question of the same trace: whether the stored tree + // alone carries what the properties read. + hostExtractors bool +} + +func parseArguments(arguments []string, stderr io.Writer) (config, error) { + flagSet := flag.NewFlagSet("oracle-reduction", flag.ContinueOnError) + flagSet.SetOutput(stderr) + flagSet.Usage = func() { + fmt.Fprint(stderr, usage) + flagSet.PrintDefaults() + } + var configuration config + flagSet.StringVar( + &configuration.runsRoot, + "runs", + "", + "directory tree holding the run directories to replay (required)", + ) + flagSet.StringVar( + &configuration.outputPath, + "output", + "", + "file to write the per-trace JSONL to (default stdout)", + ) + flagSet.StringVar( + &configuration.specPath, + "spec", + "", + "spec to bundle instead of the one each meta.json records", + ) + flagSet.BoolVar( + &configuration.hostExtractors, + "host-extractors", + false, + "re-run the spec's extractors over each stored hierarchy instead of replaying the values a web run's page computed", + ) + if err := flagSet.Parse(arguments); err != nil { + return config{}, err + } + if configuration.runsRoot == "" { + return config{}, fmt.Errorf("--runs is required") + } + return configuration, nil +} + +func main() { + configuration, err := parseArguments(os.Args[1:], os.Stderr) + if err != nil { + fmt.Fprintf(os.Stderr, "oracle-reduction: %v\n", err) + os.Exit(1) + } + code, err := run(configuration, os.Stdout, os.Stderr) + if err != nil { + fmt.Fprintf(os.Stderr, "oracle-reduction: %v\n", err) + os.Exit(1) + } + os.Exit(code) +} + +func run(configuration config, stdout, stderr io.Writer) (int, error) { + directories, err := discoverRuns(configuration.runsRoot) + if err != nil { + return 1, err + } + if len(directories) == 0 { + return 1, fmt.Errorf( + "no run directories under %s", + configuration.runsRoot, + ) + } + + output := stdout + if configuration.outputPath != "" { + file, createErr := os.Create(configuration.outputPath) + if createErr != nil { + return 1, createErr + } + defer file.Close() + output = file + } + encoder := json.NewEncoder(output) + + var reports []runReport + rejected := 0 + for _, directory := range directories { + loaded, loadErr := loadRun(directory) + if loadErr != nil { + rejected++ + fmt.Fprintf(stderr, "skipped %s: %v\n", directory, loadErr) + continue + } + specPath := loaded.Meta.SpecPath + if configuration.specPath != "" { + specPath = configuration.specPath + } + bundle, bundleErr := testrun.BundleSpec(specPath, loaded.Meta.Seed) + if bundleErr != nil { + return 1, fmt.Errorf( + "%s: bundle %s: %w", + directory, + specPath, + bundleErr, + ) + } + if loaded.Meta.BundleSHA256 != "" && + bundle.SHA256 != loaded.Meta.BundleSHA256 { + // The bundler writes each module's path into the output relative to + // the working directory, so this differs whenever the replay is + // invoked from somewhere else than the run was. What a changed spec + // would actually break is caught by the property set, the extractor + // names and the residual comparison below. + fmt.Fprintf(stderr, + "note: %s bundles to %s here and the run recorded %s\n", + directory, bundle.SHA256[:12], loaded.Meta.BundleSHA256[:12]) + } + report, replayErr := replay( + loaded, + string(bundle.JavaScript), + configuration.hostExtractors, + ) + if replayErr != nil { + return 1, fmt.Errorf("%s: %w", directory, replayErr) + } + if err := encoder.Encode(report); err != nil { + return 1, err + } + reports = append(reports, report) + } + + summarize(reports, rejected, stderr) + for _, report := range reports { + if !report.Valid { + return 2, nil + } + } + if len(reports) == 0 { + return 1, fmt.Errorf( + "every run directory was rejected; nothing was replayed", + ) + } + return 0, nil +} + +func summarize(reports []runReport, rejected int, out io.Writer) { + invalid := 0 + crashed := 0 + weakest := map[string]int{} + byClass := map[string]map[string]int{} + inexpressible := map[string]map[string]bool{} + unmatched := 0 + engineRefutations := 0 + for _, report := range reports { + if !report.Valid { + invalid++ + } + if report.CrashOnly.Fired { + crashed++ + } + for _, property := range report.Properties { + recordInexpressible( + inexpressible, + "single-state", + property.SingleState, + property.Property, + ) + recordInexpressible( + inexpressible, + "single-step", + property.SingleStep, + property.Property, + ) + if !property.Engine.Refuted { + if property.SingleState.Refuted || property.SingleStep.Refuted { + unmatched++ + } + continue + } + engineRefutations++ + weakest[property.Weakest]++ + if byClass[property.Class] == nil { + byClass[property.Class] = map[string]int{} + } + byClass[property.Class][property.Weakest]++ + } + } + + fmt.Fprintf( + out, + "\ntraces replayed: %d (rejected: %d)\n", + len(reports), + rejected, + ) + fmt.Fprintf( + out, + "validity: %d of %d reproduced the recorded verdicts exactly\n", + len(reports)-invalid, + len(reports), + ) + fmt.Fprintf(out, "traces where crash-only fired: %d\n", crashed) + fmt.Fprintf(out, "engine refutations: %d\n", engineRefutations) + if engineRefutations > 0 { + fmt.Fprintf(out, "weakest refuting oracle: %s\n", counts(weakest)) + for _, class := range sortedKeys(byClass) { + fmt.Fprintf(out, " %s: %s\n", class, counts(byClass[class])) + } + fmt.Fprintf(out, "temporal-only fraction: %.3f\n", + float64(weakest["temporal-only"])/float64(engineRefutations)) + } + fmt.Fprintf( + out, + "properties a reduced oracle cannot express: %s\n", + counts(distinct(inexpressible)), + ) + fmt.Fprintf( + out, + "reduced-oracle refutations the engine did not make: %d\n", + unmatched, + ) +} + +// recordInexpressible counts a property once per oracle however many traces it +// appears on, because whether an oracle can state a property is a fact about +// the property and not about the run. +func recordInexpressible( + seen map[string]map[string]bool, + oracle string, + finding refutation, + property string, +) { + if !finding.CannotExpress { + return + } + if seen[oracle] == nil { + seen[oracle] = map[string]bool{} + } + seen[oracle][property] = true +} + +func distinct(seen map[string]map[string]bool) map[string]int { + sizes := map[string]int{} + for oracle, properties := range seen { + sizes[oracle] = len(properties) + } + return sizes +} + +func counts(values map[string]int) string { + parts := make([]string, 0, len(values)) + for _, key := range sortedKeys(values) { + parts = append(parts, fmt.Sprintf("%s=%d", key, values[key])) + } + return strings.Join(parts, " ") +} + +func sortedKeys[V any](values map[string]V) []string { + keys := make([]string, 0, len(values)) + for key := range values { + keys = append(keys, key) + } + sort.Strings(keys) + return keys +} diff --git a/cmd/internal-tools/oracle-reduction/oracle.go b/cmd/internal-tools/oracle-reduction/oracle.go new file mode 100644 index 0000000..e9e53f6 --- /dev/null +++ b/cmd/internal-tools/oracle-reduction/oracle.go @@ -0,0 +1,549 @@ +package main + +import ( + "bytes" + "encoding/json" + "fmt" + "sort" + + "github.com/priyanshujain/sanderling/internal/ltl" + "github.com/priyanshujain/sanderling/internal/trace" + "github.com/priyanshujain/sanderling/internal/verifier" +) + +// foregroundLossReason is the skip reason internal/runner records when the app +// was no longer the foreground process at action time. It is the only +// foreground signal a stored trace carries, and it is what the crash-only +// oracle reads for "the application is no longer the foreground process". +const foregroundLossReason = "app_left_foreground" + +// refutation is one oracle's finding for one property on one trace. A reduced +// oracle has three of them and not two: CannotExpress says its rewrite no +// longer states the property, which is neither a refutation nor a clean bill. +type refutation struct { + Refuted bool `json:"refuted"` + CannotExpress bool `json:"cannot_express,omitempty"` + // Step is the observation whose evaluation produced the violation; + // OriginStep is the observation whose obligation failed, which for a + // deferred one is earlier. + Step int `json:"step,omitempty"` + OriginStep int `json:"origin_step,omitempty"` + Reason string `json:"reason,omitempty"` + IsError bool `json:"is_error,omitempty"` +} + +type propertyReport struct { + Property string `json:"property"` + Class string `json:"class"` + TopLevel string `json:"top_level"` + Engine refutation `json:"engine"` + SingleState refutation `json:"single_state"` + SingleStep refutation `json:"single_step"` + // SingleStepTruncatesWindow marks a property whose window the triple had to + // shorten to two observations, so what its single-step column refutes is a + // stronger property than the one the author wrote. + SingleStepTruncatesWindow bool `json:"single_step_truncates_window,omitempty"` + // Weakest names the weakest oracle that refutes this property on this + // trace, and is empty unless the engine refuted it. "temporal-only" means + // no reduced oracle did. + Weakest string `json:"weakest_refuting_oracle,omitempty"` +} + +type crashReport struct { + Fired bool `json:"fired"` + FirstStep int `json:"first_step,omitempty"` + ExceptionSteps []int `json:"exception_steps,omitempty"` + ForegroundLossSteps []int `json:"foreground_loss_steps,omitempty"` + ErrorLogSteps []int `json:"error_log_steps,omitempty"` +} + +// mismatch is one disagreement between the offline engine and the verdicts the +// run recorded. Any of these blocks the trace's result. +type mismatch struct { + Property string `json:"property"` + Field string `json:"field"` + Online string `json:"online"` + Offline string `json:"offline"` +} + +type runReport struct { + Run string `json:"run"` + Seed int64 `json:"seed"` + Platform string `json:"platform"` + Arm string `json:"arm,omitempty"` + Generator string `json:"generator,omitempty"` + // ReplayMode says where the extractor values under replay came from: + // "page-extractor-values" reuses what the page computed in V8 and the run + // evaluated against, "host-extractors" re-runs the spec's getters over the + // stored hierarchy. + ReplayMode string `json:"replay_mode"` + StepsObserved int `json:"steps_observed"` + StepsSkipped int `json:"steps_skipped"` + Valid bool `json:"valid"` + Mismatches []mismatch `json:"mismatches,omitempty"` + // ResidualMismatches counts every step whose replayed residual formula + // differed from the recorded one, of which Mismatches carries the first + // few. The recorded residual is the engine's whole pending state, so + // agreement on it is a stronger claim than agreement on the verdicts. + ResidualMismatches int `json:"residual_mismatches"` + CrashOnly crashReport `json:"crash_only"` + Properties []propertyReport `json:"properties"` + ActionsUnbounded int `json:"actions_without_resolved_bounds"` + ScrollActions int `json:"scroll_last_actions"` +} + +// witnessRecord is one violation as either side reports it: the step it was +// recorded at, plus the witness the engine attached. +type witnessRecord struct { + RecordedStep int + OriginStep int + DetectedStep int + Reason string + IsError bool +} + +// replay re-evaluates one run offline under all four oracles. The engine's +// offline verdicts are compared against the ones the run recorded, and the +// report is marked invalid on any disagreement: a mismatch is a bug here or a +// gap in the trace, not a finding. +func replay( + run loadedRun, + bundleJavaScript string, + hostExtractors bool, +) (runReport, error) { + engine, err := verifier.New( + verifier.WithSeed(uint64(run.Meta.Seed)), + verifier.WithPlatform(run.Meta.Platform), + verifier.WithAppPackage(run.Meta.BundleID), + ) + if err != nil { + return runReport{}, fmt.Errorf("verifier: %w", err) + } + if err := engine.Load(bundleJavaScript); err != nil { + return runReport{}, fmt.Errorf("load spec: %w", err) + } + formulas, err := engine.PropertyFormulas() + if err != nil { + return runReport{}, err + } + + singleState := map[string]*ltl.Evaluator{} + singleStep := map[string]*ltl.Evaluator{} + for name, formula := range formulas { + singleState[name] = ltl.NewEvaluator(singleStateFormula(formula)) + singleStep[name] = ltl.NewEvaluator(singleStepFormula(formula)) + } + + usePageValues := run.Meta.Platform == "web" && !hostExtractors + report := runReport{ + Run: run.Directory, + Seed: run.Meta.Seed, + Platform: run.Meta.Platform, + Arm: run.Meta.Arm, + Generator: run.Meta.Generator, + ReplayMode: "host-extractors", + } + var folded []map[int]json.RawMessage + if usePageValues { + report.ReplayMode = "page-extractor-values" + folded, err = extractorFold(run.Steps, engine.ExtractorNames()) + if err != nil { + return runReport{}, err + } + } + + offline := map[string]witnessRecord{} + stateFired := map[string]int{} + stepFired := map[string]int{} + var residualMismatches []mismatch + var lastAction *verifier.Action + for position, step := range run.Steps { + if step.NextAction != nil && step.NextAction.Selector != "" && + step.NextAction.ResolvedBounds == nil { + report.ActionsUnbounded++ + } + if step.SkippedVerification { + report.StepsSkipped++ + residualMismatches = append( + residualMismatches, + compareResiduals(step, engine.Residuals())...) + lastAction = lastActionFor(step) + continue + } + if lastAction != nil && lastAction.Kind == verifier.ActionKindScroll { + report.ScrollActions++ + } + if err := engine.PushSnapshot(verifier.SnapshotInput{ + Tree: step.Hierarchy, + LastAction: lastAction, + StepTime: step.Timestamp, + StepIndex: step.Index, + RunStart: run.Meta.StartedAt, + Logs: traceLogs(step.Logs), + Exceptions: traceExceptions(step.Exceptions), + }); err != nil { + return runReport{}, fmt.Errorf("step %d push: %w", step.Index, err) + } + if usePageValues { + skipped, overrideErr := engine.OverrideExtractorValues( + folded[position], + ) + if overrideErr != nil { + return runReport{}, fmt.Errorf( + "step %d override: %w", + step.Index, + overrideErr, + ) + } + if skipped > 0 { + return runReport{}, fmt.Errorf( + "step %d: %d recorded extractor values fell outside the spec's extractor list", + step.Index, + skipped, + ) + } + } + engine.EvaluateProperties() + for _, name := range engine.NewlyViolatedProperties() { + offline[name] = witnessFrom(engine.Witness(name), step.Index) + } + residualMismatches = append( + residualMismatches, + compareResiduals(step, engine.Residuals())...) + for name := range formulas { + recordFiring( + stateFired, + name, + singleState[name].ObserveAtStep(step.Timestamp, step.Index), + step.Index, + ) + recordFiring( + stepFired, + name, + singleStep[name].ObserveAtStep(step.Timestamp, step.Index), + step.Index, + ) + } + report.StepsObserved++ + lastAction = lastActionFor(step) + } + + finalizeIndex := run.finalizeIndex() + for _, name := range engine.Finalize() { + offline[name] = witnessFrom(engine.Witness(name), finalizeIndex) + } + for name := range formulas { + recordFiring( + stateFired, + name, + singleState[name].Finalize(), + finalizeIndex, + ) + recordFiring( + stepFired, + name, + singleStep[name].Finalize(), + finalizeIndex, + ) + } + + report.CrashOnly = crashOnly(run) + report.Mismatches = compareVerdicts(onlineVerdicts(run), offline) + report.ResidualMismatches = len(residualMismatches) + if len(residualMismatches) > reportedResiduals { + residualMismatches = residualMismatches[:reportedResiduals] + } + report.Mismatches = append(report.Mismatches, residualMismatches...) + report.Valid = len(report.Mismatches) == 0 + + names := make([]string, 0, len(formulas)) + for name := range formulas { + names = append(names, name) + } + sort.Strings(names) + for _, name := range names { + property := propertyReport{ + Property: name, + Class: propertyClass(formulas[name]), + TopLevel: topLevelForm(formulas[name]), + Engine: engineRefutation(offline, name), + SingleState: reducedRefutation( + singleStateExpresses(formulas[name]), + singleState[name], + stateFired[name], + ), + SingleStep: reducedRefutation( + singleStepExpresses(formulas[name]), + singleStep[name], + stepFired[name], + ), + + SingleStepTruncatesWindow: truncatesWindow(formulas[name]), + } + property.Weakest = weakestOracle(property, report.CrashOnly) + report.Properties = append(report.Properties, property) + } + return report, nil +} + +// reportedResiduals caps how many residual differences one trace lists. The +// count of all of them is reported alongside; the first few are what says +// where the two engines parted. +const reportedResiduals = 5 + +// compareResiduals checks the replayed pending state against the one the step +// recorded. A step the verifier skipped still recorded the residual it was +// holding, so those steps assert that a skipped step advanced nothing. +func compareResiduals( + step trace.Step, + replayed map[string]ltl.Formula, +) []mismatch { + if len(step.Residuals) == 0 { + return nil + } + var mismatches []mismatch + names := make([]string, 0, len(step.Residuals)) + for name := range step.Residuals { + names = append(names, name) + } + sort.Strings(names) + for _, name := range names { + formula, ok := replayed[name] + if !ok { + mismatches = append(mismatches, mismatch{ + Property: name, + Field: fmt.Sprintf("residual at step %d", step.Index), + Online: string(step.Residuals[name]), + Offline: "property not registered", + }) + continue + } + encoded, err := json.Marshal(formula) + if err != nil { + encoded = []byte(fmt.Sprintf("%q", err.Error())) + } + if !bytes.Equal(encoded, step.Residuals[name]) { + mismatches = append(mismatches, mismatch{ + Property: name, + Field: fmt.Sprintf("residual at step %d", step.Index), + Online: string(step.Residuals[name]), + Offline: string(encoded), + }) + } + } + return mismatches +} + +func witnessFrom(witness *verifier.Witness, recordedStep int) witnessRecord { + record := witnessRecord{RecordedStep: recordedStep} + if witness == nil { + return record + } + record.OriginStep = witness.Step + record.DetectedStep = witness.DetectedStep + record.Reason = witness.Reason + record.IsError = witness.IsError + return record +} + +// onlineVerdicts reads the violations the run recorded, including the +// end-of-run record a finalized liveness obligation is written to. +func onlineVerdicts(run loadedRun) map[string]witnessRecord { + recorded := map[string]witnessRecord{} + steps := run.Steps + if run.Finalize != nil { + steps = append(append([]trace.Step(nil), steps...), *run.Finalize) + } + for _, step := range steps { + for _, name := range step.Violations { + record := witnessRecord{RecordedStep: step.Index} + if witness, ok := step.Witnesses[name]; ok { + record.OriginStep = witness.Step + record.DetectedStep = witness.DetectedStep + record.Reason = witness.Reason + record.IsError = witness.IsError + } + recorded[name] = record + } + } + return recorded +} + +func compareVerdicts(online, offline map[string]witnessRecord) []mismatch { + var mismatches []mismatch + names := map[string]bool{} + for name := range online { + names[name] = true + } + for name := range offline { + names[name] = true + } + ordered := make([]string, 0, len(names)) + for name := range names { + ordered = append(ordered, name) + } + sort.Strings(ordered) + + for _, name := range ordered { + recorded, wasRecorded := online[name] + replayed, wasReplayed := offline[name] + switch { + case wasRecorded && !wasReplayed: + mismatches = append(mismatches, mismatch{ + Property: name, Field: "violated", + Online: fmt.Sprintf( + "violated at step %d", + recorded.RecordedStep, + ), + Offline: "not violated", + }) + continue + case !wasRecorded && wasReplayed: + mismatches = append(mismatches, mismatch{ + Property: name, Field: "violated", + Online: "not violated", + Offline: fmt.Sprintf( + "violated at step %d", + replayed.RecordedStep, + ), + }) + continue + case !wasRecorded: + continue + } + for _, field := range []struct { + name string + online string + offline string + }{ + {"step", fmt.Sprint(recorded.RecordedStep), fmt.Sprint(replayed.RecordedStep)}, + {"origin_step", fmt.Sprint(recorded.OriginStep), fmt.Sprint(replayed.OriginStep)}, + {"detected_step", fmt.Sprint(recorded.DetectedStep), fmt.Sprint(replayed.DetectedStep)}, + {"reason", recorded.Reason, replayed.Reason}, + } { + if field.online != field.offline { + mismatches = append(mismatches, mismatch{ + Property: name, Field: field.name, + Online: field.online, Offline: field.offline, + }) + } + } + } + return mismatches +} + +// crashOnly fires where the application left the foreground or an error +// surface was recorded. Error-level log lines are reported alongside rather +// than folded in: a console error is not a crash, and an analysis that wants +// the looser detector can read the steps from here. +func crashOnly(run loadedRun) crashReport { + report := crashReport{} + for _, step := range run.Steps { + if len(step.Exceptions) > 0 { + report.ExceptionSteps = append(report.ExceptionSteps, step.Index) + } + if step.ActionSkipped == foregroundLossReason { + report.ForegroundLossSteps = append( + report.ForegroundLossSteps, + step.Index, + ) + } + for _, entry := range step.Logs { + if entry.Level == "E" || entry.Level == "F" { + report.ErrorLogSteps = append(report.ErrorLogSteps, step.Index) + break + } + } + } + first := 0 + for _, step := range append(append([]int(nil), report.ExceptionSteps...), report.ForegroundLossSteps...) { + if first == 0 || step < first { + first = step + } + } + report.Fired = first != 0 + report.FirstStep = first + return report +} + +func engineRefutation( + offline map[string]witnessRecord, + name string, +) refutation { + record, ok := offline[name] + if !ok { + return refutation{} + } + return refutation{ + Refuted: true, + Step: record.RecordedStep, + OriginStep: record.OriginStep, + Reason: record.Reason, + IsError: record.IsError, + } +} + +// reducedRefutation reports a reduced oracle's finding, or its inability to +// state the property at all. The evaluator is driven either way so that the +// verdict a reduction would have reached is never what decides whether it was +// entitled to reach one. +func reducedRefutation( + expresses bool, + evaluator *ltl.Evaluator, + firedAt int, +) refutation { + if !expresses { + return refutation{CannotExpress: true} + } + return evaluatorRefutation(evaluator, firedAt) +} + +func evaluatorRefutation(evaluator *ltl.Evaluator, firedAt int) refutation { + violation := evaluator.Violation() + if violation == nil { + return refutation{} + } + return refutation{ + Refuted: true, + Step: firedAt, + OriginStep: violation.Step, + Reason: violation.Reason, + IsError: violation.IsError, + } +} + +// recordFiring keeps the first observation at which a reduced oracle latched, +// which the evaluator itself does not carry. +func recordFiring( + fired map[string]int, + name string, + verdict ltl.Verdict, + step int, +) { + if verdict != ltl.VerdictViolated { + return + } + if _, ok := fired[name]; ok { + return + } + fired[name] = step +} + +// weakestOracle names the weakest oracle that refutes a defect the engine +// refuted, in the order a crash detector, a single-state check and a +// single-step triple are weaker than the engine. +func weakestOracle(property propertyReport, crash crashReport) string { + if !property.Engine.Refuted { + return "" + } + switch { + case crash.Fired: + return "crash-only" + case property.SingleState.Refuted: + return "single-state" + case property.SingleStep.Refuted: + return "single-step" + default: + return "temporal-only" + } +} diff --git a/cmd/internal-tools/oracle-reduction/oracle_test.go b/cmd/internal-tools/oracle-reduction/oracle_test.go new file mode 100644 index 0000000..1af0b92 --- /dev/null +++ b/cmd/internal-tools/oracle-reduction/oracle_test.go @@ -0,0 +1,433 @@ +package main + +import ( + "encoding/json" + "fmt" + "os" + "path/filepath" + "strings" + "testing" + "time" + + "github.com/priyanshujain/sanderling/internal/hierarchy" + "github.com/priyanshujain/sanderling/internal/trace" + "github.com/priyanshujain/sanderling/internal/verifier" +) + +// fixtureSpec counts rows on screen and asserts three things about them: a +// bound a single observation can check, a reachability goal, and a growth step +// that only two consecutive observations can see. +const fixtureSpec = ` +const rows = __sanderling__.extract((s) => s.ax.findAll({ text: "row" }).length).named("rows"); +globalThis.properties = { + fewRows: __sanderling__.always(() => rows.current < 3), + rowsAppear: __sanderling__.eventually(() => rows.current > 0).within(500, "steps"), + rowsKeepGrowing: __sanderling__.always( + __sanderling__.now(() => rows.current === 1).implies( + __sanderling__.next(() => rows.current === 2))), +}; +` + +func rowTree(t *testing.T, rows int) *hierarchy.Tree { + t.Helper() + children := make([]string, 0, rows) + for range rows { + children = append( + children, + `{"attributes": {"text": "row", "bounds": "[0,0,10,10]"}, "children": []}`, + ) + } + source := fmt.Sprintf( + `{"attributes": {"resource-id": "root", "bounds": "[0,0,100,100]"}, "children": [%s]}`, + strings.Join(children, ","), + ) + tree, err := hierarchy.Parse(source) + if err != nil { + t.Fatalf("parse tree: %v", err) + } + return tree +} + +// writeFixtureRun records a run the way internal/runner does: every step's +// hierarchy, the violations that fired at it, their witnesses, and the residual +// each property was left holding. +func writeFixtureRun(t *testing.T, directory string, rowCounts []int) { + t.Helper() + engine, err := verifier.New(verifier.WithPlatform("android")) + if err != nil { + t.Fatalf("verifier: %v", err) + } + if err := engine.Load(fixtureSpec); err != nil { + t.Fatalf("load spec: %v", err) + } + writer, err := trace.NewWriter(directory) + if err != nil { + t.Fatalf("trace writer: %v", err) + } + defer writer.Close() + + runStart := time.Date(2026, 8, 15, 12, 0, 0, 0, time.UTC) + if err := writer.WriteMeta(trace.Meta{ + Seed: 11, + SpecPath: "fixture.ts", + Platform: "android", + BundleID: "com.example.fixture", + StartedAt: runStart, + }); err != nil { + t.Fatalf("meta: %v", err) + } + + lastIndex := 0 + for position, rows := range rowCounts { + index := position + 1 + lastIndex = index + stepTime := runStart.Add(time.Duration(index) * time.Second) + tree := rowTree(t, rows) + if err := engine.PushSnapshot(verifier.SnapshotInput{ + Tree: tree, + StepTime: stepTime, + StepIndex: index, + RunStart: runStart, + }); err != nil { + t.Fatalf("push step %d: %v", index, err) + } + engine.EvaluateProperties() + violations := engine.NewlyViolatedProperties() + step := trace.Step{ + Index: index, + Timestamp: stepTime, + Hierarchy: tree, + Violations: violations, + Witnesses: fixtureWitnesses(engine, violations, index), + Residuals: fixtureResiduals(t, engine), + } + if err := writer.WriteStep(step); err != nil { + t.Fatalf("write step %d: %v", index, err) + } + } + if ended := engine.Finalize(); len(ended) > 0 { + if err := writer.WriteStep(trace.Step{ + Index: lastIndex + 1, + Timestamp: runStart.Add(time.Duration(lastIndex+1) * time.Second), + Violations: ended, + Witnesses: fixtureWitnesses(engine, ended, lastIndex+1), + }); err != nil { + t.Fatalf("write finalize step: %v", err) + } + } +} + +func fixtureWitnesses( + engine *verifier.Verifier, + properties []string, + index int, +) map[string]trace.Witness { + if len(properties) == 0 { + return nil + } + witnesses := map[string]trace.Witness{} + for _, name := range properties { + witness := engine.Witness(name) + if witness == nil { + continue + } + detected := witness.DetectedStep + if detected == 0 { + detected = index + } + witnesses[name] = trace.Witness{ + Reason: witness.Reason, + IsError: witness.IsError, + Step: witness.Step, + DetectedStep: detected, + Extractors: witness.Extractors, + } + } + return witnesses +} + +func fixtureResiduals( + t *testing.T, + engine *verifier.Verifier, +) map[string]json.RawMessage { + t.Helper() + residuals := map[string]json.RawMessage{} + for name, formula := range engine.Residuals() { + body, err := json.Marshal(formula) + if err != nil { + t.Fatalf("marshal residual %q: %v", name, err) + } + residuals[name] = body + } + return residuals +} + +func replayFixture(t *testing.T, directory string) runReport { + t.Helper() + loaded, err := loadRun(directory) + if err != nil { + t.Fatalf("load run: %v", err) + } + report, err := replay(loaded, fixtureSpec, false) + if err != nil { + t.Fatalf("replay: %v", err) + } + return report +} + +func propertyByName( + t *testing.T, + report runReport, + name string, +) propertyReport { + t.Helper() + for _, property := range report.Properties { + if property.Property == name { + return property + } + } + t.Fatalf("property %q missing from the report", name) + return propertyReport{} +} + +func TestReplayReproducesTheRecordedVerdicts(t *testing.T) { + directory := t.TempDir() + writeFixtureRun(t, directory, []int{0, 1, 1, 3}) + + report := replayFixture(t, directory) + + if !report.Valid { + t.Fatalf("replay disagreed with the run: %+v", report.Mismatches) + } + if report.ResidualMismatches != 0 { + t.Errorf("residual mismatches: %d", report.ResidualMismatches) + } + if report.StepsObserved != 4 { + t.Errorf("steps observed: got %d, want 4", report.StepsObserved) + } + + growth := propertyByName(t, report, "rowsKeepGrowing") + if !growth.Engine.Refuted || growth.Engine.Step != 3 { + t.Errorf("engine on rowsKeepGrowing: %+v", growth.Engine) + } + if growth.SingleState.Refuted { + t.Errorf( + "single-state refuted a growth step it cannot see: %+v", + growth.SingleState, + ) + } + if !growth.SingleStep.Refuted { + t.Error("single-step did not refute a one-step obligation") + } + if growth.Weakest != "single-step" { + t.Errorf("weakest oracle for rowsKeepGrowing: got %q", growth.Weakest) + } + + bound := propertyByName(t, report, "fewRows") + if !bound.SingleState.Refuted || bound.Weakest != "single-state" { + t.Errorf( + "fewRows: single-state %+v weakest %q", + bound.SingleState, + bound.Weakest, + ) + } +} + +func TestReplayReportsAViolationTheRunNeverRecorded(t *testing.T) { + directory := t.TempDir() + writeFixtureRun(t, directory, []int{0, 1, 1, 3}) + dropRecordedViolation(t, directory, "rowsKeepGrowing") + + report := replayFixture(t, directory) + + if report.Valid { + t.Fatal("a trace missing a recorded violation must not replay as valid") + } + var found bool + for _, entry := range report.Mismatches { + if entry.Property == "rowsKeepGrowing" && entry.Field == "violated" { + found = true + } + } + if !found { + t.Errorf( + "no mismatch named the dropped violation: %+v", + report.Mismatches, + ) + } +} + +func TestReplayReportsAResidualTheRunNeverHeld(t *testing.T) { + directory := t.TempDir() + writeFixtureRun(t, directory, []int{0, 1, 1, 3}) + rewriteResidual(t, directory, 1, "fewRows", `{"op":"false"}`) + + report := replayFixture(t, directory) + + if report.Valid { + t.Fatal( + "a trace whose recorded residual differs must not replay as valid", + ) + } + if report.ResidualMismatches != 1 { + t.Errorf( + "residual mismatches: got %d, want 1", + report.ResidualMismatches, + ) + } +} + +// dropRecordedViolation removes one property from every step's violations, +// which is what a trace that failed to record a verdict looks like. +func dropRecordedViolation(t *testing.T, directory, property string) { + t.Helper() + rewriteSteps(t, directory, func(step *trace.Step) { + kept := step.Violations[:0] + for _, name := range step.Violations { + if name != property { + kept = append(kept, name) + } + } + step.Violations = kept + delete(step.Witnesses, property) + }) +} + +func rewriteResidual( + t *testing.T, + directory string, + index int, + property, residual string, +) { + t.Helper() + rewriteSteps(t, directory, func(step *trace.Step) { + if step.Index == index { + step.Residuals[property] = json.RawMessage(residual) + } + }) +} + +func rewriteSteps(t *testing.T, directory string, edit func(*trace.Step)) { + t.Helper() + path := filepath.Join(directory, "trace.jsonl") + body, err := os.ReadFile(path) + if err != nil { + t.Fatalf("read trace: %v", err) + } + var rewritten strings.Builder + for _, line := range strings.Split(strings.TrimSpace(string(body)), "\n") { + var step trace.Step + if err := json.Unmarshal([]byte(line), &step); err != nil { + t.Fatalf("decode step: %v", err) + } + edit(&step) + encoded, err := json.Marshal(step) + if err != nil { + t.Fatalf("encode step: %v", err) + } + rewritten.Write(encoded) + rewritten.WriteByte('\n') + } + if err := os.WriteFile(path, []byte(rewritten.String()), 0o644); err != nil { + t.Fatalf("write trace: %v", err) + } +} + +func TestCrashOnlyFiresOnAnErrorSurfaceAndOnLeavingTheForeground(t *testing.T) { + run := loadedRun{Steps: []trace.Step{ + {Index: 1, Logs: []trace.LogEntry{{Level: "E", Message: "noisy"}}}, + {Index: 2, ActionSkipped: foregroundLossReason}, + {Index: 3, Exceptions: []trace.Exception{{Class: "TypeError"}}}, + }} + + report := crashOnly(run) + + if !report.Fired || report.FirstStep != 2 { + t.Errorf("crash-only: %+v", report) + } + if len(report.ExceptionSteps) != 1 || report.ExceptionSteps[0] != 3 { + t.Errorf("exception steps: %v", report.ExceptionSteps) + } + if len(report.ErrorLogSteps) != 1 || report.ErrorLogSteps[0] != 1 { + t.Errorf("error log steps: %v", report.ErrorLogSteps) + } +} + +func TestCrashOnlyIgnoresAnErrorLogOnItsOwn(t *testing.T) { + run := loadedRun{ + Steps: []trace.Step{{Index: 1, Logs: []trace.LogEntry{{Level: "E"}}}}, + } + + if crashOnly(run).Fired { + t.Error("an error-level log line is not a crash") + } +} + +// A reachability goal the run reaches at the fourth observation is clean under +// the window its author wrote and refuted by the same window shortened to two +// observations. Reporting that shortened refutation would convict every clean +// trace, so the single-step column has to admit it cannot state the property. +func TestSingleStepDoesNotConvictACleanTraceOfATruncatedWindow(t *testing.T) { + directory := t.TempDir() + writeFixtureRun(t, directory, []int{0, 0, 0, 1}) + + report := replayFixture(t, directory) + + if !report.Valid { + t.Fatalf("replay disagreed with the run: %+v", report.Mismatches) + } + appear := propertyByName(t, report, "rowsAppear") + if appear.Engine.Refuted { + t.Fatalf( + "the trace reaches the goal inside the 500-step window: %+v", + appear.Engine, + ) + } + if appear.SingleStep.Refuted { + t.Errorf( + "single-step refuted a clean trace by shortening the window: %+v", + appear.SingleStep, + ) + } + if !appear.SingleStep.CannotExpress { + t.Error( + "single-step must record a window it cannot state as inexpressible", + ) + } + if !appear.SingleStepTruncatesWindow { + t.Error("the truncated-window marker must stay visible on the property") + } +} + +func TestSingleStateAdmitsWhatOneObservationCannotState(t *testing.T) { + directory := t.TempDir() + writeFixtureRun(t, directory, []int{0, 1, 1, 3}) + + report := replayFixture(t, directory) + + growth := propertyByName(t, report, "rowsKeepGrowing") + if !growth.SingleState.CannotExpress { + t.Errorf( + "single-state kept a next obligation it erases to nothing: %+v", + growth.SingleState, + ) + } + appear := propertyByName(t, report, "rowsAppear") + if !appear.SingleState.CannotExpress { + t.Errorf( + "single-state kept a reachability goal it erases to nothing: %+v", + appear.SingleState, + ) + } + bound := propertyByName(t, report, "fewRows") + if bound.SingleState.CannotExpress { + t.Error("single-state states a bound read at one observation") + } + if !bound.SingleState.Refuted || bound.Weakest != "single-state" { + t.Errorf( + "fewRows: single-state %+v weakest %q", + bound.SingleState, + bound.Weakest, + ) + } +} diff --git a/cmd/internal-tools/oracle-reduction/reduce.go b/cmd/internal-tools/oracle-reduction/reduce.go new file mode 100644 index 0000000..6c61b4b --- /dev/null +++ b/cmd/internal-tools/oracle-reduction/reduce.go @@ -0,0 +1,281 @@ +package main + +import ( + "fmt" + "time" + + "github.com/priyanshujain/sanderling/internal/ltl" +) + +// tripleWindow is the horizon a property triple has: an obligation armed at one +// observation must discharge at the next, and nothing outlives that. +const tripleWindow = 2 + +// singleStateFormula is what a checker holding one observation can refute. +// Every operator that defers or repeats an obligation is replaced by the +// constant that makes the formula around it trivially satisfied, so the only +// refutation left is a predicate read at a single observation. The outermost +// always survives because it is what says "check this at each observation", +// which costs no history. +func singleStateFormula(formula ltl.Formula) ltl.Formula { + if always, ok := formula.(ltl.AlwaysFormula); ok { + always.Inner = stateless(always.Inner, true) + return always + } + return stateless(formula, true) +} + +// singleStepFormula is the property triple: one step of history, and no +// obligation surviving past the next observation. A next keeps its one-step +// deferral, and an eventually of any window shrinks to the two observations a +// triple spans. +func singleStepFormula(formula ltl.Formula) ltl.Formula { + if always, ok := formula.(ltl.AlwaysFormula); ok { + always.Inner = oneStep(always.Inner, true) + return always + } + return oneStep(formula, true) +} + +// singleStateExpresses and singleStepExpresses decide, from the property's form +// alone, whether the reduced oracle can still state the property after its +// rewrite. An oracle that cannot state a property does not get to refute it, +// and is reported as silent on it rather than as either verdict. +// +// Two shapes defeat a reduction. The rewrite shortens an obligation window the +// oracle's horizon cannot hold, leaving it to refute a property strictly +// stronger than the one the author wrote. Or the rewrite leaves a formula whose +// verdict no longer depends on the trace, leaving it to report the same answer +// everywhere. Either way the column would carry a verdict about a property +// nobody wrote, which is worth less than an admission that the oracle is out of +// its depth. +func singleStateExpresses(formula ltl.Formula) bool { + return dependsOnTrace(singleStateFormula(formula)) +} + +func singleStepExpresses(formula ltl.Formula) bool { + return !truncatesWindow(formula) && + dependsOnTrace(singleStepFormula(formula)) +} + +// truncatesWindow reports whether the single-step rewrite had to shorten a +// window to fit a triple. Where it did, the reduced oracle is checking a +// stronger property than the author wrote, so a refutation of it is not the +// same event as a refutation of the property. +func truncatesWindow(formula ltl.Formula) bool { + if always, ok := formula.(ltl.AlwaysFormula); ok { + return shortensWindow(always.Inner, true) + } + return shortensWindow(formula, true) +} + +// shortensWindow walks the same shape oneStep rewrites, and reports only the +// shortening that strengthens the formula. Polarity is what separates the two: +// a shorter window under an even number of negations demands the same thing +// sooner, so a refutation of it need not be a refutation of the property, while +// under an odd number it asks for less and its refutations stay sound. The +// operators oneStep erases rather than shortens are erased to the constant its +// position is satisfied by, which also only asks for less. +func shortensWindow(formula ltl.Formula, positive bool) bool { + switch concrete := formula.(type) { + case ltl.EventuallyFormula: + return positive && windowOutlastsTriple(concrete) + case ltl.NowFormula: + return shortensWindow(concrete.Inner, positive) + case ltl.NotFormula: + return shortensWindow(concrete.Inner, !positive) + case ltl.AndFormula: + return shortensWindow(concrete.Left, positive) || shortensWindow(concrete.Right, positive) + case ltl.OrFormula: + return shortensWindow(concrete.Left, positive) || shortensWindow(concrete.Right, positive) + case ltl.ImpliesFormula: + return shortensWindow(concrete.Antecedent, !positive) || shortensWindow(concrete.Consequent, positive) + default: + return false + } +} + +// windowOutlastsTriple asks whether an obligation can still be open after the +// two observations a triple spans. A window counted in time is outside what a +// triple can state whatever its length, because a triple has no clock: it can +// say "at the next observation" and nothing about when that arrives. +func windowOutlastsTriple(formula ltl.EventuallyFormula) bool { + if formula.HasStepBound { + return formula.StepBound > tripleWindow + } + return true +} + +// dependsOnTrace reports whether a rewritten formula can still read the trace. +// Constants fold through the connectives, and one that folds away to a constant +// answers the same on every trace: silence that reads as "did not refute", or a +// refutation of everything. Neither is a verdict about the run. +func dependsOnTrace(formula ltl.Formula) bool { + _, constant := fold(formula).(ltl.PureFormula) + return !constant +} + +// fold propagates the constants the rewrites substituted for erased operators. +// An obligation whose inner formula folded to false keeps its shape, because a +// deferred false is a refutation still owed; only the side that can no longer +// fail folds away. +func fold(formula ltl.Formula) ltl.Formula { + switch concrete := formula.(type) { + case ltl.AlwaysFormula: + concrete.Inner = fold(concrete.Inner) + if pure, ok := concrete.Inner.(ltl.PureFormula); ok { + return pure + } + return concrete + case ltl.EventuallyFormula: + concrete.Inner = fold(concrete.Inner) + if isPure(concrete.Inner, true) { + return ltl.Pure(true) + } + return concrete + case ltl.NextFormula: + inner := fold(concrete.Inner) + if isPure(inner, true) { + return ltl.Pure(true) + } + return ltl.Next(inner) + case ltl.NowFormula: + inner := fold(concrete.Inner) + if _, ok := inner.(ltl.PureFormula); ok { + return inner + } + return ltl.Now(inner) + case ltl.NotFormula: + inner := fold(concrete.Inner) + if pure, ok := inner.(ltl.PureFormula); ok { + return ltl.Pure(!pure.Value) + } + return ltl.Not(inner) + case ltl.AndFormula: + left, right := fold(concrete.Left), fold(concrete.Right) + switch { + case isPure(left, false) || isPure(right, false): + return ltl.Pure(false) + case isPure(left, true): + return right + case isPure(right, true): + return left + } + return ltl.And(left, right) + case ltl.OrFormula: + left, right := fold(concrete.Left), fold(concrete.Right) + switch { + case isPure(left, true) || isPure(right, true): + return ltl.Pure(true) + case isPure(left, false): + return right + case isPure(right, false): + return left + } + return ltl.Or(left, right) + case ltl.ImpliesFormula: + antecedent, consequent := fold(concrete.Antecedent), fold(concrete.Consequent) + switch { + case isPure(antecedent, false) || isPure(consequent, true): + return ltl.Pure(true) + case isPure(antecedent, true): + return consequent + } + return ltl.Implies(antecedent, consequent) + default: + return formula + } +} + +func isPure(formula ltl.Formula, value bool) bool { + pure, ok := formula.(ltl.PureFormula) + return ok && pure.Value == value +} + +// stateless erases every temporal operator. The replacement constant follows +// the position's polarity: under an even number of negations a temporal +// sub-formula is dropped as satisfied, and under an odd number as failed, so +// that in both cases its negation cannot refute anything either. +func stateless(formula ltl.Formula, positive bool) ltl.Formula { + switch concrete := formula.(type) { + case ltl.AlwaysFormula, ltl.NextFormula, ltl.EventuallyFormula: + return ltl.Pure(positive) + case ltl.NowFormula: + return ltl.Now(stateless(concrete.Inner, positive)) + case ltl.NotFormula: + return ltl.Not(stateless(concrete.Inner, !positive)) + case ltl.AndFormula: + return ltl.And(stateless(concrete.Left, positive), stateless(concrete.Right, positive)) + case ltl.OrFormula: + return ltl.Or(stateless(concrete.Left, positive), stateless(concrete.Right, positive)) + case ltl.ImpliesFormula: + return ltl.Implies( + stateless(concrete.Antecedent, !positive), + stateless(concrete.Consequent, positive), + ) + default: + return formula + } +} + +func oneStep(formula ltl.Formula, positive bool) ltl.Formula { + switch concrete := formula.(type) { + case ltl.AlwaysFormula: + return ltl.Pure(positive) + case ltl.NextFormula: + return ltl.Next(stateless(concrete.Inner, positive)) + case ltl.EventuallyFormula: + return ltl.EventuallyWithinSteps(stateless(concrete.Inner, positive), tripleWindow) + case ltl.NowFormula: + return ltl.Now(oneStep(concrete.Inner, positive)) + case ltl.NotFormula: + return ltl.Not(oneStep(concrete.Inner, !positive)) + case ltl.AndFormula: + return ltl.And(oneStep(concrete.Left, positive), oneStep(concrete.Right, positive)) + case ltl.OrFormula: + return ltl.Or(oneStep(concrete.Left, positive), oneStep(concrete.Right, positive)) + case ltl.ImpliesFormula: + return ltl.Implies( + oneStep(concrete.Antecedent, !positive), + oneStep(concrete.Consequent, positive), + ) + default: + return formula + } +} + +// propertyClass splits safety from liveness by the property's top-level form: +// a reachability goal is liveness, everything else is a safety obligation +// re-asserted at each observation. +func propertyClass(formula ltl.Formula) string { + if _, ok := formula.(ltl.EventuallyFormula); ok { + return "liveness" + } + return "safety" +} + +func topLevelForm(formula ltl.Formula) string { + switch concrete := formula.(type) { + case ltl.AlwaysFormula: + return "always" + boundSuffix(concrete.HasStepBound, concrete.StepBound, concrete.Duration) + case ltl.EventuallyFormula: + return "eventually" + boundSuffix(concrete.HasStepBound, concrete.StepBound, concrete.Duration) + default: + return "predicate" + } +} + +func boundSuffix( + hasStepBound bool, + stepBound int, + duration time.Duration, +) string { + switch { + case hasStepBound: + return fmt.Sprintf(" within %d steps", stepBound) + case duration > 0: + return fmt.Sprintf(" within %s", duration) + default: + return "" + } +} diff --git a/cmd/internal-tools/oracle-reduction/reduce_test.go b/cmd/internal-tools/oracle-reduction/reduce_test.go new file mode 100644 index 0000000..6216e30 --- /dev/null +++ b/cmd/internal-tools/oracle-reduction/reduce_test.go @@ -0,0 +1,222 @@ +package main + +import ( + "testing" + "time" + + "github.com/priyanshujain/sanderling/internal/ltl" +) + +// observe drives an evaluator over a fixed sequence of predicate readings and +// returns the observation at which it latched, or 0 if it never did. +func observe(formula ltl.Formula, steps int) int { + evaluator := ltl.NewEvaluator(formula) + base := time.Unix(0, 0) + for step := 1; step <= steps; step++ { + if evaluator.ObserveAtStep( + base.Add(time.Duration(step)*time.Second), + step, + ) == ltl.VerdictViolated { + return step + } + } + if evaluator.Finalize() == ltl.VerdictViolated { + return steps + 1 + } + return 0 +} + +func constant(value bool) ltl.Formula { + return ltl.ThunkNamed("p", func() (bool, error) { return value, nil }) +} + +func TestSingleStateHoldsWhereRefutationNeedsTheNextObservation(t *testing.T) { + property := ltl.Always( + ltl.Implies(ltl.Now(constant(true)), ltl.Next(constant(false))), + ) + + if engine := observe(property, 4); engine == 0 { + t.Fatal( + "the engine was expected to refute a next obligation that never held", + ) + } + if reduced := observe(singleStateFormula(property), 4); reduced != 0 { + t.Errorf( + "single-state refuted at observation %d, and one observation cannot see a next", + reduced, + ) + } + if reduced := observe(singleStepFormula(property), 4); reduced == 0 { + t.Error("single-step was expected to refute a one-step obligation") + } +} + +func TestSingleStateRefutesAPredicateReadAtOneObservation(t *testing.T) { + property := ltl.Always(constant(false)) + + if reduced := observe(singleStateFormula(property), 3); reduced != 1 { + t.Errorf( + "single-state latched at %d, want the first observation", + reduced, + ) + } +} + +func TestSingleStateKeepsANegatedTemporalHarmless(t *testing.T) { + property := ltl.Always(ltl.Not(ltl.Eventually(constant(false)))) + + if reduced := observe(singleStateFormula(property), 3); reduced != 0 { + t.Errorf( + "single-state refuted at observation %d; erasing a negated eventually must not manufacture a violation", + reduced, + ) + } +} + +func TestSingleStepShrinksAReachabilityGoalToTwoObservations(t *testing.T) { + property := ltl.EventuallyWithinSteps(constant(false), 500) + + if engine := observe(property, 4); engine != 5 { + t.Fatalf( + "a 500-step window closes only at run end, latched at %d", + engine, + ) + } + if reduced := observe(singleStepFormula(property), 4); reduced != 2 { + t.Errorf( + "single-step latched at %d, want the second observation", + reduced, + ) + } + if !truncatesWindow(property) { + t.Error( + "a 500-step window shortened to two observations must be reported as truncated", + ) + } +} + +// sequence returns a predicate that reads the given values, one per call, so +// each evaluator gets its own reading counter. +func sequence(readings []bool) ltl.Formula { + position := 0 + return ltl.ThunkNamed("p", func() (bool, error) { + value := readings[position] + position++ + return value, nil + }) +} + +func TestSingleStepConvictsAGoalTheEngineSeesReached(t *testing.T) { + readings := []bool{false, false, true, true} + + if engine := observe(ltl.EventuallyWithinSteps(sequence(readings), 4), 4); engine != 0 { + t.Fatalf( + "the engine latched at %d, and the goal is reached inside its window", + engine, + ) + } + if reduced := observe(singleStepFormula(ltl.EventuallyWithinSteps(sequence(readings), 4)), 4); reduced != 2 { + t.Errorf( + "single-step latched at %d; an obligation armed at the first observation must not reach the third", + reduced, + ) + } +} + +func TestTruncatesWindowIgnoresAnObligationThatAlreadyFits(t *testing.T) { + property := ltl.Always( + ltl.Implies(ltl.Now(constant(true)), ltl.Next(constant(true))), + ) + + if truncatesWindow(property) { + t.Error("a next spans two observations already and is not truncated") + } +} + +func TestPropertyClassAndFormComeFromTheTopLevel(t *testing.T) { + safety := ltl.Always(constant(true)) + liveness := ltl.EventuallyWithinSteps(constant(true), 575) + + if got := propertyClass(safety); got != "safety" { + t.Errorf("class of an always: got %q", got) + } + if got := propertyClass(liveness); got != "liveness" { + t.Errorf("class of an eventually: got %q", got) + } + if got := topLevelForm(liveness); got != "eventually within 575 steps" { + t.Errorf("form: got %q", got) + } + if got := topLevelForm(ltl.EventuallyWithin(constant(true), 3*time.Second)); got != "eventually within 3s" { + t.Errorf("form: got %q", got) + } +} + +func TestSingleStepCannotExpressAWindowLongerThanATriple(t *testing.T) { + for _, testCase := range []struct { + name string + property ltl.Formula + expresses bool + }{ + {"reachability goal in steps", ltl.EventuallyWithinSteps(constant(true), 575), false}, + {"reachability goal in time", ltl.EventuallyWithin(constant(true), 3*time.Second), false}, + {"unbounded reachability goal", ltl.Eventually(constant(true)), false}, + {"window a triple spans exactly", ltl.EventuallyWithinSteps(constant(true), tripleWindow), true}, + {"deadline nested under an always", ltl.Always(ltl.Implies( + ltl.Now(constant(true)), ltl.EventuallyWithin(constant(true), 3*time.Second))), false}, + {"one-step obligation under an always", ltl.Always(ltl.Implies( + ltl.Now(constant(true)), ltl.Next(constant(true)))), true}, + {"predicate under an always", ltl.Always(constant(true)), true}, + } { + t.Run(testCase.name, func(t *testing.T) { + if singleStepExpresses(testCase.property) != testCase.expresses { + t.Errorf("single-step expresses %s: got %t, want %t", + testCase.name, !testCase.expresses, testCase.expresses) + } + }) + } +} + +// A shorter window under a negation asks for less rather than more, so the +// triple's refutations of it stay sound and the property stays expressible. +// Reporting it as inexpressible would push a defect the single-step oracle can +// genuinely catch into the temporal-only column. +func TestSingleStepStillExpressesANegatedWindow(t *testing.T) { + property := ltl.Always( + ltl.Not(ltl.EventuallyWithinSteps(constant(false), 575)), + ) + + if !singleStepExpresses(property) { + t.Error( + "a window shortened under a negation is weakened, not strengthened", + ) + } + if truncatesWindow(property) { + t.Error( + "the truncation marker must not fire where shortening only weakens", + ) + } +} + +func TestSingleStateCannotExpressWhatItsRewriteEmpties(t *testing.T) { + for _, testCase := range []struct { + name string + property ltl.Formula + expresses bool + }{ + {"predicate at one observation", ltl.Always(constant(true)), true}, + {"reachability goal", ltl.EventuallyWithinSteps(constant(true), 575), false}, + {"next obligation under an always", ltl.Always(ltl.Implies( + ltl.Now(constant(true)), ltl.Next(constant(true)))), false}, + {"deadline under an always", ltl.Always(ltl.Implies( + ltl.Now(constant(true)), ltl.EventuallyWithin(constant(true), 3*time.Second))), false}, + {"negated eventually under an always", ltl.Always(ltl.Not(ltl.Eventually(constant(false)))), false}, + {"predicate conjoined with a next", ltl.Always(ltl.And(constant(true), ltl.Next(constant(true)))), true}, + } { + t.Run(testCase.name, func(t *testing.T) { + if singleStateExpresses(testCase.property) != testCase.expresses { + t.Errorf("single-state expresses %s: got %t, want %t", + testCase.name, !testCase.expresses, testCase.expresses) + } + }) + } +}