From d92dd1633d2eb4abe31ab3490cf2ace056bf6377 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 09:40:40 -0400 Subject: [PATCH] Test total and partial Aeneas contract semantics Pin the execution guarantees independently of the specification macro. Add kernel-checked examples for successful returns, named assumptions, tuple results, generic modeling providers and dependent ghosts. Total contracts reject panic and divergence even with postcondition True. Partial contracts permit divergence but reject panic, wrong successful results and decoder-rejected outputs. Keep Rust None and Err payloads distinct from decoding rejection and execution failure. gherrit-pr-id: Gmokoduvrhwmesqj7moerqxqv6jjz63e5 Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/lean/ContractTests.lean | 111 ++++++++++++++++++++ 1 file changed, 111 insertions(+) create mode 100644 verification/aeneas/lean/ContractTests.lean diff --git a/verification/aeneas/lean/ContractTests.lean b/verification/aeneas/lean/ContractTests.lean new file mode 100644 index 0000000000..83fc943d03 --- /dev/null +++ b/verification/aeneas/lean/ContractTests.lean @@ -0,0 +1,111 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import ModelPrelude +@[expose] public section + +/-! +These kernel-checked examples explain Aeneas's native total and partial +contracts independently of our spec macro. They pin successful results, tuple +postconditions, panic rejection, and divergence behavior. The independently +written theorem types prevent a change in syntax from silently changing the +claim. Total contracts require successful execution even for a True +postcondition. Partial contracts may diverge, but still reject panic. +-/ +open Aeneas Aeneas.Std AeneasSpecs +namespace ContractTests + +-- Omitted requirements mean True; a successful result is still required. +theorem identity_spec (x : Nat) : + Result.ok x + ⦃ ret => ret = x ⦄ := by + exact WP.spec.ret rfl + +-- Named requirements are available without introductions in the proof body. +theorem transitive_spec (x y z : Nat) + (hxy : x = y) + (hyz : y = z) : + Result.ok x + ⦃ ret => ret = z ⦄ := by + exact WP.spec.ret (hxy.trans hyz) + +-- Reuse Aeneas's tuple-aware binders for returns and mutable post-states. +theorem tuple_spec (x : Nat) : + Result.ok (x, x + 1) + ⦃ ret x' => ret = x ∧ x' = x + 1 ⦄ := by + simp + +theorem diverging_spec : + (Result.div : Result Nat) + ⦃ _ => False ⦄div := by + exact WP.dspec.div _ + +theorem partial_identity_spec (x : Nat) : + Result.ok x + ⦃ ret => ret = x ⦄div := by + exact WP.dspec.ret rfl + +-- These independently written types pin the exported theorem types and outcomes. +example : ∀ x : Nat, WP.spec (Result.ok x) (fun ret => ret = x) := identity_spec +example : ∀ x y z : Nat, x = y → y = z → + WP.spec (Result.ok x) (fun ret => ret = z) := transitive_spec +example : ∀ x : Nat, WP.spec (Result.ok (x, x + 1)) + (fun (ret, x') => ret = x ∧ x' = x + 1) := tuple_spec +example : WP.dspec (Result.div : Result Nat) (fun _ => False) := diverging_spec +example : ∀ x : Nat, WP.dspec (Result.ok x) (fun ret => ret = x) := partial_identity_spec + +theorem panic_rejected : + ¬ WP.spec (Result.fail Error.panic : Result Nat) (fun _ => True) := by simp + +theorem divergence_rejected : + ¬ WP.spec (Result.div : Result Nat) (fun _ => True) := by simp + +-- Partial correctness must reject panic and incorrect successful returns too. +theorem partial_panic_rejected : + ¬ WP.dspec (Result.fail Error.panic : Result Nat) (fun _ => True) := by simp + +theorem partial_wrong_return_rejected : + ¬ WP.dspec (Result.ok 0) (fun ret : Nat => ret = 1) := by simp + +-- A generic identity shares one explicit dictionary and the same witness on +-- input and output, even when the dictionary rejects some representations. +theorem modeled_identity {Raw : Type} (provider : RustModel Raw) (raw : Raw) + (value : provider.Model) (h : provider.decode raw = some value) : + WP.spec (Result.ok raw) (fun out => + ∃ decoded, provider.decode out = some decoded ∧ decoded = value) := + WP.spec.ret ⟨value, h, rfl⟩ + +-- A dependent ghost retains its exact domain in mathematical input scope. +theorem modeled_position {Raw : Type} (provider : RustModel Raw) + (length : provider.Model → Nat) (raw : Raw) (value : provider.Model) + (h : provider.decode raw = some value) (position : Fin (length value)) : + WP.spec (Result.ok raw) (fun out => + ∃ decoded, provider.decode out = some decoded ∧ position.val < length decoded) := + WP.spec.ret ⟨value, h, position.isLt⟩ + +-- An accepted execution cannot return a decoder-rejected representation, even +-- when its authored postcondition contributes no information. +theorem rejected_output_rejected {Raw : Type} (provider : RustModel Raw) + (raw : Raw) (h : provider.decode raw = none) : + ¬ WP.spec (Result.ok raw) (fun out => + ∃ decoded, provider.decode out = some decoded ∧ True) := by + simp [WP.spec_ok, h] + +theorem partial_rejected_output_rejected {Raw : Type} (provider : RustModel Raw) + (raw : Raw) (h : provider.decode raw = none) : + ¬ WP.dspec (Result.ok raw) (fun out => + ∃ decoded, provider.decode out = some decoded ∧ True) := by + simp [h] + +-- Rust absence and Rust errors remain successful decoded constructor cases. +example : (@modelOption Usize (modelUScalar .Usize)).decode none = some none := rfl +example : (@modelRustResult Usize Unit (modelUScalar .Usize) modelUnit).decode + (.Err ()) = some (.Err ()) := rfl + +end ContractTests