"""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()