From 7ae2fc95d2ee7e30c973328142b5d9ae5c449114 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 09:40:40 -0400 Subject: [PATCH] Check native total and partial Aeneas specifications Keep independent native examples for successful returns, named assumptions and tuple results. Total contracts reject panic and divergence; partial contracts admit divergence while rejecting panic and incorrect successful returns. Validation: fresh pinned extraction and complete-model golden comparison; independent golden/live Lean builds, required-contract checks, and the transitive axiom audit. gherrit-pr-id: Gmasez6fvx2c6chogoybuzpgyoykiaupc 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