Golden Files

Golden files store expected verification outputs for regression testing. When you run tests, actual outputs are compared against these reference files to detect unintended changes.

What Are Golden Files?

Golden files are reference outputs stored in ok/ subdirectories alongside test sources. Each test can produce multiple golden files capturing different aspects of the verification pipeline:

Extension	Content	Purpose
.vpr	Generated Viper code	Captures the translation from Sector9 source to Viper IR
.vpr.stderr	Translator diagnostics	Warnings and errors from the translation phase
.silicon	Verification result (JSON)	Structured output from the SMT solver
.silicon.ret	Return code	Exit status indicating verification success/failure

Directory Structure

Golden files live in ok/ directories parallel to test sources:

test/viper/level1/
├── arithmetic_add_sat.mo        # Source test file
├── array_bounds_unsat.mo        # Another test
└── ok/                          # Golden directory
    ├── arithmetic_add_sat.vpr           # Generated Viper code
    ├── arithmetic_add_sat.vpr.stderr    # Translation output
    ├── arithmetic_add_sat.silicon       # Verification result
    ├── arithmetic_add_sat.silicon.ret   # Return code
    ├── array_bounds_unsat.vpr
    ├── array_bounds_unsat.vpr.stderr
    ├── array_bounds_unsat.silicon
    └── array_bounds_unsat.silicon.ret

Each test file generates up to four golden files in the corresponding ok/ directory.

Golden File Contents

.vpr - Viper Code

The generated Viper intermediate representation. This captures how Sector9 contracts translate to the verification backend:

import "/tmp/sector9/sector9/prelude.vpr"

method add($Self: Ref, a: Int, b: Int) returns ($Res: Int)
     requires true
     requires $Inv($Self)
     ensures (true && (($Res == (a + b)) && $Inv($Self)))
     {
       $Res := (a + b);
       goto $Ret;
       label $Ret;
       $expire_borrows(2);
     }

define $Inv($Self) (true)

.silicon - Verification Result

JSON-formatted verification output from the Silicon SMT solver:

{
  "schema_version": "2",
  "status": "VALID",
  "failures": [],
  "warnings": [],
  "silicon": {
    "exitCode": 0,
    "stdout": "Silicon finished verification successfully in ?s.\n",
    "stderr": ""
  }
}

For failing tests (_unsat), the status field usually shows "INVALID" and failures contains the failing obligation. Counterexample data appears only when model extraction is requested and the backend can produce a model; see counterexamples.

.silicon.ret - Return Code

A single line indicating the verification exit status:

Return code 0

Exit code 0 means verification succeeded; non-zero indicates failure.

Match Status Indicators

When running tests, the runner reports golden file status using these indicators:

Indicator	Meaning	Action
[m]	Match	Golden file matches actual output
[!]	Mismatch	Output differs from golden (regression or intended change)
[ ]	Missing	No golden file exists yet

Example test output:

=== level1 ===
✅ [m] arithmetic_add_sat.mo - verified OK
✅ [m] array_bounds_unsat.mo - postcondition might not hold
❌ [!] changed_test_sat.mo - verified OK
✅ [ ] new_test_sat.mo - verified OK

The semantic indicator (✅/❌) shows whether the test behaves as expected based on its filename suffix. The golden indicator ([m]/[!]/[ ]) shows whether outputs match stored references.

Updating Golden Files

Using update_goldens.sh

To accept new outputs as the expected reference, use the update_goldens.sh script:

# Update goldens for a specific test
./update_goldens.sh test/viper/level1/arithmetic_add_sat.mo

# The script:
# 1. Rebuilds sector9 through nix develop
# 2. Runs the relevant test runner with -a (accept) flag
# 3. Copies actual outputs to ok/ directory

Using test-viper.sh Directly

For batch updates or specific directories:

# Update all goldens in a directory from that directory
cd test/viper/level1
../../run.sh -a -v *.mo

# Or use the Viper test runner
./test-viper.sh -a

Run ./test-viper.sh -a from the repository root. It sweeps test/viper rather than a single directory, skips // SLOW tests unless --slow is passed, and uses the expected outcome encoded in the test filename. The Viper runner invokes the compiler with --json and --verify-vpr-out, so the .vpr, .vpr.stderr, .silicon, and .silicon.ret files all describe the same translation and backend verification run.

When to Update Goldens

Update golden files when:

• Intentional translation changes: You modified the Viper translator and outputs changed as expected
• New tests: You added tests that need initial golden files
• Bug fixes: A fix changes output in a correct way

Do not blindly accept changes. Always review diffs to ensure changes are intentional:

# See what changed
diff test/viper/level1/ok/test_sat.vpr /tmp/actual_output.vpr

Workflow Example

Adding a New Test

1. Create the test file:

// test/viper/level1/my_new_test_sat.mo
persistent actor {
  public func double(n : Nat) : async Nat
    ensures result == n * 2;
  {
    n * 2
  };
}

2. Run the test (will show missing goldens):

./test-viper.sh
# Output: ✅ [ ] my_new_test_sat.mo - verified OK

3. Accept the golden files:

./update_goldens.sh test/viper/level1/my_new_test_sat.mo

4. Verify goldens were created:

ls test/viper/level1/ok/my_new_test_sat.*
# my_new_test_sat.vpr
# my_new_test_sat.vpr.stderr
# my_new_test_sat.silicon
# my_new_test_sat.silicon.ret

Investigating a Mismatch

When you see [!] indicating a mismatch:

1. Check if the change is expected based on your modifications
2. Compare the actual vs expected output:

# Run test and keep output from the test directory
cd test/viper/level1
../../run.sh -v my_test_sat.mo
diff ok/my_test_sat.vpr _out/my_test_sat.vpr

3. If the change is correct, accept it:

./update_goldens.sh test/viper/level1/my_test_sat.mo

4. If the change is unexpected, investigate and fix the regression

Output Normalization

Golden files are normalized to reduce reproducible-output noise across different environments. The shared runner removes or standardizes values such as:

• Memory addresses (wasm:0x... → wasm:0x___)
• Compiler version strings and source paths
• Canister IDs
• Timestamps and timing information
• Stack traces from exceptions

This normalization happens automatically during test execution.

Deterministic Mode

For reliable golden file testing, Sector9 uses --deterministic mode, which ensures:

• Consistent identifier generation using content hashes
• Alphabetically sorted declarations
• Reproducible Viper output across runs

Verification automatically enables deterministic mode. For manual Viper generation:

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --viper --deterministic file.mo > output.vpr

See deterministic mode for when to request deterministic output manually.

Summary

• Golden files in ok/ directories store expected verification outputs
• Four file types: .vpr, .vpr.stderr, .silicon, .silicon.ret
• Match indicators: [m] match, [!] mismatch, [ ] missing
• Use update_goldens.sh to accept new outputs as reference
• Always review changes before accepting to catch unintended regressions
• Output normalization ensures reproducible comparisons