EFCH — Investigación en Computación Orientada a Propiedades
EFCH explora si los sistemas de software pueden construirse a partir de propiedades y restricciones explícitas, organizando la síntesis, la verificación y la ejecución en torno a dichas especificaciones.
ESQUEMA TÉCNICO // FLUJO DE VERIFICACIÓN
Flujo experimental en EFCH 0.1.0a1
En el prototipo EFCH, la fuente de verdad de un programa es una definición formal (.efch) con semántica, propiedades, dominio, carga de trabajo y presupuesto. Las implementaciones son candidatas que solo se aceptan si el verificador formal demuestra su equivalencia.
definition (.efch) ──► typed core ──► semantic identity (SHA-256)
│
candidates (.efl / LLM / SyGuS) ──────┼──► SMT (Z3 5.1.0.0): well-defined + equivalent ──► proved | refuted | unknown
│
└──► C (gcc -O2) ──► differential vectors ──► interleaved timing ──► evidencia.json1. Definición Formal (.efch)
Declara semántica precisa, propiedades matemáticas, dominio acotado de entrada, distribución de carga de trabajo, objetivo y presupuesto.
2. Núcleo Tipado e Identidad Semántica
Normaliza la especificación a un núcleo tipado y calcula una identidad semántica determinista (SHA-256).
3. Implementaciones Candidatas
Pueden ser propuestas por una persona, EFCH Lang (.efl), búsqueda enumerativa SyGuS (cvc5) o síntesis guiada por LLM.
4. Verificación Formal Independiente (Z3)
Comprueba buena definición y equivalencia semántica frente a la especificación, emitiendo probado, refutado (con contraejemplo) o desconocido.
5. Materialización en C y Medición
Las candidatas probadas se traducen a C (gcc -O2), se contrastan con pruebas diferenciales, se miden de forma intercalada y se registran en evidencia.json.
REGISTRO DE HIPÓTESIS // H1–H6
Compuertas de investigación y registro experimental
Persistencia de evidencia semántica frente a reverificación completa y memoización reforzada ante cambios controlados de especificación y solucionador.
Evaluado bajo protocolo congelado (tag exp019-protocolo); artefactos y borrador archivados en Zenodo (10.5281/zenodo.23873679). Los defectos D10–D13 y la limitación L-D14 siguen abiertos.
Decodificación binaria acotada en EFCH Lang 0.1 con prueba de equivalencia SMT y generación de código C.
Equivalencia probada en Z3 y reproducida en la reejecución del 2 de noviembre de 2026 (razones M9 de 1.030 y 0.965 frente a C). Archivado en Zenodo (10.5281/zenodo.23874420).
Comparación empírica de EFCH Lang 0.1 frente a C manual, Rust-Kani 0.68.0, Go 1.26 y Dafny 4.11.0.
Muestra concisión en decodificación binaria acotada junto con compromisos claros de expresividad frente a verificadores de propósito general.
Pruebas de estrés de complejidad de protocolo (incluyendo DNS) y evaluaciones negativas de frontera.
Preservados íntegramente en el archivo público P2 para documentar dónde fallan las restricciones actuales del dominio acotado.
Ventaja estructural de rendimiento de candidatas seleccionadas frente a compiladores optimizadores estándar (gcc -O2).
EXP-001 y EXP-002 no mostraron ventaja frente a gcc -O2 en las primitivas evaluadas; documentado en README-efch-0.1.0a1.md.
Separación de supervisión humana (H1) y persistencia de evidencia (H2) mediante contratos semánticos mínimos.
Documentado en RFC y Contract Conformance Pack 0.1; no autoriza implementación P0 ni valida hipótesis empíricas.
FRONTERAS METODOLÓGICAS
Limitaciones explícitas de EFCH 0.1.0a1
- L-01Dominio pequeño y estrictamente acotado: no hay bucles no acotados, recursión, memoria mutable ni efectos de E/S. Las entradas bytes tienen como máximo 64 bytes.
- L-02La traducción a C no está verificada formalmente: solo se contrasta mediante pruebas diferenciales.
- L-03Algunas propiedades son difíciles para SMT: por ejemplo, la igualdad entre dos árboles de sumadores de 64 bits (popcount.efch, propiedad complemento) queda como desconocido.
- L-04La generación por LLM no es determinista: las candidatas generadas se guardan y se verifican de forma determinista con efch verify.
- L-05Medición local y defectos abiertos: el objetivo minimize time se mide en una sola máquina, y los defectos de integridad D10–D13 / limitación L-D14 siguen abiertos.
VERIFICACIÓN Y REPRODUCIBILIDAD
Artefactos públicos y reproducción informada
Todos los paquetes públicos incluyen manifiestos SHA-256 y scripts para fijar Z3 5.1.0.0 de modo que cualquier investigador pueda auditar y reejecutar las pruebas.
Artefactos EFCH P1 — Persistencia de Evidencia Semántica (EXP-019)
Manuscrito en borrador — sin revisión por pares, no enviado a revista. Software de investigación (0.1.0a1).
Artefactos EFCH P2 — Decodificación Binaria Verificada con EFCH Lang (EXP-004 a EXP-015)
Manuscrito en borrador (v0.2) — sin revisión por pares, no enviado a revista. Software de investigación (0.1.0a1).