Skip to content

Prove concrete owned standard transmutation #3877

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
joshlf wants to merge 1 commit into
base: G4s3r4gpuxvvnoxoizjjgoy3b2rwmgi7g
Choose a base branch
from
Open

Prove concrete owned standard transmutation #3877

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 37 additions & 5 deletions verification/aeneas/admission.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ def __init__(self, data, registry, law_traits=()):
if options[key] != expected:
raise ValueError(f'Unreviewed extraction option {key}: {options[key]!r}')
stages = {variant(f['body'])[0] for f in self.functions.values()
if f['body'] != 'Opaque'}
if f['body'] != 'Opaque' and variant(f['body'])[0] != 'Intrinsic'}
Comment on lines 119 to +120

@gemini-code-assist gemini-code-assist Bot Oct 15, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

medium

The variant(f['body'])[0] expression is evaluated twice for each function in the set comprehension. We can optimize this and improve readability by using a standard loop to build the set.

Suggested change
stages = {variant(f['body'])[0] for f in self.functions.values()
if f['body'] != 'Opaque'}
if f['body'] != 'Opaque' and variant(f['body'])[0] != 'Intrinsic'}
stages = set()
for f in self.functions.values():
if f['body'] != 'Opaque':
stage, _ = variant(f['body'])
if stage != 'Intrinsic':
stages.add(stage)

if len(stages) != 1 or not stages <= {'Unstructured', 'Structured'}:
raise ValueError('Missing or mixed admission body stages')
self.before = stages == {'Unstructured'}
Expand Down Expand Up @@ -263,6 +263,10 @@ def visit(self, index):
continue
if kind == 'Builtin':
tag, _ = variant(detail)
if tag == 'RustcIntrinsic' and name == 'core::intrinsics::transmute':
if function['body'] != {'Intrinsic': {'name': 'transmute', 'arg_names': ['src']}}:
raise ValueError('Standard transmute intrinsic body changed')
continue
if tag in {'Inline', 'TrackCaller'}:
continue
elif kind == 'Unknown':
Expand All @@ -279,6 +283,17 @@ def visit(self, index):
if matches:
if len(matches) != 1:
raise ValueError(f'External interpretation signature changed: {name}')
if name == 'core::intrinsics::transmute':
expected_providers = {
'u32->[u8;4]': 'Zerocopy.stdTransmuteU32ToBytes',
'[u8;4]->u32': 'Zerocopy.stdTransmuteBytesToU32',
'u8->bool': 'Zerocopy.stdTransmuteU8ToBool',
}
if (matches[0].get('interpretation_extension') != 'closed-implicit-owned-provider-v1'
or matches[0].get('providers') != expected_providers
or meta['is_local'] or function['body'] != {
'Intrinsic': {'name': 'transmute', 'arg_names': ['src']}}):
raise ValueError('Standard transmute reviewed boundary extension changed')
# A builtin may replace a visible Rust body. Always select the
# interpretation first, rather than approving the unused body.
self.visited[index] = {'rust': name, 'origin': 'interpretation',
Expand Down Expand Up @@ -721,7 +736,22 @@ def block(self, block, unwind=False):
'usize', 'core::num::niche_types::NonZeroUsizeInner']
if actual != expected:
raise ValueError(f'Unsupported NonZero::new_unchecked instantiation {actual}')
self.calls.append({'caller': self.current, 'callee': name})
call_evidence = {'caller': self.current, 'callee': name}
if name == 'core::intrinsics::transmute':
actual = [self.ty_name(ty) for ty in fn['generics']['types']]
providers = {
('u32', '[u8;4]'): 'Zerocopy.stdTransmuteU32ToBytes',
('[u8;4]', 'u32'): 'Zerocopy.stdTransmuteBytesToU32',
('u8', 'bool'): 'Zerocopy.stdTransmuteU8ToBool',
}
if tuple(actual) not in providers:
raise ValueError(f'Unsupported standard transmute instantiation {actual}')
if fn['generics']['regions'] or fn['generics']['const_generics'] or fn['generics']['trait_refs']:
raise ValueError('Standard transmute acquired additional generic arguments')
call_evidence.update(type_arguments=actual,
provider=providers[tuple(actual)],
caller_def_id=self.current_function['def_id'])
self.calls.append(call_evidence)
self.visit(callee)
self.block(body['on_unwind'], True)
elif tag == 'Assert':
Expand Down Expand Up @@ -837,7 +867,7 @@ def input_identity(root):
for name, value in os.environ.items():
if value and (name in {'RUSTFLAGS', 'CARGO_ENCODED_RUSTFLAGS',
'CARGO_BUILD_RUSTFLAGS', 'RUSTC', 'RUSTC_WRAPPER',
'RUSTC_WORKSPACE_WRAPPER', 'CHARON_ARGS'} or
'RUSTC_WORKSPACE_WRAPPER', 'CHARON_ARGS', 'CARGO_BUILD_TARGET'} or
re.fullmatch(r'CARGO_TARGET_.*_RUSTFLAGS', name)):
raise ValueError(f'Unreviewed compiler override {name}')
configs = []
Expand All @@ -856,7 +886,7 @@ def input_identity(root):
# Conservative lexical check avoids implementing Cargo's precedence
# rules. Even a dormant override is rejected, rather than guessed safe.
text = '\n'.join(line.split('#', 1)[0] for line in path.read_text().splitlines())
if re.search(r'\b(rustflags|rustc|rustc-wrapper|rustc-workspace-wrapper)\b', text):
if re.search(r'\b(rustflags|rustc|rustc-wrapper|rustc-workspace-wrapper)\b|\b(?:build\.)?target\s*=', text):
raise ValueError(f'Unreviewed Cargo compiler configuration: {path}')
# Discovery and freshness use the same unconditional source inventory.
# Cache-like names under src cannot hide newly added Rust specifications.
Expand Down Expand Up @@ -909,7 +939,7 @@ def inspect(root, work, roots, sources, body_digests=None, law_traits=()):
guarded = {row['rust'] for row in registry
if row.get('opaque') or row['signature']['unsafe']}
def guarded_calls(stage):
return Counter((call['caller'], call['callee']) for call in stage['calls']
return Counter((call['caller'], call['callee'], tuple(call.get('type_arguments', []))) for call in stage['calls']
if call.get('callee') in guarded)
missing = guarded_calls(reports['before']) - guarded_calls(reports['llbc'])
if missing:
Expand All @@ -932,6 +962,8 @@ def guarded_calls(stage):
def check_translation(work, evidence):
text = (work / 'Zerocopy/FunsExternal_Template.lean').read_text()
signatures = {
'core.intrinsics.transmute':
'axiom core.intrinsics.transmute {Src : Type} (Dst : Type) : Src → Result Dst',
'util.transmute_unchecked':
'axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst',
'util.copy_unchecked':
Expand Down
4 changes: 2 additions & 2 deletions verification/aeneas/control_runner.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,9 +27,9 @@
import time

FAMILIES = ('producers', 'authoring', 'trait-rounding', 'unsafe', 'coverage', 'abi',
'contracts', 'dependencies', 'admission', 'semantics')
'contracts', 'dependencies', 'admission', 'semantics', 'owned-std')
MODELS = ('golden-verification', 'verification')
FIXTURES = ('NegativeControl.lean', 'WeakOutcome.lean',
FIXTURES = ('StdTransmuteAuditProbe.lean', 'NegativeControl.lean', 'WeakOutcome.lean',
'RoundingConstructorControl.lean', 'RoundingDomainControl.lean',
'Zerocopy/ScopeControl.lean', 'Zerocopy/ShapeControl.lean',
'Zerocopy/ModelControl.lean', 'Proofs/WitnessOwnerControl.lean',
Expand Down
3 changes: 2 additions & 1 deletion verification/aeneas/external.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,5 +33,6 @@
{"rust": "core::num::{u32}::to_le_bytes", "signature": {"unsafe": false, "inputs": ["u32"], "output": "[u8;4]", "types": 0, "consts": 0}, "lean": "core.num.U32.to_le_bytes"},
{"rust": "core::num::{usize}::MAX", "signature": {"unsafe": false, "inputs": [], "output": "usize", "types": 0, "consts": 0}, "lean": "Usize.MAX"},
{"rust": "core::clone::impls::{core::clone::Clone<usize>}::clone", "signature": {"unsafe": false, "inputs": ["&usize"], "output": "usize", "types": 0, "consts": 0}, "lean": "core.clone.CloneUsize"},
{"rust": "core::num::niche_types::{core::clone::Clone<core::num::niche_types::NonZeroUsizeInner>}::clone", "signature": {"unsafe": false, "inputs": ["&core::num::niche_types::NonZeroUsizeInner"], "output": "core::num::niche_types::NonZeroUsizeInner", "types": 0, "consts": 0}, "lean": "core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone"}
{"rust": "core::num::niche_types::{core::clone::Clone<core::num::niche_types::NonZeroUsizeInner>}::clone", "signature": {"unsafe": false, "inputs": ["&core::num::niche_types::NonZeroUsizeInner"], "output": "core::num::niche_types::NonZeroUsizeInner", "types": 0, "consts": 0}, "lean": "core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone"},
{"rust": "core::intrinsics::transmute", "signature": {"unsafe": true, "inputs": ["T0"], "output": "T1", "types": 2, "consts": 0}, "lean": "core.intrinsics.transmute", "interpretation_extension": "closed-implicit-owned-provider-v1", "providers": {"u32->[u8;4]": "Zerocopy.stdTransmuteU32ToBytes", "[u8;4]->u32": "Zerocopy.stdTransmuteBytesToU32", "u8->bool": "Zerocopy.stdTransmuteU8ToBool"}}
]
43 changes: 39 additions & 4 deletions verification/aeneas/golden/Funs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -792,7 +792,7 @@ def trait_checks.check_array_into_bytes : Result Unit := do
(Array.Insts.ZerocopyIntoBytes 2#usize Bool.Insts.ZerocopyIntoBytes))

/-- [zerocopy::util::padding_needed_for]:
Source: 'src/util/mod.rs', lines 163:0-223:1 -/
Source: 'src/util/mod.rs', lines 166:0-226:1 -/
def util.padding_needed_for
(len : Std.Usize)
(align : core.num.nonzero.NonZero Std.Usize
Expand All @@ -808,7 +808,7 @@ def util.padding_needed_for
ok (i2 &&& mask)

/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
Source: 'src/util/mod.rs', lines 250:0-268:1 -/
Source: 'src/util/mod.rs', lines 253:0-271:1 -/
def util.round_down_to_next_multiple_of_alignment
(n : Std.Usize)
(align : core.num.nonzero.NonZero Std.Usize
Expand All @@ -825,7 +825,7 @@ def util.round_down_to_next_multiple_of_alignment
ok (n &&& mask)

/-- [zerocopy::util::max]:
Source: 'src/util/mod.rs', lines 277:0-283:1 -/
Source: 'src/util/mod.rs', lines 280:0-286:1 -/
def util.max
(a : core.num.nonzero.NonZero Std.Usize
core.num.niche_types.NonZeroUsizeInner)
Expand All @@ -845,7 +845,7 @@ def util.max
else ok a

/-- [zerocopy::util::min]:
Source: 'src/util/mod.rs', lines 292:0-298:1 -/
Source: 'src/util/mod.rs', lines 295:0-301:1 -/
def util.min
(a : core.num.nonzero.NonZero Std.Usize
core.num.niche_types.NonZeroUsizeInner)
Expand All @@ -864,6 +864,41 @@ def util.min
then ok b
else ok a

/-- [zerocopy::util::owned_transmute::to_bytes_native]:
Source: 'src/util/owned_transmute.rs', lines 29:0-33:1 -/
def util.owned_transmute.to_bytes_native
(value : Std.U32) : Result (Array Std.U8 4#usize) := do
core.intrinsics.transmute (Array Std.U8 4#usize) value

/-- [zerocopy::util::owned_transmute::to_bytes]:
Source: 'src/util/owned_transmute.rs', lines 22:0-24:1 -/
def util.owned_transmute.to_bytes
(value : Std.U32) : Result (Array Std.U8 4#usize) := do
util.owned_transmute.to_bytes_native value

/-- [zerocopy::util::owned_transmute::from_bytes]:
Source: 'src/util/owned_transmute.rs', lines 44:0-48:1 -/
def util.owned_transmute.from_bytes
(bytes : Array Std.U8 4#usize) : Result Std.U32 := do
core.intrinsics.transmute Std.U32 bytes

/-- [zerocopy::util::owned_transmute::checked_bool]:
Source: 'src/util/owned_transmute.rs', lines 59:0-67:1 -/
def util.owned_transmute.checked_bool
(byte : Std.U8) : Result (Option Bool) := do
if byte < 2#u8
then let b ← core.intrinsics.transmute Bool byte
ok (some b)
else ok none

/-- [zerocopy::util::owned_transmute::round_trip_checks]:
Source: 'src/util/owned_transmute.rs', lines 75:0-79:1 -/
def util.owned_transmute.round_trip_checks
(value : Std.U32) : Result Unit := do
let bytes ← util.owned_transmute.to_bytes value
let restored ← util.owned_transmute.from_bytes bytes
massert (restored = value)

/-- [zerocopy::util::safety_checks::checked_bool]:
Source: 'src/util/safety_checks/mod.rs', lines 28:0-38:1 -/
def util.safety_checks.checked_bool
Expand Down
11 changes: 9 additions & 2 deletions verification/aeneas/golden/FunsExternal_Template.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,13 @@ set_option maxHeartbeats 1000000
set_option maxRecDepth 2048
open Zerocopy

/-- [core::intrinsics::transmute]:
Source: '/rustc/library/core/src/intrinsics/mod.rs', lines 898:0-898:57
Name pattern: [core::intrinsics::transmute]
Visibility: public -/
@[rust_fun "core::intrinsics::transmute"]
axiom core.intrinsics.transmute {Src : Type} (Dst : Type) : Src → Result Dst

/-- [core::num::niche_types::{impl core::clone::Clone for core::num::niche_types::NonZeroUsizeInner}::clone]:
Source: '/rustc/library/core/src/num/niche_types.rs', lines 17:17-17:22
Name pattern: [core::num::niche_types::{core::clone::Clone<core::num::niche_types::NonZeroUsizeInner>}::clone]
Expand All @@ -51,11 +58,11 @@ axiom core.num.nonzero.NonZero.get
core.num.nonzero.NonZero T Clause0_NonZeroInner → Result T

/-- [zerocopy::util::copy_unchecked]:
Source: 'src/util/mod.rs', lines 310:0-325:1 -/
Source: 'src/util/mod.rs', lines 313:0-328:1 -/
axiom util.copy_unchecked
: Slice Std.U8 → Slice Std.U8 → Result (Slice Std.U8)

/-- [zerocopy::util::transmute_unchecked]:
Source: 'src/util/mod.rs', lines 337:0-366:1 -/
Source: 'src/util/mod.rs', lines 340:0-369:1 -/
axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst

Loading
Loading