NEVER-MERGE: BQ-11 import inventory profile only

.github/workflows/fold-affine-bridge.yml

@@ -1,4 +1,4 @@
-name: Exact fold affine bridge companion
+name: NEVER-MERGE fold import inventory diagnostic
 'on':
   pull_request:
     paths:
@@ -15,9 +15,9 @@ name: Exact fold affine bridge companion
 permissions:
   contents: read
 jobs:
-  fold-affine-bridge:
+  import-inventory-only:
     runs-on: ubuntu-latest
-    timeout-minutes: 25
+    timeout-minutes: 10
     env:
       LEAN_NUM_THREADS: 2
     steps:
@@ -35,13 +35,13 @@ jobs:
           lint: 'false'
           use-mathlib-cache: 'true'
           use-github-cache: 'false'
-      - name: Check primary package and separate exact fold contracts
-        run: python3 -B -S companions/fold_affine_bridge_20261006/replay.py execute
+      - name: Measurement only - no fresh replay or proof receipt
+        run: python3 -B -S companions/fold_affine_bridge_20261006/replay.py profile
       - name: Preserve original success or failure evidence
         if: always()
         uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a
         with:
-          name: fold-affine-bridge-${{ github.run_id }}-${{ github.run_attempt }}
+          name: fold-import-profile-${{ github.run_id }}-${{ github.run_attempt }}
           path: |
             .lake/fold-affine-bridge-evidence/
             formal/.lake/formal-evidence/

companions/fold_affine_bridge_20261006/README.md

@@ -1,3 +1,33 @@
+# NEVER-MERGE diagnostic carrier: import inventory only
+
+This separate carrier is authorized by
+https://github.com/d6g8k5htny-coder/Math-/pull/389#issuecomment-6029010837.
+PR389 and frozen candidate9c3246ddc22783b3933d6125798a19cbce4a7b4b stay unchanged.
+Only replay/test/README/SOURCE_FILES and the dedicated workflow differ here;
+FoldAffineBridge.lean and Contract.lean must remain byte-identical.
+
+Exactly one profile-only hosted job, maximum10minutes; each profile<=90seconds.
+No leanchecker, fresh replay, negative/full-suite result or proof receipt is
+produced by the profile command. A successful inventory is measurement only.
+The ordinary execute command remains defined but is not invoked on this carrier.
+No merge or mathematical acceptance is authorized.
+
+The generated temporary Lean program calls the pinned withImportModules API
+and counts the same map1 constants and unsafe/partial exclusion used by pinned
+Lean.Replay. It does not replay declarations. It records actual module names,
+resolved .olean paths, effective Lean environment paths and binary/version.
+Import-load wall milliseconds are measured inside withImportModules;
+GNU-time CPU/maximum RSS/elapsed values cover the entire profile process,
+including Lean startup and counting. Those resource scopes are kept distinct.
+Failure stdout/stderr/status and any partial resource output are retained.
+
+The sole intended command is:
+
+    python3 -B -S companions/fold_affine_bridge_20261006/replay.py profile
+
+The preserved mathematical source scope and prior failures follow below;
+they are not new verification claims for this diagnostic carrier.
+
 # Exact fold derivatives and affine coordinates
 
 Scientific effect: NONE. Author: OpenAI, `fold-affine-bridge-author-20261006`,

companions/fold_affine_bridge_20261006/SOURCE_FILES.json

@@ -8,9 +8,9 @@
   ],
   "files": {
     ".github/workflows/fold-affine-bridge.yml": {
-      "bytes": 1684,
-      "git_blob": "c35ae86d1d74c8ee7aad9df4b0c7e55718d51ac0",
-      "sha256": "33dd9770af74c79461372089ef18eef0451a67d8a6db3c514259285be8c25299"
+      "bytes": 1694,
+      "git_blob": "0f59d8b851fd4673655a338673e1ca32c4b28b9b",
+      "sha256": "058337051b2105c122e42d3bae0dcc44c9bf43e9911b165803eb5f5ab605a462"
     },
     "companions/fold_affine_bridge_20261006/Contract.lean": {
       "bytes": 5724,
@@ -23,19 +23,19 @@
       "sha256": "e43c0d2084590b564618d9774feae9a40a24a31deb5227b66b6e54901ada56ea"
     },
     "companions/fold_affine_bridge_20261006/README.md": {
-      "bytes": 8682,
-      "git_blob": "caf8daeec44a41763a679fb8071cf5d8b6a5572b",
-      "sha256": "e8a6ef8549e2de79609d0d5e4117bf779cc7a2839befce66baa34f7b21d0584a"
+      "bytes": 10303,
+      "git_blob": "02616ecb5bd8286650d1b70f3f2de13e3861571a",
+      "sha256": "c9cbffe257d1505edb3963ff119b09056d2034b9b0de0099cba517f71ddd3eb2"
     },
     "companions/fold_affine_bridge_20261006/replay.py": {
-      "bytes": 12704,
-      "git_blob": "c382ca9373e1208bb0cfb2f115b55eeba6d07526",
-      "sha256": "bd9469efa4b50eee11be46b3711d25abe412b52941c6cee5a9e23c864932a301"
+      "bytes": 17581,
+      "git_blob": "622f720082146c3e2a71ec9c9814f5046da0387f",
+      "sha256": "839cff0951b03070dd2a64cb2d6ce7e7215849fb48da8e431dbb4f0befc620f2"
     },
     "companions/fold_affine_bridge_20261006/test_contract.py": {
-      "bytes": 5651,
-      "git_blob": "77db54dc107a6ba328ad50b4ae14e19148f8ce78",
-      "sha256": "992b6fc162f0546e370c00af6d479771f4d9d680cfebd308977e4255ac9c6c88"
+      "bytes": 6806,
+      "git_blob": "b7691a4db48c64c0e5801312a6f1ca649d096b61",
+      "sha256": "f51fa7a971eea426f35bcebc93cbed63a8039da829f474bc1c2c060574b21e6e"
     }
   },
   "scientific_effect": "NONE",

companions/fold_affine_bridge_20261006/replay.py

@@ -187,9 +187,80 @@ def lean(label,args,success=True):
     (out/'receipt.json').write_text(json.dumps(result,sort_keys=True,indent=2)+'\n')
     return result
 
+PROFILE_TARGETS=('ResearchFormalCoreR1.AlgebraV2','ResearchFormalCoreR1.D2Schur','FoldAffineBridge')
+FROZEN_CANDIDATE='9c3246ddc22783b3933d6125798a19cbce4a7b4b'
+
+def profile_program(target):
+    require(target in PROFILE_TARGETS,'unknown profile target')
+    return r'''import Lean
+open Lean
+unsafe def main : IO Unit := do
+  initSearchPath (← findSysroot)
+  let target : Name := `TARGET
+  let started ← IO.monoMsNow
+  withImportModules #[{ module := target }] {} fun env => do
+    let loaded ← IO.monoMsNow
+    let cs := env.constants.map₁
+    let mut eligible : Nat := 0
+    for (_, ci) in cs.toList do
+      if !ci.isUnsafe && !ci.isPartial then
+        eligible := eligible + 1
+    IO.println s!"BQ_PROFILE module={target} loaded_modules={env.header.moduleNames.size} constants={cs.size} eligible={eligible} import_load_ms={loaded - started}"
+    for name in [`FoldAffineBridge, `ResearchFormalCoreR1.AlgebraV2, `ResearchFormalCoreR1.D2Schur, `Mathlib, `Mathlib.Tactic] do
+      let path ← findOLean name
+      IO.println s!"BQ_OLEAN module={name} path={path}"
+'''.replace('TARGET',target)
+
+def parse_profile(text,target):
+    pattern=r'^BQ_PROFILE module=([A-Za-z0-9_.]+) loaded_modules=([0-9]+) constants=([0-9]+) eligible=([0-9]+) import_load_ms=([0-9]+)$'
+    matches=re.findall(pattern,text,re.M)
+    require(len(matches)==1,'missing/duplicate/malformed profile')
+    name,*values=matches[0]
+    require(name==target,'profile target mismatch')
+    result={'module':name,**dict(zip(('loaded_modules','constants','eligible','import_load_ms'),map(int,values)))}
+    require(0<result['constants'] and result['eligible']<=result['constants'],'invalid constant inventory')
+    return result
+
+def profile(out):
+    require(not out.exists(),'output already exists');out.mkdir(parents=True)
+    before=source();(out/'source.json').write_text(json.dumps(before,sort_keys=True,indent=2)+'\n')
+    for name in ('FoldAffineBridge.lean','Contract.lean'):
+        require(git('rev-parse','HEAD:'+PACKAGE+'/'+name)==git('rev-parse',FROZEN_CANDIDATE+':'+PACKAGE+'/'+name),'frozen proof/contract changed')
+    require(Path('/usr/bin/time').is_file(),'GNU time unavailable; no resource measurement')
+    run_process(out,'profile-driver-tests',[sys.executable,'-B','-S',str(SIDE/'test_contract.py')],timeout=30)
+    run_process(out,'setup-import-build',['lake','build','ResearchFormalCoreR1.AlgebraV2','ResearchFormalCoreR1.D2Schur'],timeout=120,cwd=ROOT/'formal')
+    build=out/'build';build.mkdir()
+    env={**os.environ,'BQ_BUILD':str(build),'BQ_SIDE':str(SIDE),'LC_ALL':'C'}
+    prefix=['lake','env','bash','-c','export LEAN_PATH="$BQ_BUILD:$BQ_SIDE:${LEAN_PATH:-}"; export LEAN_SRC_PATH="$BQ_SIDE:${LEAN_SRC_PATH:-}"; exec "$@"','--']
+    def command(label,args,timeout=90):
+        return run_process(out,label,prefix+args,timeout=timeout,cwd=ROOT/'formal',env=env)
+    command('toolchain',['lean','--version'],30)
+    command('lean-prefix',['lean','--print-prefix'],30)
+    command('effective-paths',[sys.executable,'-c','import os,json,shutil; print(json.dumps({"LEAN_PATH":os.environ.get("LEAN_PATH"),"LEAN_SRC_PATH":os.environ.get("LEAN_SRC_PATH"),"lean_command":shutil.which("lean"),"lake_command":shutil.which("lake")},sort_keys=True))'],30)
+    binary=Path((out/'lean-prefix.stdout').read_text().strip())/'bin/lean'
+    require(binary.is_file(),'reported Lean binary missing')
+    (out/'lean-binary.json').write_text(json.dumps({'path':str(binary.resolve()),**identity(binary.read_bytes())},sort_keys=True,indent=2)+'\n')
+    command('setup-candidate-build',['lean','-DwarningAsError=true','--root='+str(SIDE),'-o',str(build/'FoldAffineBridge.olean'),str(SIDE/'FoldAffineBridge.lean')])
+    records=[]
+    for index,target in enumerate(PROFILE_TARGETS):
+        label='import-profile-'+str(index)
+        program=out/(label+'.lean');program.write_text(profile_program(target))
+        resource_file=out/(label+'.resource.json')
+        fmt='{"user_seconds":%U,"system_seconds":%S,"maxrss_kib":%M,"elapsed_seconds":%e,"exit_code":%x}'
+        command(label,['/usr/bin/time','-f',fmt,'-o',str(resource_file),'lean','--run',str(program)])
+        record=parse_profile((out/(label+'.stdout')).read_text(),target)
+        record['whole_process_resources']=strict_json(resource_file.read_bytes())
+        record['scope_note']='Import-load milliseconds are internal; CPU/RSS and elapsed resource values include Lean startup and inventory work. No kernel replay.'
+        records.append(record)
+    require(source()==before,'source changed during profile')
+    result={**before,'frozen_candidate':FROZEN_CANDIDATE,'diagnostic_only':True,'fresh_replay_run':False,'proof_receipt':False,'profiles':records}
+    (out/'profile.json').write_text(json.dumps(result,sort_keys=True,indent=2)+'\n')
+    return result
+
+
 def main():
-    ap=argparse.ArgumentParser(description=__doc__);ap.add_argument('command',choices=('source','controls','execute'))
+    ap=argparse.ArgumentParser(description=__doc__);ap.add_argument('command',choices=('source','controls','execute','profile'))
     ap.add_argument('--out',type=Path,default=ROOT/'.lake/fold-affine-bridge-evidence');a=ap.parse_args()
-    result=source() if a.command=='source' else rational_controls() if a.command=='controls' else execute(a.out.resolve())
+    result=source() if a.command=='source' else rational_controls() if a.command=='controls' else profile(a.out.resolve()) if a.command=='profile' else execute(a.out.resolve())
     print(json.dumps(result,sort_keys=True,indent=2))
 if __name__=='__main__':main()

companions/fold_affine_bridge_20261006/test_contract.py

@@ -19,6 +19,25 @@ def api(self,name):
         self.assertTrue(callable(getattr(replay,name,None)), 'missing driver behavior '+name)
         return getattr(replay,name)
 
+    def test_profile_program_is_inventory_only(self):
+        fn=self.api('profile_program')
+        for target in ('ResearchFormalCoreR1.AlgebraV2','ResearchFormalCoreR1.D2Schur','FoldAffineBridge'):
+            program=fn(target)
+            self.assertIn('withImportModules',program)
+            self.assertIn('!ci.isUnsafe && !ci.isPartial',program)
+            self.assertNotIn('replay',program)
+            self.assertNotIn('leanchecker',program)
+        with self.assertRaises(ValueError):fn('Other')
+
+    def test_profile_parser_is_strict(self):
+        fn=self.api('parse_profile')
+        raw='BQ_PROFILE module=FoldAffineBridge loaded_modules=10 constants=30 eligible=20 import_load_ms=4\n'
+        got=fn(raw,'FoldAffineBridge')
+        self.assertEqual(got,{'module':'FoldAffineBridge','loaded_modules':10,'constants':30,'eligible':20,'import_load_ms':4})
+        for bad in [raw+raw,raw.replace('eligible=20','eligible=31'),raw.replace('import_load_ms=4','import_load_ms=NaN'),'']:
+            with self.assertRaises(ValueError):fn(bad,'FoldAffineBridge')
+        with self.assertRaises(ValueError):fn(raw,'ResearchFormalCoreR1.AlgebraV2')
+
     def test_absolute_value_token_spacing(self):
         for name in ('FoldAffineBridge.lean','Contract.lean'):
             with self.subTest(name=name):