ownership-semantics-lab: discovery experiment records for 22 libraries, tier-2 pipeline runs, overlap repros (research-only)

Adds the per-library S1..S8 artefacts of the six tier-2 libraries (K4os, ZstdSharp,
Google.Protobuf, Serilog, NLog, Microsoft.Data.Sqlite.Core), the tier-2 witness rows
and results, the updated ledger/triage/record, the compare/record/triage scripts and
the Serilog and K4os overlap repros. The Own.NET expected outputs of the six earlier
repros had been committed empty (bookkeeping slip); regenerated from the recorded facts.
No production code changes.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Am9eQwzNfbugH72eVKetC2

Author: claude

corpus/ownership-lab/README.md

@@ -15,7 +15,9 @@ probes, discovery protocol and results).
 | `h16/` | the Z3 symbolic probe and the complementary-guard fixture |
 | `h20/` | F3 (throw-exit versus bare return) with observed outputs off/on |
 | `witness/` | the runtime-witness generator (`gen.py`), its ten rows and results |
-| `discovery/` | the discovery-experiment pipeline scripts (acquire, API surface, fetch, derive, consumers, scan) |
+| `discovery/` | the discovery-experiment pipeline scripts (acquire, API surface, fetch, derive, compare, consumers, scan, triage, record) |
+| `discovery/records/` | the per-library S1..S8 artefacts of the 22 completed libraries (acquire/identity, API surface, LLM candidates written before bodies, pinned source digests, derivation summary, applied rows, consumer file digests, OFF/KEY scan results), the ledger, the triage file and the witness rows/results |
+| `discovery/repros/` | one minimal repro per new finding class with the expected outputs of Own.NET OFF/KEY, IDisposableAnalyzers and CA2000 |
 
 Tools: `frontend/roslyn/OwnSharp.AsmId` (assembly identity facets), `frontend/roslyn/OwnSharp.ApiList`
 (public resource-bearing API surface). Scratch paths inside the scripts point at the session

corpus/ownership-lab/discovery/compare.py

@@ -0,0 +1,45 @@
+"""discovery S7: per library, compare the LLM arm (S3 SUGGESTED) with the proofs (S5 BODY_PROVED) and the witnesses
+(S6), assemble rows-applied.json (BODY_PROVED + WITNESSED, MVID-pinned) and the per-library ledger."""
+import sys, os, json, glob
+S='/tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad'; D=f'{S}/lab/disc'
+wit={}
+for f in (f'{D}/witness-results-libs.json', f'{D}/libs/Npgsql/s6-witness-results.json', f'{D}/witness-results-tier2.json'):
+    if os.path.exists(f):
+        for r in json.load(open(f)): wit.setdefault(r['callable'],[]).append(r)
+out={}
+for acq in sorted(glob.glob(f'{D}/libs/*/acquire.json')):
+    L=os.path.dirname(acq); pid=os.path.basename(L); a=json.load(open(acq)); mvid=(a.get('identity') or {}).get('mvid')
+    proved=json.load(open(f'{L}/rows-bodyproved.json'))['entries'] if os.path.exists(f'{L}/rows-bodyproved.json') else []
+    base=json.load(open(f'{L}/rows-bodyproved-base.json'))['entries'] if os.path.exists(f'{L}/rows-bodyproved-base.json') else None
+    s3=json.load(open(f'{L}/s3-llm-candidates.json')) if os.path.exists(f'{L}/s3-llm-candidates.json') else {'suggested_rows':[],'suggested_negatives':[]}
+    pk={(e['callable'],e['effect']) for e in proved}
+    llm=[(r['callable'],r['effect']) for r in s3['suggested_rows']]
+    admitted_proof=[c for c in llm if c in pk]
+    witnessed=[]; wit_rows=[]
+    for r in wit.get('',[]): pass
+    for cal,rs in wit.items():
+        if not cal.startswith(tuple({e['callable'].rsplit('.',2)[0] for e in proved} | {x[0].rsplit('.',2)[0] for x in llm} | {pid})): pass
+    for cal,rs in wit.items():
+        for r in rs:
+            if r.get('verdict')=='fresh' and (cal,'return_fresh_owned') not in pk and (r.get('asm')==mvid or pid in cal or cal.startswith(pid.split('.')[0])):
+                if not any(w['callable']==cal for w in wit_rows):
+                    wit_rows.append({'callable':cal,'effect':'return_fresh_owned','provenance':'WITNESSED','assembly':{'name':a['package'],'mvid':mvid},'witness':r['id'],'witness_asm_mvid':r.get('asm')})
+    wit_rows=[w for w in wit_rows if w['witness_asm_mvid']==mvid]
+    # the pin must name the ASSEMBLY (simple name), not the package id (SSH.NET -> Renci.SshNet, SharpZipLib -> ICSharpCode.SharpZipLib);
+    # constructor 'callables' from the witness list are objects, not factory rows
+    asm_name=(a.get('identity') or {}).get('name') or a['package']
+    wit_rows=[w for w in wit_rows if not w['callable'].endswith('..ctor')]
+    for e in proved+wit_rows: e.setdefault('assembly',{})['name']=asm_name
+    applied=proved+wit_rows
+    json.dump({'schema':'own.net/re-oracle/v1','label':f'discovery APPLIED rows for {pid} {a["version"]} (BODY_PROVED + WITNESSED; MVID {mvid})','entries':applied}, open(f'{L}/rows-applied.json','w'), indent=1)
+    wl=[(c,e) for c,e in llm]
+    admitted_wit=[c for c in wl if any(w['callable']==c[0] for w in wit_rows)]
+    rejected=[c for c in wl if c not in pk and not any(w['callable']==c[0] for w in wit_rows)]
+    wit_all=[r for cal,rs in wit.items() for r in rs if r.get('asm')==mvid or (cal.split('.')[0] in pid)]
+    out[pid]={'version':a['version'],'mvid':mvid,'body_proved_rows':len(proved),'body_proved_rows_before_H20':(len(base) if base is not None else None),'witnessed_rows_added':len(wit_rows),'applied_rows':len(applied),
+              'llm_candidates':len(llm),'llm_admitted_by_proof':len(admitted_proof),'llm_admitted_by_witness':len(admitted_wit),'llm_rejected_or_undecidable':len(rejected),
+              'proved_not_suggested_by_llm':len([e for e in proved if (e['callable'],e['effect']) not in set(llm)]),
+              'witness_runs':[{k:r.get(k) for k in ('id','callable','verdict','expect')} for r in wit_all],
+              'llm_rejected_list':[c[0] for c in rejected]}
+json.dump(out, open(f'{D}/s7-ledger.json','w'), indent=1)
+for pid,v in out.items(): print(pid, {k:v[k] for k in ('body_proved_rows','body_proved_rows_before_H20','witnessed_rows_added','applied_rows','llm_candidates','llm_admitted_by_proof','llm_admitted_by_witness','llm_rejected_or_undecidable','proved_not_suggested_by_llm')})

corpus/ownership-lab/discovery/derive.py

@@ -4,6 +4,7 @@
 import sys, os, json, subprocess, glob, re
 S='/tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad'; R='/home/user/Own.NET'
 pid=sys.argv[1]; d=f'{S}/lab/disc/libs/{pid}'; acq=json.load(open(f'{d}/acquire.json'))
+open(f'{d}/src/__GlobalUsings.cs','w').write('// synthesised for the discovery derivation: the SDK implicit usings (ImplicitUsings=enable) the fetched files rely on\nglobal using System;\nglobal using System.Collections.Generic;\nglobal using System.IO;\nglobal using System.Linq;\nglobal using System.Net.Http;\nglobal using System.Threading;\nglobal using System.Threading.Tasks;\n')
 src=sorted(glob.glob(f'{d}/src/**/*.cs', recursive=True))
 env={**os.environ,'PATH':'/root/.dotnet:'+os.environ['PATH'],'DOTNET_NOLOGO':'1','DOTNET_CLI_TELEMETRY_OPTOUT':'1','PYTHONPATH':R,
      'OWEN_RE_BODY':'1','OWEN_RE_MINTED_RETURN':'1','OWEN_RE_MIXED_RETURN':'1','OWEN_RE_DUMP_EFFECTS':f'{d}/dump.json'}
@@ -16,6 +17,27 @@
 summ=subprocess.run(['python3','-m','ownlang','summaries',f'{d}/facts.json'],cwd=R,capture_output=True,text=True,env=env).stdout
 try: summaries=json.loads(summ)['summaries']
 except Exception: summaries=[]
+# per-file union (E1/E2 proofs are local to a method body; a curated source SUBSET can make a created type's
+# declaration incomplete and lose the whole-set record, so each file is also derived alone against the package
+# assembly and the fresh/release results are unioned; the provenance stays BODY_PROVED)
+perfile_fresh=set(); perfile_rel=[]
+for f in src:
+    argv1=['dotnet',f'{R}/frontend/roslyn/OwnSharp.Extractor/bin/Release/net8.0/ownsharp-extract.dll','--flow-locals',f,'-o',f'{d}/facts.one.json']
+    if refdir: argv1+=['--ref-dir',refdir]
+    e1={**env,'OWEN_RE_DUMP_EFFECTS':f'{d}/dump.one.json'}
+    subprocess.run(argv1,cwd=R,capture_output=True,text=True,env=e1)
+    s1=subprocess.run(['python3','-m','ownlang','summaries',f'{d}/facts.one.json'],cwd=R,capture_output=True,text=True,env=env).stdout
+    try:
+        for s in json.loads(s1)['summaries']:
+            if s.get('returns',{}).get('owned')=='fresh': perfile_fresh.add(s['method'])
+    except Exception: pass
+    try:
+        for e in json.load(open(f'{d}/dump.one.json')).get('receiver_release',[]):
+            if e.get('releases'): perfile_rel.append(e)
+    except Exception: pass
+whole_fresh={s['method'] for s in summaries if s.get('returns',{}).get('owned')=='fresh'}
+for m in sorted(perfile_fresh-whole_fresh):
+    summaries.append({'method':m,'returns':{'owned':'fresh'},'source':'inferred (per-file run)'})
 api=json.load(open(f'{d}/api.json')) if os.path.exists(f'{d}/api.json') else {'factories':[],'release_name_candidates':[],'types':[]}
 public_callables={f['callable'] for f in api['factories']} | {r['callable'] for r in api['release_name_candidates']} | {f"{t['type']}.Dispose" for t in api['types']}
 public_types={t['type'] for t in api['types']}
@@ -29,6 +51,9 @@
         if m in public_callables and (m,'fresh') not in seen:
             seen.add((m,'fresh')); rows.append({'callable':m,'effect':'return_fresh_owned','provenance':'BODY_PROVED','assembly':{'name':asm,'mvid':mvid},'derived_from':f"{acq.get('repository_url')}@{acq.get('repository_commit')} via E1/E3 ({s.get('source')})"})
 dump=json.load(open(f'{d}/dump.json')) if os.path.exists(f'{d}/dump.json') else {}
+seen_rel={(e['callable'],e.get('arity')) for e in dump.get('receiver_release',[])}
+for e in perfile_rel:
+    if (e['callable'],e.get('arity')) not in seen_rel: dump.setdefault('receiver_release',[]).append(e); seen_rel.add((e['callable'],e.get('arity')))
 for e in dump.get('receiver_release',[]):
     if e.get('releases') and e['callable'] in public_callables and not e['callable'].endswith('.Dispose') and (e['callable'],e.get('arity')) not in seen:
         seen.add((e['callable'],e.get('arity'))); rows.append({'callable':e['callable'],'effect':'receiver_terminal_release','arity':e.get('arity'),'provenance':'BODY_PROVED','assembly':{'name':asm,'mvid':mvid},'derived_from':f"{acq.get('repository_url')}@{acq.get('repository_commit')} via E2"})
@@ -38,6 +63,6 @@
 fresh_all=[s['method'] for s in summaries if s.get('returns',{}).get('owned')=='fresh']
 fresh_public_missing=[s['method'] for s in summaries if s.get('returns',{}).get('owned')=='fresh' and s['method'].split('(')[0] not in public_callables]
 rel_all=[e['callable'] for e in dump.get('receiver_release',[]) if e.get('releases')]
-json.dump({'source_files':len(src),'extractor_stats':stats,'re_body_census':census.group(1) if census else None,'fresh_summaries_all':fresh_all,'receiver_release_all':rel_all,'fresh_not_public_surface':fresh_public_missing,'instance_methods_evaluated':dump.get('instance_methods_evaluated'),'public_rows':len(rows)},open(f'{d}/derive-summary.json','w'),indent=1)
+json.dump({'source_files':len(src),'perfile_union_added_fresh':sorted(perfile_fresh-whole_fresh),'extractor_stats':stats,'re_body_census':census.group(1) if census else None,'fresh_summaries_all':fresh_all,'receiver_release_all':rel_all,'fresh_not_public_surface':fresh_public_missing,'instance_methods_evaluated':dump.get('instance_methods_evaluated'),'public_rows':len(rows)},open(f'{d}/derive-summary.json','w'),indent=1)
 print(json.dumps({'package':pid,'files':len(src),'stats':stats,'census':census.group(1) if census else None,'fresh_all':len(fresh_all),'release_all':len(rel_all),'public_rows':len(rows)}))
 for x in rows: print('  ROW', x['effect'], x['callable'], x.get('arity',''))

corpus/ownership-lab/discovery/derive_tier2.sh

@@ -0,0 +1,7 @@
+#!/usr/bin/env bash
+export PATH=/root/.dotnet:$PATH DOTNET_CLI_TELEMETRY_OPTOUT=1 DOTNET_NOLOGO=1 OWEN_LAB_THROWEXIT=1
+S=/tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad; cd $S/lab/disc
+for p in ZstdSharp.Port Google.Protobuf Serilog K4os.Compression.LZ4.Streams NLog Microsoft.Data.Sqlite.Core; do
+  extra=""; [ "$p" = "Microsoft.Data.Sqlite.Core" ] && extra=$(ls -d $S/lab/disc/deps/SQLitePCLRaw.core/lib/netstandard2.0 2>/dev/null)
+  OWN_EXTRA_REF_DIRS="$extra" python3 derive.py $p 2>&1 | head -1 | python3 -c "import sys,json; d=json.loads(sys.stdin.read()); print(d['package'],'rows',d['public_rows'],'fresh_all',d['fresh_all'],'release_all',d['release_all'])"
+done; echo DERIVE_TIER2_DONE

corpus/ownership-lab/discovery/record.py

@@ -0,0 +1,36 @@
+"""discovery: assemble the per-library record (S1..S10) into discovery-v1.json from the pipeline artefacts and the
+experimenter's triage file (triage.json: {"<pid>/<tag>": [{"finding": [file,line,code], "verdict": TRUE|BENIGN|FALSE,
+"root_cause": ..., "severity": ..., "overlap": ..., "note": ...}]})."""
+import json, os, glob, hashlib, datetime, collections
+S='/tmp/claude-0/-home-user/8a9da608-aa27-5449-8306-1fae9426f9b9/scratchpad'; D=f'{S}/lab/disc'
+OD=collections.OrderedDict
+ledger=json.load(open(f'{D}/s7-ledger.json')) if os.path.exists(f'{D}/s7-ledger.json') else {}
+triage=json.load(open(f'{D}/triage.json')) if os.path.exists(f'{D}/triage.json') else {}
+libs=OD()
+for acq in sorted(glob.glob(f'{D}/libs/*/acquire.json')):
+    L=os.path.dirname(acq); pid=os.path.basename(L); a=json.load(open(acq))
+    api=json.load(open(f'{L}/api.json')) if os.path.exists(f'{L}/api.json') else {}
+    s3=json.load(open(f'{L}/s3-llm-candidates.json')) if os.path.exists(f'{L}/s3-llm-candidates.json') else {}
+    s4=json.load(open(f'{L}/s4-source.json')) if os.path.exists(f'{L}/s4-source.json') else {}
+    ds=json.load(open(f'{L}/derive-summary.json')) if os.path.exists(f'{L}/derive-summary.json') else {}
+    rows=json.load(open(f'{L}/rows-applied.json'))['entries'] if os.path.exists(f'{L}/rows-applied.json') else []
+    scans=OD()
+    for sc in sorted(glob.glob(f'{L}/s8-scan-*.json')):
+        r=json.load(open(sc)); tag=r['consumer']
+        cons=json.load(open(f'{L}/s8-consumers-{tag}.json')) if os.path.exists(f'{L}/s8-consumers-{tag}.json') else {}
+        scans[tag]=OD([("files_scanned",r['files']),("files_fetched",len([x for x in cons.get('files',[]) if 'sha256' in x])),("off_findings",len(r['off']['findings'])),("key_findings",len(r['key_arm']['findings'])),("new",r['new_findings']),("lost",r['lost_findings']),("python_equals_rust",r['off']['python_equals_rust'] and r['key_arm']['python_equals_rust']),("key_census",r['key_arm']['census']),("triage",triage.get(f'{pid}/{tag}',[]))])
+    adopt_bool=[c for c in api.get('adopting_ctors',[]) if c.get('bool_params')]
+    if not a.get('main_assembly'):
+        libs[pid]=OD([("version",a['version']),("nupkg_sha256",a['nupkg_sha256']),("status","meta-package without a lib assembly; substituted by Microsoft.Data.Sqlite.Core "+a['version']+" (the assembly-bearing package); not counted as a completed library")]); continue
+    libs[pid]=OD([
+        ("version",a['version']),("nupkg_sha256",a['nupkg_sha256']),("repository",a.get('repository_url')),("commit_pin",a.get('repository_commit') or 'tag (no nuspec commit)'),("assembly_mvid",(a.get('identity') or {}).get('mvid')),
+        ("S2_surface",OD([("disposable_types",api.get('disposable_types')),("factory_candidates",len(api.get('factories',[]))),("adopting_ctors",len(api.get('adopting_ctors',[]))),("adopting_ctors_with_bool",len(adopt_bool)),("release_name_candidates",len(api.get('release_name_candidates',[])))])),
+        ("S3_llm",OD([("suggested_rows",len(s3.get('suggested_rows',[]))),("suggested_negatives",len(s3.get('suggested_negatives',[]))),("written_before_bodies",s3.get('written_before_bodies'))])),
+        ("S4_source",OD([("files_fetched",len([f for f in s4.get('files',[]) if 'sha256' in f])),("files_requested",len(s4.get('files',[])))])),
+        ("S5_derivation",OD([("extractor_stats",ds.get('extractor_stats')),("re_body_census",ds.get('re_body_census')),("fresh_summaries_all",len(ds.get('fresh_summaries_all',[]))),("perfile_union_added",len(ds.get('perfile_union_added_fresh',[]))),("public_body_proved_rows",ds.get('public_rows'))])),
+        ("S6_S7",ledger.get(pid,{})),
+        ("applied_rows",[OD([("callable",e['callable']),("effect",e['effect']),("provenance",e['provenance'])]) for e in rows]),
+        ("S8_scans",scans),
+    ])
+json.dump(OD([("schema","own.net/ownership-lab/discovery/v1"),("generated_utc",datetime.datetime.utcnow().strftime('%Y-%m-%dT%H:%M:%SZ')),("libraries",libs)]), open(f'{D}/discovery-libs.json','w'), indent=1)
+print('libraries recorded:', len(libs))