pub fn to_dafny(value: AlgorithmSpec) -> Rc<AlgorithmSpec>