Skip to content

Commit 52fc2c7

Browse files
committed
ownership-lab H-25: the await-wrapped acquire fixture (positive forms AW1-AW6, hostile twins HW1-HW8), its fixture library and pinned rows, frozen before any code
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Am9eQwzNfbugH72eVKetC2
1 parent 337ca30 commit 52fc2c7

4 files changed

Lines changed: 97 additions & 0 deletions

File tree

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
namespace RLibA;
2+
public sealed class R : IDisposable
3+
{
4+
public bool Disposed;
5+
public void Dispose() { Disposed = true; }
6+
public void Ping() { }
7+
}
8+
public static class FA
9+
{
10+
static readonly R Shared = new R();
11+
public static R Factory() => new R(); // trusted row (sync)
12+
public static Task<R> FactoryAsync() => Task.FromResult(new R()); // trusted row: Task<R>, logical result fresh owned
13+
public static ValueTask<R> FactoryValueTaskAsync() => new ValueTask<R>(new R()); // trusted row: ValueTask<R>
14+
public static Task<R> BorrowedAsync() => Task.FromResult(Shared); // no row: a shared instance
15+
public static Task<R> CachedAsync() => Task.FromResult(Shared); // no row: cached
16+
public static Task FireAndForgetAsync() => Task.CompletedTask; // Task without a resource result
17+
public static Task<R> UnknownAsync() => Task.FromResult(new R()); // fresh in fact, NO row: must not be an acquire
18+
public static Task<R> BorrowedTwinAsync() => Task.FromResult(Shared); // the sync name `BorrowedTwin` has no row either
19+
}
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
<Project Sdk="Microsoft.NET.Sdk"><PropertyGroup><TargetFramework>net8.0</TargetFramework><Nullable>disable</Nullable><ImplicitUsings>enable</ImplicitUsings><Deterministic>true</Deterministic></PropertyGroup></Project>
Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
using System;
2+
using System.Threading.Tasks;
3+
using RLibA;
4+
// H-25 await-wrapped acquire recognition: positive forms and hostile twins, frozen BEFORE any code (h25-prereg-v1.json).
5+
// FA.FactoryAsync / FA.FactoryValueTaskAsync carry trusted rows (the LOGICAL result is fresh owned); BorrowedAsync,
6+
// CachedAsync, UnknownAsync carry none. Expected classifications are in the prereg, not here. Census only: no lowering.
7+
public static class Positive
8+
{
9+
// AW1: Task<R> awaited in an existing-local assignment
10+
public static async Task AW1_task_assignment() { R x = null; x = await FA.FactoryAsync(); x.Ping(); x.Dispose(); }
11+
// AW2: the same through ConfigureAwait(false)
12+
public static async Task AW2_configure_await() { R x = null; x = await FA.FactoryAsync().ConfigureAwait(false); x.Ping(); x.Dispose(); }
13+
// AW3: ValueTask<R>
14+
public static async Task AW3_valuetask() { R x = null; x = await FA.FactoryValueTaskAsync(); x.Ping(); x.Dispose(); }
15+
// AW4: declaration form `var x = await FactoryAsync()`
16+
public static async Task AW4_declaration() { var x = await FA.FactoryAsync(); x.Ping(); x.Dispose(); }
17+
// AW5: declaration form through ConfigureAwait
18+
public static async Task AW5_declaration_configure_await() { var x = await FA.FactoryAsync().ConfigureAwait(false); x.Ping(); }
19+
// AW6: the try/finally initialisation idiom with an awaited trusted factory (the dominant population shape)
20+
public static async Task AW6_try_finally() { R x = null; try { x = await FA.FactoryAsync(); x.Ping(); } finally { x?.Dispose(); } }
21+
}
22+
public static class Hostile
23+
{
24+
// HW1: the task is stored first and awaited later: the Task<R> local is NOT an R acquire; the obligation belongs to the awaited R
25+
public static async Task HW1_deferred_await() { var task = FA.FactoryAsync(); var x = await task; x.Ping(); }
26+
// HW2: awaited result is borrowed (no row): no acquire
27+
public static async Task HW2_borrowed() { R x = null; x = await FA.BorrowedAsync(); x.Ping(); }
28+
// HW3: awaited result is cached (no row): no acquire
29+
public static async Task HW3_cached() { R x = null; x = await FA.CachedAsync(); x.Ping(); }
30+
// HW4: Task without a resource result: nothing is written
31+
public static async Task HW4_fire_and_forget() { await FA.FireAndForgetAsync(); }
32+
// HW5: fresh in fact but NO row: must not be an acquire (the effect comes only from a trusted row)
33+
public static async Task HW5_unknown() { R x = null; x = await FA.UnknownAsync(); x.Ping(); }
34+
// HW6: the sync twin name has no row either; a name-based `Async` strip must never mint
35+
public static async Task HW6_name_twin() { R x = null; x = await FA.BorrowedTwinAsync(); x.Ping(); }
36+
// HW7: awaited result assigned to a field: an escape, classified only
37+
static R _f;
38+
public static async Task HW7_field_store() { _f = await FA.FactoryAsync(); }
39+
// HW8: `await using` declaration of an awaited factory: a using shape, classified only
40+
public static async Task HW8_using_declaration() { using var x = await FA.FactoryAsync(); x.Ping(); }
41+
}
Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
{
2+
"schema": "own.net/re-oracle/v1",
3+
"label": "H-25 await fixture: three trusted rows (sync Factory, Task<R> FactoryAsync, ValueTask<R> FactoryValueTaskAsync), pinned to the fixture assembly; a row on a Task<T>/ValueTask<T> callable means the LOGICAL result T is fresh owned (h25-prereg-v1)",
4+
"entries": [
5+
{
6+
"callable": "RLibA.FA.Factory",
7+
"effect": "return_fresh_owned",
8+
"provenance": "BODY_PROVED",
9+
"assembly": {
10+
"name": "RLibA",
11+
"mvid": "a972665e-5b5e-420c-806d-90011486d0cb"
12+
},
13+
"derived_from": "fixture: FA.Factory() => new R()"
14+
},
15+
{
16+
"callable": "RLibA.FA.FactoryAsync",
17+
"effect": "return_fresh_owned",
18+
"provenance": "BODY_PROVED",
19+
"assembly": {
20+
"name": "RLibA",
21+
"mvid": "a972665e-5b5e-420c-806d-90011486d0cb"
22+
},
23+
"derived_from": "fixture: FA.FactoryAsync() => Task.FromResult(new R()); the logical result is minted"
24+
},
25+
{
26+
"callable": "RLibA.FA.FactoryValueTaskAsync",
27+
"effect": "return_fresh_owned",
28+
"provenance": "BODY_PROVED",
29+
"assembly": {
30+
"name": "RLibA",
31+
"mvid": "a972665e-5b5e-420c-806d-90011486d0cb"
32+
},
33+
"derived_from": "fixture: FA.FactoryValueTaskAsync() => new ValueTask<R>(new R()); the logical result is minted"
34+
}
35+
]
36+
}

0 commit comments

Comments
 (0)