Traducción de los crates core y alloc de Rust
Ejecución inicial 🐥
- Al hacer una ejecución inicial de los crates
allocycorede Rust concoq-of-rust, se generaron dos archivos de código Coq de varios cientos de miles de líneas. - Esto significa que la herramienta funciona incluso con bases de código grandes, pero el código Coq generado no compila. Los errores aparecen con poca frecuencia (aproximadamente una vez cada varios miles de líneas).
Tamaño del código Rust de entrada (según el comando cloc)
-
alloc: 26,299 líneas de código Rust -
core: 54,192 líneas de código Rust -
Como hay que traducir expandiendo macros, el tamaño real a traducir es mayor.
División del código generado 🪓
- El cambio principal fue dividir la salida generada por
coq-of-rusten un archivo por cada archivo Rust de entrada. - Esto es posible porque la traducción puede hacerse sin depender del orden de las definiciones. Aunque las dependencias circulares entre archivos Rust están prohibidas en Coq, aun así es posible dividirlos.
Tamaño de la salida
alloc: 54 archivos Coq, 171,783 líneas de código Coqcore: 190 archivos Coq, 592,065 líneas de código Coq
Ventajas de dividir el código
- Es más fácil leer y navegar el código generado
- Es más fácil compilarlo porque se puede compilar en paralelo
- Es más fácil depurar enfocándose en un solo archivo
- Es más fácil ignorar los archivos que no compilan
- Es más fácil rastrear cambios en un solo archivo, lo que simplifica el mantenimiento
Corrección de algunos bugs 🐞
- Había un bug causado por colisiones entre nombres de módulos. Esto ocurría al elegir el nombre del módulo para los bloques
impl. - Se añadió más información a los nombres de módulo para aumentar su unicidad. Por ejemplo, se agregó la cláusula
where.
Ejemplo
-
Implementación del tipo
Mappingpara el traitDefault:#[derive(Default)] struct Mapping<K, V> { // ... } -
Código Coq anterior:
Module Impl_core_default_Default_for_dns_Mapping_K_V. (* ...trait implementation ... *) End Impl_core_default_Default_for_dns_Mapping_K_V. -
Código Coq corregido:
Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_dns_Mapping_K_V. (* ... *)
Lista de archivos que no compilan
-
alloc/boxed.v -
core/any.v -
core/array/mod.v -
core/cmp/bytewise.v -
core/error.v -
core/escape.v -
core/iter/adapters/flatten.v -
core/net/ip_addr.v -
Esto representa el 4% del total de archivos. Incluso en los archivos que sí compilan puede haber estructuras de Rust que todavía no se procesan.
Ejemplo 🔎
Código fuente del método unwrap_or_default del tipo Option
pub fn unwrap_or_default(self) -> T
where
T: Default,
{
match self {
Some(x) => x,
None => T::default(),
}
}
Código Coq traducido
Definition unwrap_or_default (T : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
let Self : Ty.t := Self T in
match τ, α with
| [], [ self ] =>
ltac:(M.monadic
(let self := M.alloc (| self |) in
M.read (|
M.match_operator (|
self,
[
fun γ =>
ltac:(M.monadic
(let γ0_0 :=
M.get_struct_tuple_field_or_break_match (|
γ,
"core::option::Option::Some",
0
|) in
let x := M.copy (| γ0_0 |) in
x));
fun γ =>
ltac:(M.monadic
(M.alloc (|
M.call_closure (|
M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
[]
|)
|)))
]
|)
|)))
| _, _ => M.impossible
end.
Código simplificado de la función
Definition unwrap_or_default {T : Set}
{_ : core.simulations.default.Default.Trait T}
(self : Self T) :
T :=
match self with
| None => core.simulations.default.Default.default (Self := T)
| Some x => x
end.
- Esta definición simplificada se usa al verificar el código. La prueba de equivalencia está en
CoqOfRust/core/proofs/option.v.
Conclusión
-
La formalización de la biblioteca estándar permite confiar en el trabajo de verificación de programas Rust.
-
El siguiente objetivo sigue siendo simplificar el proceso de prueba, que todavía es engorroso. En particular, se busca separar pasos como la resolución de nombres, la introducción de tipos avanzados y la eliminación de efectos secundarios en el proceso de demostrar que la simulación es equivalente al código Rust original.
-
Si te interesa la verificación formal de proyectos Rust, contacta a contact@formal.land. La verificación formal ofrece el nivel más alto de seguridad al garantizar matemáticamente la ausencia de bugs con respecto a una especificación dada.
Etiquetas:
- coq-of-rust
- Rust
- Coq
- traducción
- core
- alloc
Opinión de GN⁺
- Integración de Rust y Coq: La integración de Rust y Coq ayuda mucho a mejorar la confiabilidad de los programas Rust. Combinar la seguridad de Rust con la verificación formal de Coq resulta especialmente útil en aplicaciones críticas.
- Importancia de la automatización: La traducción automática con la herramienta
coq-of-rustes más confiable que el trabajo manual. Aun así, sigue siendo necesario tener cuidado, porque todavía pueden aparecer errores durante el proceso de verificación. - Gestión de bases de código complejas: Al trabajar con bases de código grandes, dividir el código ayuda mucho al mantenimiento y la depuración. Esto es especialmente importante en el trabajo en equipo.
- Necesidad de la verificación formal: La verificación formal es esencial en áreas críticas como finanzas, salud y aviación. La combinación de Rust y Coq puede aportar un gran valor en estos sectores.
- Consideraciones al adoptar la tecnología: Al introducir nuevas tecnologías, hay que considerar la curva de aprendizaje y la compatibilidad con los sistemas existentes. Las herramientas de verificación formal como Coq pueden tener una curva de aprendizaje alta, por lo que se necesita suficiente preparación y capacitación.
1 comentarios
Opinión de Hacker News
Resumen de comentarios de Hacker News
Confiabilidad de las herramientas de traducción automática
Tamaño del programa y verificación
Posibilidad de errores en el proceso de traducción
Publicación relacionada con criptomonedas
Límites de la verificación formal
Verificación formal de Rust
Escritura de especificaciones para verificación formal
Comparación con otros enfoques
Adopción de Rust en el kernel
Agregar un backend de Rust a F*