Struct JournaledInjectivity 

pub struct JournaledInjectivity {
    pub name: String,
    pub in_bits: u32,
    pub reverse: HashMap<usize, usize>,
    pub sva_property: String,
}

A discharged JOURNALED-op injectivity obligation — the hardware twin of the software minimal-bit journaling (corner 1). A Journaled op F is many-to-one (it erases), but AUGMENTED with its Bennett ancilla J (the journal entry — the exact bits it destroyed), the map x ↦ (F(x), J(x)) is INJECTIVE: the reverse module reconstructs x from the post-state AND the ancilla. This closes the R4 gap — the Z3/exhaustive proofs covered the Bijection core, and this covers every Journaled op the same way.

Fields

name: String

in_bits: u32

reverse: HashMap<usize, usize>

The constructive reverse: the packed (F(x), J(x)) output ↦ the input x.

sva_property: String

The SVA property asserting the ancilla-augmented map is injective over every input.

Trait Implementations

impl Clone for JournaledInjectivity

fn clone(&self) -> JournaledInjectivity

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for JournaledInjectivity

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.