nvx-rs: stop reading the activation record's template and workload identity by esaurez · Pull Request #1279 · microsoft/nvx

Enrique Saurez (esaurez) · 2026-11-04T12:30:58Z

Part of #1101 (SL2.5a: no consumer outside the codec and its schema reads what record v2 drops).

Stacked on #1277, the follow-up of SL0.4 (#1261, in #1091) whose public-API snapshots this pull request updates: #1277's head, cfd105a9, is this pull request's base. GitHub retargets this pull request to dev once #1277 merges.

What and why

Record v2, in SL2.5b, drops among other fields the activation record's template reference and workload identity. Two readers of those fields remain outside the codec, both in the nvx crate: the host's reattach of a clone, and the guest's apply. This pull request removes those two reads, so that SL2.5b can change the codec without keeping fields for them. The runtime adapter, a test program, follows the smaller result.

Reattach (nvx-rs/src/host/template/clone/reattach.rs). Reattaching a clone no longer compares the activation record's template with the clone's lease. The clone records check it instead: read_failure_of (records.rs), which the reattach already calls under the store's lock, refuses a failure record whose store, lease, generation, key or launch differs. A healthy clone, which has no failure record, is taken over as before. The activation record must still be the canonical encoding of a restore's record, or the reattach fails with the same host fault as before. Leases, clone records and their matching rules don't change.
Apply (nvx-rs/src/guest/clone/activation/apply.rs). The guest's apply no longer extracts the record's workload identity, checks its account in the image or passes it on.
- Applied loses its identity and Applied::identity, and into_parts returns (Root, RuntimeBinds).
- ApplyError::Account, System::account and the account check go with them.
- The hostname, machine-ID, resolver, image, mapping, transaction and cleanup checks don't change.
- The private View::entry, through which the guest binds the runtime files, such as the generated machine ID and the resolver file, now builds its Entry with the identity 0:0. That entry validates its path, IDs, capabilities and hostname and binds those files. It prepares no execution, and 0:0 is no default identity of a sandbox or an execution.
Each execution names its identity (tests/runtime-adapter/src/worker.rs and worker/activation.rs).
- The runtime adapter's RootOperations::apply returns Result<(), ApplyError>.
- A clone's sandbox starts with no sandbox-wide identity: each execution in a clone names its own identity, and one that names none fails with EINVAL.
- A machine ID or a view that fails still ends the clone with the workload's activation status.
- A cold sandbox's workload identity is still checked against the accounts of its assembled root before Ready. An execution's explicit identity is still checked when it starts.
Record v1 stays as it is. VERSION stays 1, and the schema, the codec, the canonical fixtures and the record writers don't change. TemplateReference, StoreGeneration and activation::Identity stay for the old stores. start --workload-identity and run --workload-identity still accept the identity and record it in the activation record; the guest now ignores it when it applies the record, and SL2.5b drops it from the record.
The documentation says so:
- the guest's clone module and nvx-rs's README;
- the activation module's docs of WorkloadView, its identity field and WorkloadIdentity, and the doc comment of CloneRequest::workload;
- the doc comments of the runtime adapter's clone::Request::workload_identity, its clone module and its host program's start;
- the docs of the runtime adapter's worker and activation, and of vm_clone's module and its NOBODY;
- the runtime adapter's README: its clone steps, clone::Request's paragraph, its status table, start --workload-identity, the guest-session fake root, and the rows of the three rewritten vm_clone scenarios.

python scripts/public_api.py --update regenerated the public API on Linux, which loses 4 lines; the one on Windows doesn't change:

--- nvx-rs/public-api/linux.txt (base)
+++ nvx-rs/public-api/linux.txt (this head)
@@ -678 +677,0 @@ method nvx::guest::clone::Applied::hostname
-method nvx::guest::clone::Applied::identity
@@ -691,3 +689,0 @@ enum nvx::guest::clone::ApplyError
-variant nvx::guest::clone::ApplyError::Account
-field nvx::guest::clone::ApplyError::Account::error
-field nvx::guest::clone::ApplyError::Account::teardown

Not in this pull request, as #1101 says:

The activation schema, codec, version and canonical fixtures, which SL2.5b changes together.
Deleting TemplateReference, StoreGeneration or activation::Identity, which the old stores use until SL6.1.
Replacing the test adapter or redesigning execution identities.
Changing clone leases, clone records or their matching rules.

Tests

python scripts/check_test_changes.py --base cfd105a9797fce81d0b72ee5b9ccf3700d2f1d2e reports "33 change(s) to existing tests; relocated unchanged: 0; added: 3".

The 3 added entries are not three new scenarios: they are the new reattach test, and the two tests that replace retired ones under new names.
Every change follows from the account check and the identity leaving apply, or from the reattach's check moving to the clone records.
No test is disabled or deselected, and the test layout check passes.

Added, in nvx-rs/src/host/template/clone/tests/launch.rs:

a_reattach_fails_a_clone_whose_record_of_a_failure_is_of_another_template:
- a healthy clone, with no failure record, is taken over;
- a failure record whose leased generation differs, or whose key does, is refused as another clone's failure: the clone is ended, its runtime cleared and its lease released, and nothing is quarantined.

nvx-rs/src/guest/clone/activation/apply/tests.rs, 18 tests, which run on Linux only:

Retired: a_workload_identity_without_an_account_in_the_image_is_refused_before_ready.
- the_application_checks_no_account_of_the_record_s_workload_identity replaces it: all 7 systems, whatever accounts their images hold, reach Ready, with the assembly and the view's bind as the only effects.
Renamed: assembly_and_identity_inputs_are_taken_exactly_from_the_record becomes assembly_inputs_are_taken_exactly_from_the_record.
- It keeps the image, upper and overlay assertions for records with and without an identity, and loses the identity's flow.
Rewritten: an_export_or_a_network_that_fails_fails_the_activation_once_the_root_is_torn_down.
- The failing steps' indices shift down by one (4 to 3, 5 to 4, 6 to 5, and 7 to 6 in three cases), since the account check is no longer a step.
- All six failure cases and their cleanup assertions stay.
Rewritten: application_errors_name_their_cause.
- Its Account case goes.
- The case that checks how an activation wraps an error now uses a machine ID's AlreadyExists.
Rewritten so that they lose only the record's identity or the account from their expectations, keeping their other assertions:
- a_valid_activate_activates_the_root_and_the_workload_once_before_ready;
- a_gpt_disk_s_partition_table_is_reread_before_its_root_is_assembled;
- a_generated_machine_id_is_generated_once_after_the_gate_for_every_execution;
- the_view_s_entry_takes_the_record_s_hostname_and_machine_id;
- a_machine_id_or_a_view_that_fails_fails_the_activation_once_the_root_is_torn_down;
- an_export_is_mounted_through_the_template_s_device_and_handed_to_the_adapter;
- a_network_s_dns_server_is_written_to_a_resolver_file_that_every_execution_sees;
- a_network_that_publishes_the_workload_s_listeners_starts_their_announcer_to_its_gateway;
- a_generated_machine_id_and_a_resolver_file_keep_the_root_busy_until_their_binds_are_removed, which needs root.
Kept unchanged:
- no_mount_spawn_or_id_generation_happens_before_the_gate, whose shared expectations lose only the account;
- a_failed_assembly_is_final_and_reads_and_tears_down_nothing;
- the_runtime_s_binds_are_removed_before_the_root_is_torn_down;
- a_resolver_file_names_its_dns_server_once_and_every_execution_may_read_it;
- the_application_refuses_without_privileges_what_it_cannot_assemble.
Helpers:
- Effect loses Account;
- view() and activated() lose the identity, and full_view(), applied_everything() and the imports follow;
- Refusal, FakeSystem::account and workload(), which nothing uses any more, go.

The runtime adapter:

worker::activation::tests::each_class_of_failure_ends_the_clone_with_its_own_status (src/worker/activation/tests.rs): its ApplyError::Account case goes. Its machine-ID and view cases, and the other status classes, stay.
tests/guest_session.rs:
- The fake root's apply checks no account and returns Ok(()).
- a_clone_s_activation_fails_finally_with_the_status_of_the_failure_s_class loses only its two cases of a record whose workload identity has no account, 4242 and ORPHAN. ORPHAN stays for the checks of explicit executions.
- Retired: a_clone_s_executions_run_as_the_workload_identity_and_with_the_hostname_of_its_record. a_clone_s_executions_name_their_own_identity_and_take_the_hostname_of_its_record replaces it: for a record with a workload identity and for one without, an execution that names no identity fails with EINVAL, and one that names an identity runs with the record's hostname.
- a_clone_reports_when_its_events_happened_after_the_acknowledgement and a_clone_maps_its_record_s_table_from_its_export_and_leaves_the_proxy_to_the_host now name their executions' identity. Their ordering, mapping and teardown assertions stay.
tests/vm_clone.rs, which boots VMs:
- a_clone_whose_activation_fails_ends_before_it_is_ready loses only its case of a start with a workload identity whose account the image lacks, with that identity's constant, STRANGER. Its unusable scratch, forbidden journal and three protocol refusals stay.
- Renamed: a_clone_runs_its_executions_as_its_workload_identity_once_it_is_ready becomes a_clone_runs_the_executions_that_name_their_identity_once_it_is_ready.
  - Its start still passes --workload-identity 65534:65534, nobody's, which the record keeps.
  - An execution with --identity 65534:65534 runs as 65534/65534, and one without --identity fails with EINVAL.
  - Its timeline checks stay.
- a_run_runs_one_execution_in_its_clone_then_tears_the_clone_down: the run no longer passes --workload-identity, its execution names --identity 65534:65534, and its refused execution names none. Its environment, directory, status and output assertions stay.
tests/runtime-adapter/scenarios.txt and the README's scenario rows follow the rename.
Kept unchanged, and run:
- the cold path's the_worker_checks_the_account_of_the_sandbox_s_workload_identity_in_the_assembled_root, in tests/guest_session.rs;
- vm_layered's accountless_workload_identity_fails_its_stage and executions_run_as_the_workload_identity;
- vm_clone's a_clone_whose_view_cannot_be_set_ends_before_it_is_ready;
- the guest entry's existing_accounts_are_read_below_the_root and account_databases_are_bounded_regular_files_reached_through_no_link.

Size

9 core lines in 2 counted files, as measured under #1076's rules: 5 in apply.rs and 4 in reattach.rs. #1101 estimated 80 core lines in 2 files, with a stop at 160.

The measure excludes 31 added lines of documentation and 260 of tests.
It counts the runtime adapter, tests/runtime-adapter/, as tests, although its worker changes change how that test program behaves.
In all, 18 paths change, with 353 lines added and 524 removed.

The 18 changed paths, by the measure's category

Path	Category	Core lines
`nvx-rs/README.md`	doc	0
`nvx-rs/public-api/linux.txt`	doc	0
`nvx-rs/src/activation/mod.rs`	core, no core lines	0
`nvx-rs/src/guest/clone.rs`	core, no core lines	0
`nvx-rs/src/guest/clone/activation/apply.rs`	core	5
`nvx-rs/src/guest/clone/activation/apply/tests.rs`	test	0
`nvx-rs/src/host/template/clone.rs`	core, no core lines	0
`nvx-rs/src/host/template/clone/reattach.rs`	core	4
`nvx-rs/src/host/template/clone/tests/launch.rs`	test	0
`tests/runtime-adapter/README.md`	doc	0
`tests/runtime-adapter/scenarios.txt`	doc	0
`tests/runtime-adapter/src/bin/runtime-adapter-host.rs`	test	0
`tests/runtime-adapter/src/clone.rs`	test	0
`tests/runtime-adapter/src/worker.rs`	test	0
`tests/runtime-adapter/src/worker/activation.rs`	test	0
`tests/runtime-adapter/src/worker/activation/tests.rs`	test	0
`tests/runtime-adapter/tests/guest_session.rs`	test	0
`tests/runtime-adapter/tests/vm_clone.rs`	test	0

Validation

At this head, 36fa8834, on a Windows x86-64 host with WHP and on a Linux x86-64 host with MSHV (Azure Linux 3, kernel 6.18.34.mshv3-1.azl3, AMD EPYC 9V74), with Rust 1.95.0 and the MSRV, 1.89. CI hasn't run on this head, and nothing was published.

check-nvx-rs on Windows: the 29 steps that apply there pass.
- cargo fmt.
- clippy with all targets and features; for the library, with default features and without; for the library and the binaries with cli, and with testing but no default features; and for -p nvx's library without default features.
- The tests with all features (1315 passed, 0 failed, 19 ignored) and with the default ones.
- A --list check that the new reattach test runs.
- The library without default features, built and tested.
- Artifact bundling, the docs, python scripts/public_api.py and the MSRV check.
- The runtime adapter's protocol and host configurations, each with fmt, clippy, build, test, docs and the MSRV.
- clippy for x86_64-unknown-linux-musl, of nvx-rs with all features and of the adapter's guest configuration.
check-nvx-rs on Linux: every step passes.
- fmt and clippy.
- The tests with all features (2128 passed, 0 failed, 34 ignored), and the --list check.
- The 18 apply tests by name: 17 passed and 1 ignored, the root-only test below.
- The default tests, and the library without default features.
- Artifact bundling and the docs.
- python scripts/public_api.py, whose listings equal the committed snapshots byte for byte.
- The MSRV check and the macOS check.
- check-guest-binaries, and the guest binaries built and tested.
- The runtime adapter's protocol, host and guest (musl) configurations, each with build, test, docs and the MSRV.
The root-only apply test: a_generated_machine_id_and_a_resolver_file_keep_the_root_busy_until_their_binds_are_removed needs root and Linux 6.8 or later, and CI doesn't run it.
- It passed as root on Linux 6.18, with the same test binary as the tests above: 1 passed, 0 ignored.
- It printed no skip reason under --nocapture.
validate-nvx and check-quality on Linux: all pass:
- the unit tests (1797 run, 39 skipped) and scripts/test_adversarial.py (84 run, none skipped);
- test_hosts.py, the CLI's help, and the OpenVMM vectors and CPU profiles;
- nvx.py test-runtime-adapter --check-only;
- ShellCheck, shfmt, ruff, and pyright for Linux and Windows;
- the Markdown links, the test layout, the kernel config, the specula tests (25) and the test-change check.
validate-nvx and check-quality on Windows: 27 of 28 steps pass:
- the unit tests (1797 run, 71 skipped), and scripts/test_adversarial.py with CPython 3.14.9 (84 run, 11 of them skipped there as Linux-only);
- test_hosts.py, the CLI's help, and the OpenVMM vectors and CPU profiles;
- ruff, pyright, the links, the test layout, the kernel config and the PowerShell syntax;
- nvx.py test-runtime-adapter --check-only ("156 scenarios name exactly the tests of 11 targets") and the test-change check.
- The specula tests FAIL there: test_ci imports fcntl, which Windows lacks (ModuleNotFoundError: No module named 'fcntl'), as at nvx: hide NVX's programs from the public API #1265's head. They pass on Linux, where check-quality runs them.
VMs: python scripts/nvx.py test-runtime-adapter passed "the 156 scenarios of 11 targets" on MSHV and on WHP.
- These include vm_clone's 35: the three rewritten ones by name, the view refusal and the cold path's identity scenarios.
- The four public test-microvm sandbox scenarios, managed-exec-config, sandbox-lifecycle, sandbox-proxy-only and sandbox-ram-upper, passed on both.
- On MSHV, these runs ran as root, since /dev/mshv is root-only on that host, with executables that the user's account built beforehand.
Inputs built from this head:
- Guest artifacts: built with Docker. The guest binaries, the kernel, the initramfs images, the Ubuntu distro layer and the scratch template were built; only base and package layers came from Docker's cache.
  - The guest binaries' source digest is d436960d... over 146 files (2ab01e37... at the base).
  - Each initramfs's package manifest names that digest for its 9 Rust helpers.
- OpenVMM: built at the pinned 5aa8b028 for MSHV and for WHP.
- The CLI, nvx-rs: on Linux, built with Cargo before the runs; on Windows, built by nvx.py when the Python unit tests needed it, and reused by the WHP runs.
- The adapter's guest agent (musl): built on Linux, and copied with the guest artifacts, 14 files in all, to the Windows host, where their SHA-256 digests matched.
- The adapter's test executables: built on each host before the VM runs, by --check-only on Linux and by the Rust checks on Windows, and reused by the runs.
The CLI's provenance record:
- The Linux CLI was built with plain Cargo, so it had no build/nvx-rs.provenance.json during the runs above.
- Nothing that reads that record ran on either host then: nvx.py test-adversarial and packaging do, while the runtime identity that each sandbox records reads only the OpenVMM, kernel and initramfs records.
- Afterwards, release.validate_runtime_artifact_provenance passed on Windows and failed on Linux for the missing record.
- python scripts/nvx.py record-nvx-rs-provenance then recorded the unchanged Linux CLI: its bytes, size and times, and the sources, were the same before and after. The validators then passed: the OpenVMM, kernel, initramfs and CLI checks, and the whole runtime check.
- That record is post hoc. It was not written before the VM runs, and it doesn't change how those runs were set up.
Build admission on the shared Windows host: two compiles there ran without a slot of the host's build admission, with 4 Cargo jobs but no slot.
- The artifact-bundling step's cargo test --features bundled (26 s).
- The CLI build that nvx.py started in the Python unit tests (26 s).
- The same steps ran without a slot when SL0.4 and SL1.5 were validated: bundling took 58.93 s and the CLI 1 min 05 s for SL0.4, and bundling 9.99 s for SL1.5.
- These are process deviations, reported as they happened; nothing was rerun to replace them.
Not run locally: KVM; macOS beyond cargo check; test-microvm's other scenarios; the benchmarks. CI runs them.
Not addressed: the dev push run 41783992397 failed NVX microVM tests / Linux / KVM / Guests and sandboxes.
- The failure is in the vm_clone scenario one_template_serves_the_clones_of_every_network_policy_at_its_guest_s_address, whose execution reply read listener 124, a timeout, at tests/runtime-adapter/tests/vm_clone.rs:1635.
- Its cause is unknown. This pull request doesn't fix it, and the scenario's passes on MSHV and WHP here don't show that it does.
- CI's KVM run covers it.

github-actions · 2026-11-04T12:31:26Z

This pull request changes existing tests

It modifies or removes 33 existing test asset(s), listed below. Review each with care: a change to a test can hide a regression that the test caught. See doc/contribute.md#changes-to-existing-tests.

Test code

Test data

Change	What	Before	After
modified file	`tests/runtime-adapter/scenarios.txt`	`tests/runtime-adapter/scenarios.txt`	`tests/runtime-adapter/scenarios.txt`

Relocated unchanged: 0; added: 3. Compared the merge base 6bcb68fce00e with a81617afa69c.

Copilot

🟢 Approval recommended

No active review issues remain for the changes preparing NVX for activation record v2.

No open issues 🎉

What changed in this PR

Prepares NVX for activation record v2 under #1101 by removing consumers of the record’s template reference and workload identity, while leaving the v1 schema and codec unchanged.

Changes:

Removes the activation-record template comparison during reattach, retaining existing clone-record validation.
Removes workload identity checking and propagation from guest activation; runtime-adapter clone executions must name their own identity.
Updates regression tests, documentation, scenario names, and the Linux public API snapshot.

File	Description
`tests/runtime-adapter/tests/vm_clone.rs`	Updates VM scenarios for explicit execution identities.
`tests/runtime-adapter/tests/guest_session.rs`	Updates fake activation and execution-identity assertions.
`tests/runtime-adapter/src/worker/activation/tests.rs`	Removes the retired account-error status case.
`tests/runtime-adapter/src/worker/activation.rs`	Starts clone sandboxes without a sandbox-wide identity.
`tests/runtime-adapter/src/worker.rs`	Changes activation results to return no identity.
`tests/runtime-adapter/src/clone.rs`	Documents that guests ignore the recorded workload identity.
`tests/runtime-adapter/src/bin/runtime-adapter-host.rs`	Updates clone-start option documentation.
`tests/runtime-adapter/scenarios.txt`	Registers the renamed clone identity scenario.
`tests/runtime-adapter/README.md`	Documents revised activation behavior and scenarios.
`nvx-rs/src/host/template/clone/tests/launch.rs`	Tests healthy reattach and mismatched failure records.
`nvx-rs/src/host/template/clone/reattach.rs`	Removes the activation-record template comparison.
`nvx-rs/src/host/template/clone.rs`	Updates `CloneRequest::workload` documentation.
`nvx-rs/src/guest/clone/activation/apply/tests.rs`	Revises activation tests for ignored workload identities.
`nvx-rs/src/guest/clone/activation/apply.rs`	Removes account checks, identity results, and account errors.
`nvx-rs/src/guest/clone.rs`	Documents execution identities independently of activation.
`nvx-rs/src/activation/mod.rs`	Clarifies the retained v1 workload identity fields.
`nvx-rs/README.md`	Updates the guest activation description.
`nvx-rs/public-api/linux.txt`	Removes the identity accessor and account-error entries.

_{Review effort: Balanced}

A reattach refused the clone's activation record unless its restore section named the template of the clone's lease. As decided for #1101, the reattach leaves that to the clone's records: it already matches them with the lease through read_failure_of, which refuses the record of another template's failure. read_activation still requires the canonical encoding of the record of a restore, with the same fault. The new test a_reattach_fails_a_clone_whose_record_of_a_failure_is_of_another_template takes over a healthy clone without a failure record, then refuses, as another clone's failure, a failure record of another leased generation, and one of another key of the leased generation. Part of #1101. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: c2e22d0d-c583-4401-a947-31781d4fec41

A clone's activation record may carry a workload identity, whose account nvx::guest::clone::apply checked in the assembled root, and as which every execution of the clone then ran. A clone now has no workload identity of the whole sandbox: the application ignores the record's, and each execution names its own identity, as in a sandbox whose root configuration names none, so a start that names none is refused with EINVAL. A cold sandbox's workload identity is unchanged. - apply: Applied loses identity(), into_parts its identity, and ApplyError its Account variant. The entry that binds the runtime's files, through which no execution runs, takes the user and group ID 0. - The runtime adapter's worker starts a clone's sandbox without a workload identity. Machine ID and view failures keep the status ACTIVATION_WORKLOAD. - The record, its codec and validation, and the host program's --workload-identity keep the identity; their docs say that the guest ignores it. - The Linux public-API snapshot loses the four lines of Applied::identity and ApplyError::Account. The guest's apply tests and the adapter's guest_session and vm_clone tests drop the account refusals of a record's identity, and their clones' executions name their identities. Part of #1101. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: c2e22d0d-c583-4401-a947-31781d4fec41 Copilot-Session: 383380be-1df9-4f25-bf77-97c24b2eb591

Copilot

🟢 Approval recommended

No active review issues block the changes preparing activation-record consumers for v2.

No open issues 🎉

_{Review effort: Balanced}

github-actions · 2026-11-04T19:50:00Z

Neuro-formal verification (NFV) selects nontrivial properties from PR intent and source, tries verification, then tries refutation.

NFV: 0 refuted, 5 verified in PR #1279

PR head a81617afa69c, base 6bcb68fce00e · run and evidence

These are results for translated models under their stated assumptions, not proofs of source-code correctness or confirmed source bugs.

refuted: 0 · verified: 5 · resources exhausted: 0 · type-check/audit failure: 3

P1

Intended property: Invalid proposed property

Outcome: type-check/audit failure

Diagnostic

Property lacks an exact PR/commit evidence quote

P2

Intended property: If activation completion succeeds, settle launches executions in a sandbox with no sandbox-wide identity, using the applied hostname and publication; it records the applied mappings and returns exactly 1 + joined Ready messages.

Outcome: type-check/audit failure

Diagnostic

Witness arity exceeds supported bounds

P3

Inferred property: If activation completion fails, settle takes the failure-ending path rather than marking the timeline ready, launching executions, installing a mapping order, or returning Ready messages.

Outcome: verified

The property was verified for the translated model.

Verification details

Captured source (inferred property): Err(failure) => self.end(executions, &failure),

Assumptions: No additional input restrictions.

Environment models: Represents the omitted Activation::complete result using the explicit completionSucceeds input.; Clears executions and returns the failure-ending step without Ready messages.; Constructs the Ready message used by the successful continuation.; Records the observable occurrence of executions.run_in in the successful branch.

Checked property:

ensures appliedPresent && !completionSucceeds ==> (tookFailureEndingPath && !timelineReady && !executionsLaunched && !mappingOrderInstalled && !readyMessagesReturned)

Evidence: ec8a2fee5080cd810a43/verification/model.dfy; SHA-256 0ee92f51e77fc7ff58fffcb0bee2e1a883ab1df78f518e91f3b20c17545aca85.

The full verified Dafny is retained in the linked run artifact.

P4

Inferred property: If clone application fails, propagate its error without changing the worker's export or root. If it succeeds, move the applied export into the worker, retain the remaining applied clone as its assembled root, and return success.

Outcome: verified

The property was verified for the translated model.

Verification details

Captured source (inferred property): let mut applied = clone::apply(record, template, deadline)?;
self.export = applied.take_export();
self.root = Some(Assembled::Clone(applied));
Ok(())

Assumptions: No additional input restrictions.

Environment models: Represents clone::apply as propagating its supplied error on failure or returning an Applied value with the supplied export and remaining clone state on success.; Moves Applied.export to the worker while retaining the other Applied fields represented by the clone-state token.

Checked property:

ensures ((!cloneSucceeded ==> (!resultSucceeded && resultError == cloneError && finalExportPresent == oldExportPresent && (oldExportPresent ==> finalExport == oldExport) && finalRootPresent == oldRootPresent && (oldRootPresent ==> finalRoot == oldRoot))) && (cloneSucceeded ==> (resultSucceeded && finalExportPresent == appliedExportPresent && (appliedExportPresent ==> finalExport == appliedExport) && finalRootPresent && finalRoot == appliedClone)))

Evidence: 985c9c33488cbefbe869/verification/model.dfy; SHA-256 28c5547d37a1917e62b2ff94d1e30bb89db22cbcbaa32330e4b709b8af8698c4.

The full verified Dafny is retained in the linked run artifact.

P5

Intended property: Given a readable canonical restore activation record and successful preceding operations, reattachment does not reject before invoking the VM reattach operation merely because the activation record’s template reference differs from the clone lease; failure-record matching remains the mechanism for detecting another template’s clone failure.

Outcome: type-check/audit failure

Diagnostic

The requested corrected full tagged Dafny model exceeds the available response budget; returning a truncated model would violate the requirement to preserve the complete source slice and property.

P6

Intended property: For any successfully read and decoded activation record, acceptance depends only on its bytes being the canonical encoding and on it containing a restore section; its template reference is not compared with a clone lease.

Outcome: verified

The property was verified for the translated model.

Verification details

Quoted intention: Reattaching a clone no longer compares the activation record's template with the clone's lease.

Assumptions: Every integer representing a byte read from the activation record is in the Rust u8 range.; Every integer representing a byte produced by ActivationRecord::encode is in the Rust u8 range.

Environment models: Models the filesystem open/read chain using explicit abstract inputs for its success and returned bytes.; Models ActivationRecord::decode using explicit abstract inputs for decode success and the decoded template reference.; Returns the explicit abstract canonical encoding of the successfully decoded activation record.; Returns whether the decoded activation record contains its optional restore section.

Checked property:

ensures readSucceeded && decodeSucceeded ==> (accepted <==> (canonicalEncoding == bytes && hasRestore))

Evidence: 5dbc220adf0c4c527d6b/verification/model.dfy; SHA-256 09565b5223178a2c9fb70a3771b05794909e9437a4eb5b225afe55e7ea2c6466.

The full verified Dafny is retained in the linked run artifact.

P7

Intended property: For any root and view, entry builds the runtime-binding Entry with UID/GID 0:0, the view’s hostname and machine ID, and adds the view’s resolver only when one is present.

Outcome: verified

The property was verified for the translated model.

Verification details

Quoted intention: The private `View::entry`, through which the guest binds the runtime files, such as the generated machine ID and the resolver file, now builds its `Entry` with the identity `0:0`.

Assumptions: No additional input restrictions.

Environment models: Projects Entry::new as retaining root, selecting UID/GID 0:0, and initially carrying no resolver.; Models the hostname builder as storing the cloned view hostname.; Models the machine-ID builder as storing the cloned view machine ID.; Models the resolver builder as marking a resolver present and storing its cloned path.

Checked property:

ensures entryRoot == root && uid == 0 && gid == 0 && entryHostname == hostname && entryMachineId == machineId && entryHasResolver == resolverPresent && (resolverPresent ==> entryResolver == resolver)

Evidence: a80efeefc5a87e62f970/verification/model.dfy; SHA-256 a36d044997323591a587b5e58ab4de3c52a24a5c643b4ca054c4396a0b88f0be.

The full verified Dafny is retained in the linked run artifact.

P8

Inferred property: For a Failed activation cause, failure_status returns ACTIVATION_ROOT when the contained error is not one of the recognized ApplyError categories; by contrast, an otherwise unrecognized outer ActivationCause returns ACTIVATION_PROTOCOL.

Outcome: verified

The property was verified for the translated model.

Verification details

Captured source (inferred property): // A failure of the application that this build does not know.
_ => status::ACTIVATION_ROOT,

Assumptions: Each activation status constant is a Rust u8 value.

Checked property:

ensures (cause == 8 && applyError != 0 && applyError != 1 && applyError != 2 && applyError != 3 && applyError != 4 && applyError != 5 ==> status == ACTIVATION_ROOT) && (cause != 0 && cause != 1 && cause != 2 && cause != 3 && cause != 4 && cause != 5 && cause != 6 && cause != 7 && cause != 8 && cause != 9 && cause != 10 ==> status == ACTIVATION_PROTOCOL)

Evidence: 52f6d53133e7234dc6f7/verification/model.dfy; SHA-256 38ff8516961d016ff62313a230b85d363ca86e1f09e47b307040ab1033d79613.

The full verified Dafny is retained in the linked run artifact.

Generated by NFV PR reviewer for #1279 · copilot · gpt56 · 421.6 AIC · ⌖ 8.41 AIC · ⊞ 1.2K · ◷

_{Add this agentic workflow to your repo}

To install this agentic workflow, run

gh aw add microsoft/neuro-formal-verification/workflow@498aad98c39314a8c55c89dff42d771276b957d8

Enrique Saurez (esaurez) added the tests-modified Changes existing tests, test data, or test wiring label Nov 4, 2026

Enrique Saurez (esaurez) self-assigned this Nov 4, 2026

Enrique Saurez (esaurez) requested a balanced review from Copilot November 4, 2026 12:31

Copilot started reviewing on behalf of Enrique Saurez (esaurez) November 4, 2026 12:32

View session

Copilot AI reviewed Nov 4, 2026

View reviewed changes

Base automatically changed from esaurez/slim-1.1.1-sl0.4-snapshots-20261103 to dev November 4, 2026 14:56

Enrique Saurez (esaurez) marked this pull request as ready for review November 4, 2026 15:41

Enrique Saurez (esaurez) marked this pull request as draft November 4, 2026 15:51

This comment has been minimized.

Sign in to view

Enrique Saurez and others added 2 commits November 4, 2026 11:17

Enrique Saurez (esaurez) force-pushed the esaurez/slim-2.3.1-sl2.5a-20261104 branch from 36fa883 to a81617a Compare November 4, 2026 19:21

Copilot AI balanced review requested due to automatic review settings November 4, 2026 19:21

Copilot started reviewing on behalf of Enrique Saurez (esaurez) November 4, 2026 19:21

View session

Enrique Saurez (esaurez) marked this pull request as ready for review November 4, 2026 19:22

Copilot AI reviewed Nov 4, 2026

View reviewed changes

Pedro Henrique Penna (ppenna) approved these changes Nov 4, 2026

View reviewed changes

Pedro Henrique Penna (ppenna) enabled auto-merge November 4, 2026 19:35

Pedro Henrique Penna (ppenna) added this pull request to the merge queue Nov 4, 2026

Merged via the queue into dev with commit eade297 Nov 4, 2026
108 checks passed

Pedro Henrique Penna (ppenna) deleted the esaurez/slim-2.3.1-sl2.5a-20261104 branch November 4, 2026 19:47

Enrique Saurez (esaurez) mentioned this pull request Nov 10, 2026

nvx-rs slimming 2.3.1: activation record v2 carries only what the guest applies #1101

Closed

Navigation Menu

Repository navigation

nvx-rs: stop reading the activation record's template and workload identity - #1279

nvx-rs: stop reading the activation record's template and workload identity#1279
Pedro Henrique Penna (ppenna) merged 2 commits into
devfrom
esaurez/slim-2.3.1-sl2.5a-20261104

Enrique Saurez (esaurez) commented Nov 4, 2026

Uh oh!

github-actions Bot commented Nov 4, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

This comment has been minimized.

Copilot AI left a comment

Uh oh!

Uh oh!

github-actions Bot commented Nov 4, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

Enrique Saurez (esaurez) commented Nov 4, 2026

What and why

Tests

Size

Validation

Uh oh!

github-actions Bot commented Nov 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

This pull request changes existing tests

Test code

Test data

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

🟢 Approval recommended

Uh oh!

This comment has been minimized.

Copilot AI left a comment

Choose a reason for hiding this comment

🟢 Approval recommended

Uh oh!

Uh oh!

github-actions Bot commented Nov 4, 2026

NFV: 0 refuted, 5 verified in PR #1279

P1

P2

P3

P4

P5

P6

P7

P8

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions Bot commented Nov 4, 2026 •

edited

Loading