TritonVM / triton-vm

Triton is a virtual machine that comes with Algebraic Execution Tables (AET) and Arithmetic Intermediate Representations (AIR) for use in combination with a STARK proof system.
https://triton-vm.org
Apache License 2.0
223 stars 35 forks source link

Error in use of `HashSet` in `substitute` in `triton-vm/src/table/constraint_circuit.rs` #279

Closed Sword-Smith closed 1 month ago

Sword-Smith commented 1 month ago

In this code, we are mutating the elements in the all_nodes HashSet in such a way that their Eq and Hash behavior changes:

pub fn substitute(&self, old_id: usize, new: &Rc<RefCell<ConstraintCircuit<II>>>) {
    for node in self.all_nodes.borrow().iter() {
        if node.circuit.borrow().id == old_id {
            continue;
        }

        let BinaryOperation(_, ref mut lhs, ref mut rhs) = node.circuit.borrow_mut().expression
        else {
            continue;
        };

        if lhs.borrow().id == old_id {
            *lhs = new.clone();
        }
        if rhs.borrow().id == old_id {
            *rhs = new.clone();
        }
    }
}

The documentation of HashSet contains two warnings: 1.

If you implement these[Hash and Eq] yourself, it is important that the following property holds: k1 == k2 -> hash(k1) == hash(k2)

and

  1. It is also a logic error for a key to be modified in such a way that the key’s hash, as determined by the Hash trait, or its equality, as determined by the trait, changes while it is in the map. This is normally only possible through Cell, RefCell, global state, I/O, or unsafe code.

We're good on 1 and have tests covering that, but the above function violates 2, as Eq and Hash for a ConstraintCircuit is defined in terms of its expression, which is mutated here.

Sword-Smith commented 1 month ago

Closed by 6e5443e5fe21c7891b622d59d1d4e115b1922400