| """Compact certificates with the same constructive closure semantics as v3. |
| |
| The checker derives known atoms only from submitted steps, never by completing |
| the proof for the model. Redundant copying of a final atom list is unnecessary. |
| """ |
| from crypto_proof_kernel import check as full_check,reference as full_reference,trace as full_trace,parse_final,prompt |
|
|
| SCHEMA=('Return JSON with exactly "secret_unreachable" (boolean) and "steps" ' |
| '(list of zero-based public fact indices). Begin with initial_known. Each ' |
| 'submitted [message,key] fact must have an already-known key and add a new ' |
| 'message. The checker derives the known set from your steps; do not copy ' |
| 'a known-atom list. Finish the entire closure, even after finding the query: ' |
| 'every fact with a known key must have its message known. Set ' |
| 'secret_unreachable to whether query_secret is absent at that fixed point. ' |
| 'Any valid deduction order is accepted. No external tools or code.') |
|
|
|
|
| def expanded(instance,certificate): |
| if not isinstance(certificate,dict) or set(certificate)!={'secret_unreachable','steps'}:return None |
| if type(certificate['secret_unreachable']) is not bool or not isinstance(certificate['steps'],list) or len(certificate['steps'])>128:return None |
| if any(type(i) is not int for i in certificate['steps']):return None |
| known=set(instance['initial_known']);facts=instance['encrypted_facts'] |
| for i in certificate['steps']: |
| if not 0<=i<len(facts):return dict(**certificate,known=sorted(known)) |
| known.add(facts[i][0]) |
| return dict(**certificate,known=sorted(known)) |
|
|
|
|
| def reference(instance): |
| value=full_reference(instance) |
| return {k:value[k] for k in ['secret_unreachable','steps']} |
|
|
|
|
| def check(instance,certificate): |
| value=expanded(instance,certificate) |
| return 'schema' if value is None else full_check(instance,value) |
|
|
|
|
| def trace(instance,certificate): |
| assert check(instance,certificate)=='valid' |
| return full_trace(instance,expanded(instance,certificate)) |
|
|
