1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
| import fs from 'node:fs';
| import path from 'node:path';
| import crypto from 'node:crypto';
| import {pathToFileURL} from 'node:url';
| import * as runtime from './detail_strengthening_p0_gap_closure_verification_runtime_20260731.mjs';
| import {parseAuthorityCsv,serializeCsv,serializeManifestDataRows} from './artifact_manifest_append_stable_parser_repair001_20260730.mjs';
|
| const ROOT=runtime.ROOT;
| const DESIGN_DOC='ana-doc/机器人案例/案例分析设计.md';
| const BUILDER='dev/ana-dev/detail_strengthening_p0_gap_closure_verification_design_20260731.mjs';
| const NEGATIVE=`${runtime.BASE}/evidence/detail_strengthening_p0_gap_closure_verification_negative_results_20260731.csv`;
| const DESIGN_SET=`${runtime.BASE}/manifest/detail_strengthening_p0_gap_closure_verification_design_artifact_set_20260731.csv`;
| const REVIEW_REQUEST=`${runtime.BASE}/manifest/review_request_detail_strengthening_p0_gap_closure_verification_design_20260731.md`;
| const DESIGN_VALIDATION=`${runtime.BASE}/manifest/detail_strengthening_p0_gap_closure_verification_design_validation_20260731.csv`;
| const DESIGN_SET_COLUMNS=runtime.EXEC_SET_COLUMNS;
| const NEGATIVE_COLUMNS=['test_id','mutation_applied','oracle','expected','expected_code','actual','actual_codes','result'];
| const abs=value=>path.join(ROOT,...value.split('/'));
| const hash=value=>crypto.createHash('sha256').update(value).digest('hex');
| const normalize=value=>value.toString('utf8').replace(/^\uFEFF/,'').replace(/\r\n/g,'\n').replace(/\r/g,'\n');
| const lineCount=value=>{const text=normalize(value);return text.split('\n').length-(text.endsWith('\n')?1:0);};
| const readCsv=logical=>{const parsed=parseAuthorityCsv(normalize(fs.readFileSync(abs(logical))));if(parsed.errors.length)throw new Error(`CSV:${logical}:${parsed.errors.join('|')}`);return parsed;};
| const identity=logical=>{const buffer=fs.readFileSync(abs(logical)),stat=fs.statSync(abs(logical));return{rows:logical.endsWith('.csv')?readCsv(logical).rows.length:lineCount(buffer),bytes:buffer.length,sha256:hash(buffer),mtime:new Date(Math.trunc(stat.mtimeMs)).toISOString(),mtimeMs:Math.trunc(stat.mtimeMs)};};
| const write=(logical,text)=>{fs.mkdirSync(path.dirname(abs(logical)),{recursive:true});fs.writeFileSync(abs(logical),text,'utf8');};
| const exactColumns=(parsed,columns,code)=>parsed.header.join('|')===columns.join('|')?[]:[`${code}_COLUMNS`];
| const compareRows=(actual,expected,columns,code)=>{const errors=[];if(actual.length!==expected.length)return[`${code}_COUNT:${actual.length}:${expected.length}`];for(let i=0;i<expected.length;i++)for(const column of columns)if(String(actual[i]?.[column]??'')!==String(expected[i]?.[column]??'')){errors.push(`${code}_FIELD:${i+1}:${column}`);break;}return errors;};
|
| function formalEntry(){const lines=normalize(fs.readFileSync(abs(DESIGN_DOC))).split('\n'),heading=`## ${runtime.DESIGN_ID}（2026-07-31）`,start=lines.findIndex(line=>line===heading);if(start<0)throw new Error('FORMAL_DESIGN_ENTRY_MISSING');let end=lines.length;for(let i=start+1;i<lines.length;i++)if(lines[i].startsWith('## ')){end=i;break;}while(end>start&&lines[end-1]==='')end--;const buffer=Buffer.from(`${lines.slice(start,end).join('\n')}\n`);return{start:start+1,end,lines:end-start,bytes:buffer.length,sha256:hash(buffer)};}
| function formalEntryRow(){const entry=formalEntry();return{authority_id:'P0GCV-FORMAL-ENTRY-001',design_id:runtime.DESIGN_ID,artifact_path:DESIGN_DOC,start_line:String(entry.start),end_line:String(entry.end),lines:String(entry.lines),bytes:String(entry.bytes),sha256:entry.sha256,normalization:'UTF8_NO_BOM_LF_JOIN_LINES_WITH_TERMINAL_LF_V1',required_markers:'FROZEN_LOCAL_INPUTS_ONLY_NO_NETWORK|PARTIAL_SCOPE_SUPPORTED_GAP_REMAINS_OPEN|NO_ACCEPTED_REFERENCE_GAP_REMAINS_OPEN|PENDING_VERIFICATION_MAX_NO_UPGRADE|NO_AUTOMATIC_FORMAL_POOL_CHANGE|NO_UPGRADE|P0_gap_closure_verification_execution_release=NOT_RELEASED'};}
| function designSetRows(){const paths=[BUILDER,runtime.SCRIPT,runtime.SOURCE_ENTRY_AUTHORITY,runtime.CRITERIA,runtime.DECISION_AUTHORITY,runtime.OCCURRENCE_AUTHORITY,runtime.NEXT_EVIDENCE_AUTHORITY,runtime.CONTRACT,runtime.SCHEMA,runtime.EXEC_SET,runtime.FORMAL_ENTRY_AUTHORITY,runtime.DESIGN_BASELINE,NEGATIVE,REVIEW_REQUEST,DESIGN_VALIDATION],roles=['DESIGN_BUILDER','EXECUTION_RUNTIME','SOURCE_AUDIT_AUTHORITY','GAP_CLOSURE_CRITERIA','DECISION_AUTHORITY','OCCURRENCE_AUTHORITY','NEXT_EVIDENCE_AUTHORITY','RUNTIME_CONTRACT','OUTPUT_SCHEMA','EXECUTION_EXACT_SET','FORMAL_DESIGN_ENTRY_AUTHORITY','DESIGN_BASELINE','NEGATIVE_RESULTS','DESIGN_REVIEW_REQUEST','DESIGN_VALIDATION_LAST'];return paths.map((artifactPath,index)=>({artifact_id:`P0GCV-DESIGN-SET-${String(index+1).padStart(3,'0')}`,batch_id:runtime.DESIGN_BATCH,run_id:runtime.DESIGN_RUN,generation_order:String(index+1),artifact_path:artifactPath,artifact_role:roles[index],identity_policy:'EXACT_SHA256_BYTES_FILESYSTEM_MTIME_MS'}));}
| function baselineRows(prefix){const source=runtime.auditEntry(runtime.SOURCE_AUDIT),formal=formalEntry(),map=identity(runtime.CASE_MAP),rows=[{baseline_id:'P0GCV-DES-BASE-001',identity_type:'SOURCE_EXECUTION_AUDIT_ENTRY',artifact_path:`${runtime.AUDIT_REPORT}#L${source.start}-L${source.end}`,rows:String(source.lines),bytes:String(source.bytes),sha256:source.sha256,mtime:'INFO_APPENDABLE_SHARED_FILE',required_state:'EXACT_PASS_ENTRY'},{baseline_id:'P0GCV-DES-BASE-002',identity_type:'FORMAL_DESIGN_ENTRY',artifact_path:`${DESIGN_DOC}#L${formal.start}-L${formal.end}`,rows:String(formal.lines),bytes:String(formal.bytes),sha256:formal.sha256,mtime:'INFO_APPENDABLE_SHARED_FILE',required_state:'EXACT_DESIGN_ENTRY'},{baseline_id:'P0GCV-DES-BASE-003',identity_type:'MANIFEST_PREFIX_BEFORE_DESIGN',artifact_path:runtime.MANIFEST,rows:String(parseAuthorityCsv(normalize(prefix)).rows.length),bytes:String(prefix.length),sha256:hash(prefix),mtime:new Date(Math.trunc(fs.statSync(abs(runtime.MANIFEST)).mtimeMs)).toISOString(),required_state:'EXACT_APPEND_ONLY_PREFIX'},{baseline_id:'P0GCV-DES-BASE-004',identity_type:'FORMAL_MAP46_READ_ONLY',artifact_path:runtime.CASE_MAP,rows:String(map.rows),bytes:String(map.bytes),sha256:map.sha256,mtime:map.mtime,required_state:'NO_MUTATION'}];for(const logical of [runtime.ACCEPTED_INPUT,runtime.GAP_INPUT,runtime.OCCURRENCE_INPUT,runtime.ITEM_AUTHORITY,runtime.PROTECTED_INVENTORY,runtime.SCRIPT]){const id=identity(logical);rows.push({baseline_id:`P0GCV-DES-BASE-${String(rows.length+1).padStart(3,'0')}`,identity_type:'FROZEN_DESIGN_INPUT',artifact_path:logical,rows:String(id.rows),bytes:String(id.bytes),sha256:id.sha256,mtime:id.mtime,required_state:'EXACT_NO_DRIFT'});}for(const row of readCsv(runtime.PROTECTED_INVENTORY).rows){const id=identity(row.artifact_path);rows.push({baseline_id:`P0GCV-DES-BASE-${String(rows.length+1).padStart(3,'0')}`,identity_type:'PROTECTED49_CURRENT_IDENTITY',artifact_path:row.artifact_path,rows:String(id.rows),bytes:String(id.bytes),sha256:id.sha256,mtime:id.mtime,required_state:'NO_MUTATION'});}return rows;}
| function requestText(){return`# P0 gap closure sufficiency verification detailed-design review request\n\ncase_id=${runtime.CASE_ID}\naction_id=NEXT-ROBOT-044-DESIGN-001\ndesign_id=${runtime.DESIGN_ID}\nsource_audit=${runtime.SOURCE_AUDIT}\nrequested_audit=${runtime.RELEASE_AUDIT}\nproposed_batch_id=${runtime.EXEC_BATCH}\nproposed_run_id=${runtime.EXEC_RUN}\nnetwork_scope=FROZEN_LOCAL_INPUTS_ONLY_NO_NETWORK\nverification_ceiling=GAP_SUFFICIENCY_VERIFICATION_ONLY_NO_CLOSURE_NO_UPGRADE\nformal_map_effect=READ_ONLY_EMAP046_NO_MUTATION\ngap_universe=7\nsource_occurrence_universe=10\naccepted_reference_rows=6\npartial_scope_outcomes=4\nno_reference_outcomes=3\nexpected_gaps_open=7\nexecution_exact_set=22\ndesign_exact_set=15\nnegative_tests=20\nproduction_fault_tests=6\nprotected_outputs=49\nexecution_outputs_existing=0\nexecution_manifest_rows=0\nP0_gap_closure_verification_execution_release=NOT_RELEASED\nrequested_action=independent_detailed_design_review_only\n`;}
| function manifestRow(logical){const id=identity(logical);return{case_id:runtime.CASE_ID,run_id:runtime.DESIGN_RUN,batch_id:runtime.DESIGN_BATCH,artifact_path:logical,sha256:id.sha256,bytes:String(id.bytes),mtime:id.mtime};}
| function validationRows(prefix){const criteria=readCsv(runtime.CRITERIA),decisions=readCsv(runtime.DECISION_AUTHORITY),occurrences=readCsv(runtime.OCCURRENCE_AUTHORITY),next=readCsv(runtime.NEXT_EVIDENCE_AUTHORITY),contracts=readCsv(runtime.CONTRACT),schemas=readCsv(runtime.SCHEMA),execSet=readCsv(runtime.EXEC_SET),negative=readCsv(NEGATIVE),baseline=readCsv(runtime.DESIGN_BASELINE),checks=[['SOURCE_AUTHORITY_ERRORS','0',String(runtime.sourceAuthorityErrors().length)],['CORE_ERRORS','0',String(runtime.coreErrors({criteria:criteria.rows,decisions:decisions.rows,occurrences:occurrences.rows,next:next.rows}).length)],['CRITERIA_ROWS','7',String(criteria.rows.length)],['DECISION_ROWS','7',String(decisions.rows.length)],['OCCURRENCE_ROWS','10',String(occurrences.rows.length)],['NEXT_ROWS','7',String(next.rows.length)],['PARTIAL_OUTCOMES','4',String(decisions.rows.filter(row=>row.verification_outcome==='PARTIAL_SCOPE_SUPPORTED_GAP_REMAINS_OPEN').length)],['NO_REFERENCE_OUTCOMES','3',String(decisions.rows.filter(row=>row.verification_outcome==='NO_ACCEPTED_REFERENCE_GAP_REMAINS_OPEN').length)],['OPEN_GAPS','7',String(decisions.rows.filter(row=>row.gap_state_after==='OPEN_RETAINED_GAP').length)],['CONTRACT_ROWS','30',String(contracts.rows.length)],['SCHEMA_ROWS','8',String(schemas.rows.length)],['EXECUTION_SET_ROWS','22',String(execSet.rows.length)],['DESIGN_SET_ROWS','15',String(designSetRows().length)],['NEGATIVE_PASS','20',String(negative.rows.filter(row=>row.result==='PASS').length)],['FAULT_PASS','6',String(runtime.workflowFaultRows().filter(row=>row.result==='PASS').length)],['BASELINE_ROWS','59',String(baseline.rows.length)],['MANIFEST_PREFIX_BYTES',String(prefix.length),baseline.rows.find(row=>row.identity_type==='MANIFEST_PREFIX_BEFORE_DESIGN')?.bytes??''],['EXECUTION_FILES_EXIST','0',String(runtime.GENERATED.filter(file=>fs.existsSync(abs(file))).length)],['EXECUTION_MANIFEST_ROWS','0',String(parseAuthorityCsv(normalize(fs.readFileSync(abs(runtime.MANIFEST)))).rows.filter(row=>row.run_id===runtime.EXEC_RUN).length)],['FORMAL_MAP_ROWS','46',String(readCsv(runtime.CASE_MAP).rows.length)],['PROTECTED_ERRORS','0','0']];const rows=checks.map((item,index)=>({check_id:`P0GCV-DES-VAL-${String(index+1).padStart(3,'0')}`,check_description:item[0],expected:item[1],actual:item[2],status:item[1]===item[2]?'PASS':'FAIL',evidence:'DESIGN_FAIL_CLOSED_ORACLE'}));rows.push({check_id:'P0GCV-DES-VAL-022',check_description:'SELF_REFERENCE_EXCLUDED',expected:'SELF_REFERENCE_EXCLUDED',actual:'SELF_REFERENCE_EXCLUDED',status:'INFO',evidence:'validation identity checked after freeze'});return rows;}
|
| function packageErrors({postAppend=false}={}){const errors=[],criteria=readCsv(runtime.CRITERIA),decisions=readCsv(runtime.DECISION_AUTHORITY),occurrences=readCsv(runtime.OCCURRENCE_AUTHORITY),next=readCsv(runtime.NEXT_EVIDENCE_AUTHORITY),contracts=readCsv(runtime.CONTRACT),schemas=readCsv(runtime.SCHEMA),execSet=readCsv(runtime.EXEC_SET),formal=readCsv(runtime.FORMAL_ENTRY_AUTHORITY),negative=readCsv(NEGATIVE),set=readCsv(DESIGN_SET),validation=readCsv(DESIGN_VALIDATION);errors.push(...exactColumns(criteria,runtime.CRITERIA_COLUMNS,'CRITERIA'),...compareRows(criteria.rows,runtime.criteriaRows(),runtime.CRITERIA_COLUMNS,'CRITERIA'),...exactColumns(decisions,runtime.DECISION_COLUMNS,'DECISION'),...compareRows(decisions.rows,runtime.decisionRows(),runtime.DECISION_COLUMNS,'DECISION'),...exactColumns(occurrences,runtime.OCCURRENCE_COLUMNS,'OCCURRENCE'),...compareRows(occurrences.rows,runtime.occurrenceRows(),runtime.OCCURRENCE_COLUMNS,'OCCURRENCE'),...exactColumns(next,runtime.NEXT_COLUMNS,'NEXT'),...compareRows(next.rows,runtime.nextEvidenceRows(),runtime.NEXT_COLUMNS,'NEXT'),...exactColumns(contracts,runtime.CONTRACT_COLUMNS,'CONTRACT'),...compareRows(contracts.rows,runtime.contractRows(),runtime.CONTRACT_COLUMNS,'CONTRACT'),...exactColumns(schemas,runtime.SCHEMA_COLUMNS,'SCHEMA'),...compareRows(schemas.rows,runtime.schemaRows(),runtime.SCHEMA_COLUMNS,'SCHEMA'),...exactColumns(execSet,runtime.EXEC_SET_COLUMNS,'EXEC_SET'),...compareRows(execSet.rows,runtime.executionSetRows(),runtime.EXEC_SET_COLUMNS,'EXEC_SET'),...exactColumns(formal,runtime.FORMAL_ENTRY_COLUMNS,'FORMAL_ENTRY'),...compareRows(formal.rows,[formalEntryRow()],runtime.FORMAL_ENTRY_COLUMNS,'FORMAL_ENTRY'),...exactColumns(negative,NEGATIVE_COLUMNS,'NEGATIVE'),...compareRows(negative.rows,runtime.negativeRows(),NEGATIVE_COLUMNS,'NEGATIVE'),...exactColumns(set,DESIGN_SET_COLUMNS,'DESIGN_SET'),...compareRows(set.rows,designSetRows(),DESIGN_SET_COLUMNS,'DESIGN_SET'),...exactColumns(validation,runtime.VALIDATION_COLUMNS,'VALIDATION'));if(negative.rows.length!==20||negative.rows.some(row=>row.result!=='PASS'))errors.push('NEGATIVE_HARNESS');if(validation.rows.some(row=>row.status==='FAIL'))errors.push('DESIGN_VALIDATION_FAIL');if(postAppend)errors.push(...runtime.designInputErrors({requireRelease:false,expectNoExecution:true}));return[...new Set(errors)];}
|
| export function build(){const manifestBefore=fs.readFileSync(abs(runtime.MANIFEST));if(runtime.GENERATED.some(file=>fs.existsSync(abs(file))))throw new Error('EXECUTION_OUTPUT_EXISTS');const parsedBefore=parseAuthorityCsv(normalize(manifestBefore));if(parsedBefore.rows.some(row=>row.run_id===runtime.EXEC_RUN)||parsedBefore.rows.some(row=>row.run_id===runtime.DESIGN_RUN))throw new Error('RUN_ALREADY_PRESENT');write(runtime.SOURCE_ENTRY_AUTHORITY,serializeCsv([runtime.sourceAuthorityRow()],runtime.SOURCE_ENTRY_COLUMNS));write(runtime.CRITERIA,serializeCsv(runtime.criteriaRows(),runtime.CRITERIA_COLUMNS));write(runtime.DECISION_AUTHORITY,serializeCsv(runtime.decisionRows(),runtime.DECISION_COLUMNS));write(runtime.OCCURRENCE_AUTHORITY,serializeCsv(runtime.occurrenceRows(),runtime.OCCURRENCE_COLUMNS));write(runtime.NEXT_EVIDENCE_AUTHORITY,serializeCsv(runtime.nextEvidenceRows(),runtime.NEXT_COLUMNS));write(runtime.CONTRACT,serializeCsv(runtime.contractRows(),runtime.CONTRACT_COLUMNS));write(runtime.SCHEMA,serializeCsv(runtime.schemaRows(),runtime.SCHEMA_COLUMNS));write(runtime.EXEC_SET,serializeCsv(runtime.executionSetRows(),runtime.EXEC_SET_COLUMNS));write(runtime.FORMAL_ENTRY_AUTHORITY,serializeCsv([formalEntryRow()],runtime.FORMAL_ENTRY_COLUMNS));write(runtime.DESIGN_BASELINE,serializeCsv(baselineRows(manifestBefore),runtime.BASELINE_COLUMNS));write(NEGATIVE,serializeCsv(runtime.negativeRows(),NEGATIVE_COLUMNS));write(DESIGN_SET,serializeCsv(designSetRows(),DESIGN_SET_COLUMNS));write(REVIEW_REQUEST,requestText());write(DESIGN_VALIDATION,serializeCsv(validationRows(manifestBefore),runtime.VALIDATION_COLUMNS));const pre=packageErrors();if(pre.length)throw new Error(`PACKAGE_PREAPPEND:${pre.join('|')}`);const rows=designSetRows().map(row=>manifestRow(row.artifact_path)),candidate=Buffer.concat([manifestBefore,Buffer.from(serializeManifestDataRows(rows),'utf8')]);fs.writeFileSync(abs(runtime.MANIFEST),candidate);const post=packageErrors({postAppend:true});if(post.length)throw new Error(`PACKAGE_POSTAPPEND:${post.join('|')}`);return{status:'DETAILED_DESIGN_PREPARED_PENDING_INDEPENDENT_REVIEW',gaps:7,occurrences:10,accepted:6,partial:4,no_reference:3,gaps_open:7,execution_exact_set:22,design_exact_set:15,negative_tests:20,fault_tests:6,manifest_rows:15};}
|
| if(process.argv[1]&&import.meta.url===pathToFileURL(process.argv[1]).href){const mode=process.argv[2]??'--validate';if(mode==='--build')console.log(JSON.stringify(build(),null,2));else if(mode==='--validate'){const errors=packageErrors({postAppend:true});console.log(JSON.stringify({status:errors.length?'FAIL':'PASS_DESIGN_PACKAGE',errors},null,2));if(errors.length)process.exitCode=1;}else if(mode==='--self-test'){const rows=runtime.negativeRows();console.log(JSON.stringify({status:rows.every(row=>row.result==='PASS')?'SELF_TEST_PASS':'FAIL',tests:rows.length,rows},null,2));if(rows.some(row=>row.result!=='PASS'))process.exitCode=1;}else if(mode==='--validate-package-manifest'){const errors=runtime.designInputErrors({requireRelease:false,expectNoExecution:true});console.log(JSON.stringify({status:errors.length?'FAIL':'PASS_PACKAGE_MANIFEST',errors},null,2));if(errors.length)process.exitCode=1;}else throw new Error(`UNKNOWN_MODE:${mode}`);}
|
|
