Tradução dos crates core e alloc do Rust
Execução inicial 🐥
- Usando
coq-of-rust, uma execução inicial dos cratesallocecoredo Rust gerou dois arquivos de código Coq com algumas centenas de milhares de linhas. - Isso significa que a ferramenta funciona mesmo em codebases grandes, mas o código Coq gerado não compila. Os erros ocorrem raramente (aproximadamente uma vez a cada alguns milhares de linhas).
Tamanho do código Rust de entrada (com base no comando cloc)
-
alloc: 26.299 linhas de código Rust -
core: 54.192 linhas de código Rust -
Como é necessário expandir macros para fazer a tradução, o volume real a ser traduzido é ainda maior.
Divisão do código gerado 🪓
- A principal mudança foi dividir a saída gerada pelo
coq-of-rustem um arquivo por arquivo Rust de entrada. - Isso é possível porque a tradução pode ser feita independentemente da ordem das definições. Dependências circulares entre arquivos Rust são proibidas em Coq, mas ainda assim a divisão é possível.
Tamanho da saída
alloc: 54 arquivos Coq, 171.783 linhas de código Coqcore: 190 arquivos Coq, 592.065 linhas de código Coq
Vantagens da divisão do código
- Facilita a leitura e navegação no código gerado
- Facilita a compilação por permitir compilação em paralelo
- Facilita o debug ao focar em um único arquivo
- Facilita ignorar arquivos que não compilam
- Facilita a manutenção ao rastrear mudanças em um único arquivo
Correção de alguns bugs 🐞
- Havia um bug causado por colisões entre nomes de módulos. Isso acontecia ao escolher o nome do módulo para blocos
impl. - Mais informações foram adicionadas ao nome do módulo para aumentar a unicidade. Por exemplo, foi adicionada a cláusula
where.
Exemplo
-
Implementação do tipo
Mappingpara o 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 corrigido:
Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_dns_Mapping_K_V. (* ... *)
Lista de arquivos que não compilam
-
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 -
Isso representa 4% do total de arquivos. Mesmo os arquivos que compilam podem conter estruturas Rust ainda não tratadas.
Exemplo 🔎
Código-fonte original do método unwrap_or_default do tipo Option
pub fn unwrap_or_default(self) -> T
where
T: Default,
{
match self {
Some(x) => x,
None => T::default(),
}
}
Código Coq traduzido
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 da função simplificada
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.
- Essa definição simplificada é usada na verificação do código. A prova de equivalência está em
CoqOfRust/core/proofs/option.v.
Conclusão
-
A formalização da biblioteca padrão torna confiável o trabalho de verificação de programas Rust.
-
O próximo objetivo é simplificar o processo de prova, que ainda é trabalhoso. Em especial, deseja-se separar etapas como resolução de nomes, introdução de tipos avançados e remoção de efeitos colaterais no processo de mostrar que a simulação é equivalente ao código Rust original.
-
Se você tem interesse em verificação formal de projetos Rust, entre em contato pelo e-mail contact@formal.land. A verificação formal oferece o mais alto nível de segurança ao garantir matematicamente a ausência de bugs em relação a uma especificação dada.
Tags:
- coq-of-rust
- Rust
- Coq
- tradução
- core
- alloc
Opinião do GN⁺
- Integração entre Rust e Coq: A integração entre Rust e Coq ajuda bastante a aumentar a confiabilidade de programas Rust. Combinar a segurança do Rust com a verificação formal do Coq é especialmente útil em aplicações críticas.
- Importância da automação: A tradução automática com a ferramenta
coq-of-rusté mais confiável do que o trabalho manual. Ainda assim, é preciso cuidado, pois erros podem surgir durante o processo de verificação. - Gestão de codebases complexas: Em codebases grandes, a divisão do código ajuda muito na manutenção e no debug. Isso é especialmente importante em trabalho em equipe.
- Necessidade de verificação formal: A verificação formal é essencial em áreas críticas como finanças, saúde e aviação. A combinação de Rust e Coq pode gerar grande valor nesses setores.
- Pontos a considerar na adoção da tecnologia: Ao adotar uma nova tecnologia, é preciso considerar a curva de aprendizado e a compatibilidade com sistemas existentes. Ferramentas de verificação formal como Coq podem ter uma curva de aprendizado alta, exigindo preparo e treinamento adequados.
1 comentários
Comentários do Hacker News
Resumo da coletânea de comentários do Hacker News
Confiabilidade das ferramentas de tradução automática
Tamanho dos programas e verificação
Possibilidade de erros no processo de tradução
Postagens relacionadas a criptomoedas
Limites da verificação formal
Verificação formal em Rust
Escrita de especificações de verificação formal
Comparação com outras abordagens
Adoção de Rust no kernel
Adição de backend Rust ao F*