ljz
7611f13208
相较上一版 Jacobian 确定性复用更新，本次补齐事件边界一致性、结果两侧采样及接触事件定位；保留已有物性复用和组件力学公式。 - 统一 UD00 信号求值与下一事件查询的绝对时间边界，修复循环边界浮点舍入导致的阶段错位、重复或漏报，并覆盖零时长、多阶段及长周期场景。 - 引入原生输出语义 v2：保留规则网格真实时间，补充内部时间事件和状态事件的左邻及事件后采样，按保存时间、状态和离散模式重放结果。 - 两条代码生成路径均发出 LSTP 接触描述，默认定位间隙过零及非负力模式的力截断；仅在接受事件时更新防重复记录，增加 contactEvents 诊断计数。 - 补充 MASS/LSTP 独立事件实验、八路全曲线与驱动阶段配对评估，以及 Amesim 不连续点输出对照和力差定位报告；MASS 新增释放机制仍保留为独立实验。 - 保存局部 probe、context 访问与回退、shadow replay、R288 real skip/typed replay 及阀门数值尾部诊断工具和报告；未证明净收益的实验不启用为生产默认优化。 - 更新原生运行说明和元件建模规范，补充信号边界、输出语义、接触事件和实验依赖回归测试。 验证：五组专项回归共 34 项全部通过；37 个待提交 Python 文件语法检查通过；git diff --cached --check 通过。
257 lines
16 KiB
Python
257 lines
16 KiB
Python
"""Verify each actual read and ordered write, then summarize the two cases."""
|
||
from collections import Counter
|
||
from pathlib import Path
|
||
import ctypes as c
|
||
import hashlib
|
||
import json
|
||
import struct
|
||
|
||
ROOT = Path(__file__).resolve().parents[2]
|
||
OUT = ROOT/'test/context-access-20260917'
|
||
|
||
|
||
class Medium(c.Structure):
|
||
_fields_ = [('real_helium', c.c_int)] + [(k, c.c_double) for k in ['R','cp','Tref','slope','mu','muT','S']]
|
||
|
||
|
||
class State(c.Structure):
|
||
_fields_ = [('medium', Medium)] + [(k, c.c_double) for k in ['p','T','h','rho','mu','isentropic_factor','isentropic_exponent']] + [('valid', c.c_uint),('temperatures',c.c_void_p),('jacobian',c.c_void_p)]
|
||
|
||
|
||
class Pipe(c.Structure):
|
||
_fields_ = [('medium',Medium)] + [(k,c.c_double) for k in ['p1','p2','T','diameter','length','roughness','flow']] + [('kind',c.c_int),('valid',c.c_int)]
|
||
|
||
|
||
class Context(c.Structure):
|
||
_fields_ = [('states',c.c_void_p),('count',c.c_size_t),('capacity',c.c_size_t),('temperatures',c.c_void_p),('jacobian',c.c_void_p)]
|
||
|
||
|
||
def doubles(value):
|
||
data = bytes.fromhex(value)
|
||
return list(struct.unpack('<'+'d'*(len(data)//8),data))
|
||
|
||
|
||
def value(data, typ):
|
||
if typ == c.c_double:
|
||
return struct.unpack('<d', data)[0]
|
||
return int.from_bytes(data, 'little')
|
||
|
||
|
||
def named(domain, offset, size):
|
||
typ = {'states':State, 'pipes':Pipe, 'context':Context}[domain]
|
||
slot, off = divmod(offset,c.sizeof(typ))
|
||
if size == c.sizeof(typ):
|
||
return slot, '*', None
|
||
for name, ft in typ._fields_:
|
||
begin = getattr(typ,name).offset
|
||
if begin == off and c.sizeof(ft) == size:
|
||
return slot,name,ft
|
||
if ft == Medium and begin <= off < begin+c.sizeof(ft):
|
||
for mn,mt in Medium._fields_:
|
||
if getattr(Medium,mn).offset+begin == off:
|
||
return slot,'medium.'+mn,mt
|
||
raise AssertionError((domain,offset,size))
|
||
|
||
|
||
def first_match(memory, query):
|
||
ctx = Context.from_buffer_copy(memory['context'])
|
||
key = doubles(query['key']); p, second = key[:2]
|
||
matches = []
|
||
for i in range(ctx.count):
|
||
st = State.from_buffer_copy(memory['states'],i*c.sizeof(State))
|
||
flag, actual = (1, st.T) if query['kind']=='PT' else (2, st.h)
|
||
if st.valid & flag and st.p == p and actual == second and st.medium.real_helium == query['mediumKind'] and all(getattr(st.medium,k)==v for (k,_),v in zip(Medium._fields_[1:],key[2:])):
|
||
matches.append(i)
|
||
return matches
|
||
|
||
|
||
def analyze_operation(events):
|
||
begin=events[0]; entry=events[1]
|
||
assert begin['stateSize']==c.sizeof(State) and begin['pipeSize']==c.sizeof(Pipe)
|
||
memory={k:bytearray.fromhex(entry[k]) for k in ['context','states','pipes']}
|
||
known={k:bytearray(b'\1'*len(v)) for k,v in memory.items()}
|
||
ctx=Context.from_buffer_copy(memory['context'])
|
||
memory['states'].extend(bytes((ctx.capacity-ctx.count)*c.sizeof(State)))
|
||
known['states'].extend(bytes((ctx.capacity-ctx.count)*c.sizeof(State)))
|
||
summary={k:begin[k] for k in ['jac','group','position','t','inputs']}
|
||
summary.update(entryCount=ctx.count,capacity=ctx.capacity,queries=[],allocations=[],writes=[],consumed=[],validTests=[],sameValueWrites=0,accessReads=0,accessWrites=0,scalar=[])
|
||
assert not ctx.temperatures, 'Non-NULL observer is outside this verified contract.'
|
||
summary['bindings']={'jacobian':ctx.jacobian or 0,'temperatures':ctx.temperatures or 0}
|
||
st74=State.from_buffer_copy(memory['states'],74*c.sizeof(State)) if ctx.count>74 else None
|
||
if st74: summary['state74']={'p':st74.p,'T':st74.T,'valid':st74.valid}
|
||
pending=None
|
||
for event in events[2:]:
|
||
kind=event['event']
|
||
if kind=='query':
|
||
assert pending is None
|
||
pending=dict(event, allMatches=first_match(memory,event), tested=[])
|
||
elif kind=='match':
|
||
assert pending and pending['kind']==event['kind']
|
||
matches=pending['allMatches']; expected=matches[0] if matches else -1
|
||
assert event['slot']==expected and event['hit']==bool(matches)
|
||
expected_scans=list(range(expected+1 if expected>=0 else pending['count']))
|
||
assert pending['tested']==expected_scans,(begin,pending)
|
||
summary['queries'].append(dict(kind=event['kind'],key=pending['key'],keyValues=doubles(pending['key']),mediumKind=pending['mediumKind'],hit=event['hit'],slot=event['slot'],allMatches=matches,scanCount=len(expected_scans)))
|
||
pending=None
|
||
elif kind in ['read','write']:
|
||
domain=event['domain']; offset=event['offset']; data=bytes.fromhex(event['value'])
|
||
previous=memory[domain][offset:offset+len(data)]
|
||
slot,field,typ=named(domain,offset,len(data))
|
||
if kind=='read':
|
||
assert previous==data,(begin,event,'read mismatch')
|
||
summary['accessReads']+=1
|
||
# Lookup reads are recorded in raw events; this list isolates
|
||
# fields consumed after selection, including observers/keys.
|
||
if domain!='context' and pending is None and event['function']!='same_medium':
|
||
summary['consumed'].append(dict(domain=domain,slot=slot,field=field,value=event['value'],function=event['function']))
|
||
else:
|
||
summary['accessWrites']+=1
|
||
equal=all(known[domain][offset:offset+len(data)]) and previous==data
|
||
summary['sameValueWrites']+=equal
|
||
memory[domain][offset:offset+len(data)]=data
|
||
known[domain][offset:offset+len(data)]=b'\1'*len(data)
|
||
summary['writes'].append(dict(domain=domain,slot=slot,field=field,value=event['value'],sameValue=equal,function=event['function']))
|
||
elif kind=='valid_test':
|
||
st=State.from_buffer_copy(memory['states'],event['slot']*c.sizeof(State))
|
||
assert st.valid & event['mask']==event['value']
|
||
if pending is not None:
|
||
pending['tested'].append(event['slot'])
|
||
else:
|
||
summary['validTests'].append(event)
|
||
elif kind=='allocate':
|
||
assert event['branch']=='append', 'Scratch requires additional object registration; fail closed.'
|
||
assert event['slot']==event['countAfter']-1
|
||
assert event['countAfter']==Context.from_buffer_copy(memory['context']).count
|
||
assert event['countAfter']<=event['capacity']
|
||
summary['allocations'].append(event)
|
||
elif kind=='snapshot':
|
||
assert event['phase']=='exit'
|
||
for domain in memory:
|
||
expected=bytes.fromhex(event[domain])
|
||
assert memory[domain][:len(expected)]==expected,(begin,domain,'write replay mismatch')
|
||
summary['exitCount']=event['count']
|
||
# Everything not written remains the live probe entry, checked
|
||
# across every byte of every existing slot and every pipe slot.
|
||
summary['replayExact']=True
|
||
elif kind=='end':
|
||
summary['outputs']=event['outputs']
|
||
summary['outputValues']=doubles(event['outputs'])
|
||
elif kind.startswith('scalar_'):
|
||
summary['scalar'].append(event)
|
||
else:
|
||
raise AssertionError(event)
|
||
assert pending is None and summary['replayExact']
|
||
# Snapshot replay alone cannot detect an omitted equal-valued write.
|
||
# Check the reviewed source's mandatory store sequence independently.
|
||
pipe_writes=[w for w in summary['writes'] if w['domain']=='pipes']
|
||
assert [w['field'] for w in pipe_writes]==['valid','medium','p1','p2','T','diameter','length','roughness','kind','flow','valid']
|
||
assert int.from_bytes(bytes.fromhex(pipe_writes[0]['value']),'little')==0
|
||
assert int.from_bytes(bytes.fromhex(pipe_writes[-1]['value']),'little')==1
|
||
assert pipe_writes[-2]['value']==summary['outputs']
|
||
assert all(w['slot']==(28 if begin['position']==52 else 0) for w in pipe_writes)
|
||
for allocation in summary['allocations']:
|
||
writes=[w for w in summary['writes'] if w['domain']=='states' and w['slot']==allocation['slot']]
|
||
assert [w['field'] for w in writes[:7]]==['*','medium','p','T','valid','temperatures','jacobian']
|
||
assert not [w for w in summary['writes'] if w['domain']=='states' and w['slot']<summary['entryCount']]
|
||
return summary
|
||
|
||
|
||
def compare_logical(b,p):
|
||
"""Pair hits by query order and appends by creation order, never slot ID."""
|
||
mapping={}
|
||
assert b['bindings']==p['bindings'], 'Observer/memo ownership changed within this Jacobian.'
|
||
for bq,pq in zip(b['queries'],p['queries']):
|
||
assert (bq['kind'],bq['key'],bq['mediumKind'],bq['hit'])==(pq['kind'],pq['key'],pq['mediumKind'],pq['hit'])
|
||
if bq['hit']:
|
||
assert mapping.setdefault(bq['slot'],pq['slot'])==pq['slot']
|
||
assert len(b['allocations'])==len(p['allocations'])
|
||
for ba,pa in zip(b['allocations'],p['allocations']):
|
||
assert mapping.setdefault(ba['slot'],pa['slot'])==pa['slot']
|
||
def normalized(items, translate, writes=False):
|
||
result=[]
|
||
for event in items:
|
||
domain,slot,field,v=event['domain'],event['slot'],event['field'],event['value']
|
||
if domain=='states' and translate:slot=mapping[slot]
|
||
if domain=='context' and field=='count':v='increment'
|
||
if field in ['jacobian','temperatures']:
|
||
assert int.from_bytes(bytes.fromhex(v),'little')==b['bindings'][field]
|
||
v='current_context.'+field
|
||
result.append((domain,slot,field,v))
|
||
return result if writes else set(result)
|
||
assert normalized(b['consumed'],True)==normalized(p['consumed'],False),(b['jac'],b['position'],'consumed')
|
||
assert normalized(b['writes'],True,True)==normalized(p['writes'],False,True),(b['jac'],b['position'],'ordered writes')
|
||
assert [(mapping[v['slot']],v['mask'],v['value']) for v in b['validTests']]==[(v['slot'],v['mask'],v['value']) for v in p['validTests']]
|
||
return mapping
|
||
|
||
|
||
def write_checklists(examples, summaries):
|
||
lines=['# Context 访问级清单：实测数据', '', '由 `analyze_context_access.py` 从访问事件生成。slot、Jacobian 和 position 均从 0 开始；group=-1 为 baseline。', '',
|
||
'以下以 Jacobian 200 为主案例，补充 position 52 的 PH 命中/未命中路径。完整逐次记录位于 `test/context-access-20260917/operations.json`；原始访问事件在 `audit/access.jsonl`。', '']
|
||
chosen=[s for s in summaries if (s['jac']==200 and s['group'] in [6,18]) or (s['jac'] in [1,2] and s['group']==18)]
|
||
for s in chosen:
|
||
lines += [f"## Jacobian {s['jac']}，group {s['group']}，position {s['position']}", '',
|
||
f"t={s['t']:.17g}；count {s['entryCount']} → {s['exitCount']}；capacity={s['capacity']}；输出 `{s['outputValues'][0]:.17g}`；model evaluator 返回 `{s['evalReturn']}`。", '',
|
||
'### 查询与首次匹配', '', '| 顺序 | 类型 | 完整 key：p, T 或 h, R, cp, Tref, slope, mu, muT, S | medium kind | 首个匹配 slot | 扫描条数 |', '|---|---|---|---|---|---|']
|
||
for i,q in enumerate(s['queries']):
|
||
lines.append(f"| {i+1} | {q['kind']} | `"+', '.join(format(v,'.17g') for v in q['keyValues'])+f"` | {q['mediumKind']} | {q['slot'] if q['hit'] else 'miss'} | {q['scanCount']} |")
|
||
lines += ['', '### 实际选中后的字段读取', '', '| 域 / slot | 字段 |', '|---|---|']
|
||
fields={}
|
||
for r in s['consumed']:fields.setdefault((r['domain'],r['slot']),set()).add(r['field'])
|
||
for (domain,slot),names in sorted(fields.items()):lines.append(f"| {domain}[{slot}] | "+', '.join(f'`{n}`' for n in sorted(names))+' |')
|
||
lines += ['', '查询扫描另外按短路次序读取 `valid & PT/H`、`p`、`T/h`、medium；未匹配项的字段不等于被用于物性计算。', '', '### 选中后的 valid 测试', '', '| 顺序 | slot | mask | 结果 |', '|---|---|---|---|']
|
||
for i,v in enumerate(s['validTests']):lines.append(f"| {i+1} | {v['slot']} | {v['mask']} | {v['value']} |")
|
||
lines += ['', '### 必须保留的 probe 数据', '', f"保留入口 `states[0:{s['entryCount']}]` 的全部字段；此路径没有写已有物性条目。仅追加以下新条目，修改本 operation 的 pipe 槽；其余 pipe 槽保持 probe 值。", '', '### 有序写入动作', '', '| 顺序 | 目标 | 写入值 | 已知同值写入 |', '|---|---|---|---|']
|
||
for i,w in enumerate(s['writes']):
|
||
field=w['field'];data=bytes.fromhex(w['value'])
|
||
if field=='*':text='完整 struct 清零（显式写入）'
|
||
elif field=='medium':text='复制上述完整 medium'
|
||
elif field in ['temperatures','jacobian']:text='NULL' if not int.from_bytes(data,'little') else '当前 context 的 Jacobian memo 指针'
|
||
elif field in ['count','valid','kind']:text=str(int.from_bytes(data,'little'))
|
||
else:text=format(struct.unpack('<d',data)[0],'.17g')
|
||
lines.append(f"| {i+1} | `{w['domain']}[{w['slot']}].{field}` | {text} | {'是' if w['sameValue'] else '—'} |")
|
||
lines += ['', '新条目分配分支均为 positive/finite key 且 `count < capacity`；每次在当前 count 追加，再 count++。未初始化槽的 struct 首次清零不计入“已知同值写入”。', '',
|
||
'### Fallback 原因', '', '查询 key/首匹配逻辑条目不同、已消费字段或已测试 valid 位不同、容量不足转 scratch、observer 非空、pipe 命中分支改变，或无法建立无冲突的 slot 映射时，执行原 operation。此清单不授权放宽现有 guard。', '']
|
||
(ROOT/'tests/manual/context_access_checklists.md').write_text('\n'.join(lines),encoding='utf-8')
|
||
|
||
|
||
def main():
|
||
summaries=[]; events=[]; return_pending=[]; returns=Counter(); examples=[]
|
||
with (OUT/'audit/access.jsonl').open(encoding='utf-8') as stream:
|
||
for line in stream:
|
||
event=json.loads(line)
|
||
if event['event']=='eval_return':
|
||
assert return_pending
|
||
for item in return_pending: item['evalReturn']=event['result']
|
||
return_pending=[]; returns[event['result']]+=1
|
||
elif event['event']=='begin':
|
||
assert not events
|
||
events=[event]
|
||
else:
|
||
assert events
|
||
events.append(event)
|
||
if event['event']=='end':
|
||
item=analyze_operation(events);summaries.append(item);return_pending.append(item)
|
||
if item['jac']==200: examples.append(dict(summary=item,events=events))
|
||
events=[]
|
||
assert not events and not return_pending
|
||
by_key={(x['jac'],x['group'],x['position']):x for x in summaries}
|
||
cases={}
|
||
for group,pos in [(18,52),(6,16)]:
|
||
pairs=[]
|
||
for jac in range(896):
|
||
b=by_key[jac,-1,pos];p=by_key[jac,group,pos]
|
||
assert b['inputs']==p['inputs'] and b['outputs']==p['outputs'] and b['evalReturn']==p['evalReturn']==1
|
||
equal_query=[(q['kind'],q['key'],q['mediumKind'],q['hit']) for q in b['queries']]==[(q['kind'],q['key'],q['mediumKind'],q['hit']) for q in p['queries']]
|
||
mapping=compare_logical(b,p)
|
||
pairs.append(dict(jac=jac,queryKeysAndHitsEqual=equal_query,logicalReadsAndOrderedWritesEqual=True,slotMapping=mapping,entryCounts=[b['entryCount'],p['entryCount']],exitCounts=[b['exitCount'],p['exitCount']],slots=[[q['slot'] for q in b['queries']],[q['slot'] for q in p['queries']]],allocations=[[a['slot'] for a in b['allocations']],[a['slot'] for a in p['allocations']]],state74=[b.get('state74'),p.get('state74')]))
|
||
cases[f'group{group}_position{pos}']=dict(pairs=len(pairs),equalQueryKeysAndHits=sum(p['queryKeysAndHitsEqual'] for p in pairs),countShiftPairs=sum(p['entryCounts'][0]!=p['entryCounts'][1] for p in pairs),rows=pairs)
|
||
result=dict(operations=len(summaries),replayExact=len(summaries),reads=sum(s['accessReads'] for s in summaries),writes=sum(s['accessWrites'] for s in summaries),sameValueWrites=sum(s['sameValueWrites'] for s in summaries),evalReturns=dict(returns),cases=cases)
|
||
for name,obj in [('summary.json',result),('operations.json',summaries),('jacobian-200.json',examples)]:
|
||
(OUT/name).write_text(json.dumps(obj,ensure_ascii=False,indent=2)+'\n',encoding='utf-8')
|
||
write_checklists(examples,summaries)
|
||
print(json.dumps({k:v for k,v in result.items() if k!='cases'},indent=2))
|
||
for name,case in cases.items(): print(name,{k:v for k,v in case.items() if k!='rows'})
|
||
|
||
|
||
if __name__=='__main__':main()
|