FENCE.I

1// PTO-INSTRUCTION: {"assembly":["fence.i"],"block":[],"catalog_indices":[97],"catalog_records":[{"asm":"fence.i","constraints":[],"encoding":[{"index":0,"mask":"0xffffffff","match":"0x1000202b","width_bits":32}],"encoding_kind":"L32","fields":[],"form_id":"fence_i_32_a321a2a186b1","length_bits":32,"mnemonic":"FENCE.I","semantic_family":"SYS","semantic_group":"SYS","semantic_handler":"FenceInstruction","semantic_summary":"FENCE.I establishes instruction visibility, invalidates the reservation, and advances the instruction-cache epoch.","status":"accepted"}],"classification":["sys"],"contract":{"block_composition":["FENCE.I executes as one scalar operation in the body of an active SYS block."],"canonical_assembly":["fence.i"],"defaults":["The instruction has no operand or mask field."],"encoding_class":"standalone-encoded","examples":["fence.i"],"exceptions":["Invalid block placement raises Illegal Block Exception before encoded-field legality or effects.","A reserved encoding or rejected access raises Illegal Instruction before destination, queue, system-state, or TPC effects."],"field_contracts":{},"field_zero_meanings":{},"legality":["Every fixed bit and explicit field constraint is checked before operation semantics."],"memory_effects":["none"],"operands":[],"ordering":["Check block placement and encoded legality before architectural effects.","Invalidate the local reservation and advance the instruction-cache epoch exactly once; FENCE.I emits no data-memory event."],"standalone_opcode":true,"state_effects":["Invalidate the local reservation, advance the instruction-cache epoch exactly once, and advance TPC."]},"depends_on":["PTO-SCALAR-MODEL-SYS-SEMANTICS"],"id":"PTO-SCALAR-FENCE-I","mnemonic":"FENCE.I","summary":"FENCE.I establishes instruction visibility, invalidates the reservation, and advances the instruction-cache epoch.","surface":"scalar"}2// PTO-REVIEW: {"review_method":"formal-definition-read","outcome":"FORMAL-COMPLETE","reviewed_fields":["assembly","encoding","defaults","operation","state","memory","ordering","faults","reserved"]}3// NDF-BEGIN: PTO-FENCE-I-DECISION-BINDING-0014// ndf: kind=contract level=L1 layer=scalar status=accepted5// FENCE.I MUST implement the mnemonic-local canonical assembly, encoded6// legality, defaults, state and memory effects, ordering, and fault boundaries7// declared in this owner. The operation region below is the executable binding8// for every accepted decision that names this mnemonic.9// NDF-END: PTO-FENCE-I-DECISION-BINDING-00110// DOC-BEGIN: decode11readonly func InstructionContractOperation_FENCE_I()12    => ScalarOperation13begin14    return ScalarOperation_FENCE_I;15end;16// DOC-END: decode17// DOC-BEGIN: operation18readonly func InstructionContractHandler_FENCE_I()19    => ScalarSemanticHandler20begin21    return ScalarHandler_FenceInstruction;22end;23
24pure func InstructionContractRequiresSystemBlock_FENCE_I()25    => boolean26begin27    return TRUE;28end;29
30pure func InstructionContractFenceInvalidatesReservation_FENCE_I()31    => boolean32begin33    return TRUE;34end;35
36pure func InstructionContractAdvancesInstructionEpoch_FENCE_I()37    => boolean38begin39    return TRUE;40end;41// DOC-END: operation42