Primero identidad estable. Después cambios de fuente.
El grafo semántico permite consultar declaraciones, tipos, efectos, contratos, propiedad y relaciones de llamadas mediante identidades estables. La versión 0.8.0 amplía ese modelo con leyes del código, reparación protegida de implementaciones, integraciones Rust más completas y un entorno de orquestación.
entity Semaprax
status beta
snapshot 615e501
authority github.com/wavect/semaprax| Instantánea del repositorio | 615e501 · 2026-10-06. La etiqueta v0.8.0 apunta al commit de código fijado. La CI exacta de la etiqueta terminó correctamente. Esto no garantiza aptitud para producción ni seguridad general. |
|---|---|
| Estado del producto completo | 55 Parcial · 0 Implementado · 0 Faltante |
| Contrato de grafo y proyecto | El código canónico, los ID estables y las representaciones comprobadas del compilador conectan leyes, consultas semánticas, cambios y ejecución. Los esquemas de grafo y Project seleccionados por funcionalidad conservan sus propios contratos de admisión, compatibilidad y autoridad del anfitrión. |
| Versión beta publicada | v0.8.0 · Publicada el 6 de octubre de 2026 a las 07:37 UTC. Los 82 trabajos de CI de la etiqueta exacta finalizaron correctamente. Se publicaron tres archivos de la cadena de herramientas, SHA256SUMS, atestaciones por archivo y procedencia agregada firmada. El trabajo de lanzamiento verificó de forma independiente el conjunto firmado antes de publicarlo. Los archivos no están notarizados ni se afirma que las compilaciones sean reproducibles; la verificación sin conexión no acredita el estado actual de revocación. CI de la etiqueta exacta. |
| Previews de paquetes y API | La versión incluye perfiles útiles del lenguaje, leyes del programa, orquestación e integración con el sistema anfitrión. La publicación y el soporte de los paquetes Rust/npm generados, las ABI genéricas públicas y otras plataformas siguen requiriendo decisiones independientes. |
Semaprax comprueba el código .spx legible y lo resuelve a HIR, su representación tipada del compilador. Las identidades del código y de su significado vinculan consultas, obligaciones de prueba, cambios candidatos y ejecución al programa inspeccionado. Los agentes de programación pueden usar la orquestación alrededor de este núcleo; los Agents en ejecución decodifican propuestas, autorizan efectos y actualizan el estado mediante capacidades suministradas explícitamente por el anfitrión.
El código .spx legible sigue siendo la representación canónica en Git. Un @id explícito identifica una declaración durante los cambios de nombre admitidos. Las revisiones derivadas del compilador vinculan el código y el preludio seleccionado; las codificaciones del grafo exponen esos hechos sin sustituir el código fuente.
Selecciona una declaración, dirección, profundidad, número de nodos y límite de bytes. El contexto de tarea y las proyecciones text, binary o model-text mantienen la comprobación exacta frente a los hechos seleccionados. El gestor nativo de contexto semántico puede usar Graft o Graphify para navegar por el repositorio sin atribuir a un índice externo la autoridad del compilador.
Las declaraciones nativas de leyes asignan identidades persistentes a los requisitos contractuales y relacionales. Un LawSet seleccionado por separado fija el inventario completo y la política estricta. Los adaptadores Lean/Z3 instalados prueban las leyes escalares, modulares, estructuradas y de listas admitidas; distinguen los resultados obsoletos, no admitidos, desconocidos y refutados. La reparación candidata debe satisfacer el requisito conservado.
Inspecciona el contexto, deriva un candidato, examina su impacto y revisión, repite las comprobaciones y autoriza su aplicación. La sustitución acotada de expresiones, los cambios estructurales y la composición especificada mantienen sus límites de operación y revisión. Los cambios en leyes y las reparaciones de implementación siguen reglas de protección distintas.
Las generaciones gestionadas del espacio de trabajo, la evidencia del candidato y los almacenes de revisiones Project vinculan la publicación al candidato comprobado. La API de integración Rust ofrece entradas acotadas y sesiones opacas. Validar varios archivos no actualiza por sí solo archivos arbitrarios, referencias Git ni búferes del editor.
Los perfiles admitidos incluyen registros, variantes, clases, herencia, genéricos con inferencia de argumentos acotada, Option/Result, bucles, iteradores, valores de función, cadenas y bytes. List<i64> inmutable añade operaciones persistentes nil/cons/uncons. Las restricciones generales y las combinaciones arbitrarias siguen necesitando su propia admisión.
Los valores con propietario, las vistas prestadas, los planes de liberación y ciertas composiciones de recursos son ejecutables. Los perfiles acotados de closures incluyen capturas de Bytes con propietario, copias de valores escalares, estado escalar mutable transaccional y capturas síncronas de texto prestado. Cada perfil comprueba sus reglas de escape, movimiento, reversión y liberación; las relaciones de tiempo de vida más amplias siguen pendientes.
Los índices preparados de API Rust seleccionan importaciones admitidas y entradas Cargo exactas. Los adaptadores generados de propiedad, vistas prestadas y callbacks conectan código comprobado con consumidores reales de Regex/Url y Serde/iteradores. La integración de Futures en un mismo hilo utiliza un ejecutor controlado por el llamador. Las suposiciones sobre código externo permanecen explícitas; el código de enlace generado no prueba el interior de una crate.
Inicializar, observar, proponer, decodificar, autorizar, ejecutar y reducir. La autorización se repite en cada turno y el reductor elige Continue, Complete, Suspend o Fail. Las rutas de ejecución predeterminadas usan el intérprete; las rutas opcionales de biblioteca aceptan anfitriones de etapas C11 nativas o Core Wasm retenidos por el llamador, con evidencia local acotada de equivalencia.
Los adaptadores explícitos aportan transporte, credenciales y almacenamiento. Los perfiles persistentes confirman la intención antes de despachar y conservan como inciertos los intentos no resueltos. Los límites y registros separan llamadas, trabajo, bytes, tokens y costes. Los reintentos y la conmutación del anfitrión genérico tienen un contrato distinto al de la ruta vinculada de modelo y código; esta última no cambia automáticamente de proveedor ni reintenta trabajo incierto.
El intérprete dispone de yields secuenciales y dependientes del control acotados, conservación selectiva de Bytes con propietario y perfiles persistentes autenticados. El perfil público de Agents con propiedad tiene un ciclo de dos turnos y comprobaciones de reinicio de proceso seleccionadas. Los emisores nativos/Wasm habituales siguen rechazando funciones con yields; quedan pendientes un planificador general y una ABI universal de continuaciones.
La orquestación de la cadena completa coordina tareas explícitas, respuestas del compilador, descriptores de proveedores, bloqueos y confianza por proyecto, selección de modelos, skills y conexiones. Los paquetes oficiales Ponytail/Caveman, los adaptadores Graft/Graphify y las vistas RTK sirven a flujos seleccionados. Los resultados autoritativos de comandos permanecen separados de las salidas compactas dirigidas al modelo.
Una sesión de intérprete retenida admite un candidato, planifica la compatibilidad y lo activa entre invocaciones. El sondeo vigila las entradas declaradas del Project; los cambios inválidos dejan utilizable la revisión activa. Los controles de VS Code muestran el estado activo, pendiente y modificado sin guardar. La migración del diario de Agents definidos en el código es una ruta separada de la cadena completa.
Un servicio de referencia combina decisiones comprobadas de sesiones, tareas y trabajos con un anfitrión de instantáneas, HTTP/TLS explícito y telemetría seleccionada de eventos JSON u OTLP. El recorrido aceptado con Linux/Podman mantiene un alcance acotado; se rechazan los adaptadores SQL. Los agentes económicos conservan en el anfitrión el control de la cartera, aprobación, firma y conciliación.
Los perfiles Project de datos con propiedad y un endpoint Wasm genérico privado del compilador tienen evidencia de consumidores generados. El soporte genérico público sigue sin estar admitido ni publicado. Los metadatos firmados del registro local, las generaciones retenidas y las lecturas vinculadas al bloqueo no proporcionan por sí solos un registro de paquetes alojado ni autoridad para descargar por red.
El trabajo Lean de la etiqueta exacta comprueba su núcleo formal acotado y la exportación de obligaciones. Los trabajos de lanzamiento atestiguan por separado los tres archivos y firman y verifican la procedencia agregada. Son cadenas de evidencia distintas; ninguna demuestra la corrección de todo el lenguaje, notarización ni compilaciones reproducibles entre anfitriones.
module examples.meaning;
@id("math.add")
fn add(left: i64, right: i64) -> i64
requires left >= 0
requires right >= 0
ensures result == left + right
{
left + right
}
@id("app.main")
fn main() -> i64
ensures result == 42
{
add(19, 23)
}Revisado frente a la etiqueta v0.8.0 y su commit de código fijado. Las especificaciones versionadas definen admisión y autoridad; los títulos de versiones anteriores en la matriz y el roadmap son históricos. GitHub repository.
El manual en línea es la guía en inglés publicada desde main y puede incluir cambios posteriores a 0.8.0. Utiliza la copia fijada a la revisión al reproducir esta versión.
La ruta de aprendizaje actual en inglés, publicada desde main.
Los archivos del manual en el commit exacto del lanzamiento revisado.
Guía actual en inglés del manifiesto, las comprobaciones, las pruebas y las compilaciones de la calculadora.
Introducción actual en inglés a valores, funciones y estructura del código.
Guía actual en inglés de contexto semántico y flujos seguros de cambios.
Comandos fijados a la revisión y límites entre la CLI independiente y la cadena completa.
Configuración, navegación semántica, revisión y controles de desarrollo fijados a la revisión.
Ejemplos fijados a la revisión para el lenguaje, proyectos, leyes, Agents e integraciones con el anfitrión.
Revisado frente a la etiqueta v0.8.0 y su commit de código fijado. Las especificaciones versionadas definen admisión y autoridad; los títulos de versiones anteriores en la matriz y el roadmap son históricos.
El compilador deriva el grafo central del código comprobado, con declaraciones, tipos, contratos y relaciones estables. La orquestación puede usar también Graft o Graphify para navegar por el repositorio. Esos índices externos complementan los hechos semánticos del compilador y no sustituyen sus reglas de revisión y validación.
La cadena expone operaciones de edición concretas vinculadas a revisiones, revisión de candidatos y repetición de comprobaciones. Los inventarios protegidos de leyes mantienen separados los requisitos y los cuerpos de implementación editables. Un agente debe usar una operación admitida y una ruta de aplicación autorizada; una consulta de contexto o una prueba correcta no da permiso para sobrescribir archivos arbitrarios.