Skip to main content

load_store_realized

Function load_store_realized 

Source
pub fn load_store_realized(op: &Op) -> bool
Expand description

The load-store ops realized in the soft-core’s heap unit (soft_core.v’s dmem/hp + the run_soft_core model): sequence construction, push, indexed read, and length. Proven by the the_soft_core_runs_logos_programs_identically_to_the_vm differential (heap ≡ VM RuntimeValue::List) and decoded at their binisa wire opcodes by the soft_core_decodes_the_wire_opcodes lock.