Primero identidad estable. Después cambios de fuente.
El grafo semántico de Semaprax registra declaraciones tipadas, efectos, contratos, datos de ownership, llamadas e identidades de compilación bajo una revisión derivada del contenido.
entity Semaprax
status investigación pre-alfa
snapshot b9f593c
authority github.com/wavect/semaprax| Instantánea del repositorio | b9f593c · 2026-09-16. El commit de main revisado coincide con la etiqueta v0.5.0. La CI de esa etiqueta terminó correctamente; la CI independiente de la rama fue cancelada. 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 | Los esquemas del grafo se seleccionan por función y preservan contratos anteriores. Project v1 es la base; los perfiles de datos con ownership v8, v9, v10 y v11 tienen límites propios. |
| Versión preliminar publicada | v0.5.0 · Publicada el 16 de septiembre de 2026 a las 09:43 UTC. Tres archivos: Linux x86-64, macOS Apple Silicon y Windows x86-64, con SHA256SUMS. El binario semaprax incluido es la toolchain completa, no la CLI independiente de Cargo. CI de la etiqueta exacta. |
| Previews de paquetes y API | Publicar la toolchain no publica sus paquetes Rust/npm generados ni promueve APIs privadas. Las decisiones sobre Project v8-v11, ownership genérico público, más plataformas y etapas Agent nativas/Wasm siguen siendo independientes. |
Semaprax transforma código .spx canónico en HIR validado, una representación del significado tipado. Las identidades estables conectan consultas, candidatos, ejecución y evidencia. Los cambios admitidos deben coincidir con su revisión; las propuestas Agent pasan decodificación tipada y autorización determinista. Ni grafos ni recibos conceden por sí solos permiso para publicar, usar la red o pagar.
El código .spx legible sigue siendo canónico en Git. Los valores @id identifican declaraciones independientemente de cambios de nombre admitidos. La revisión vincula código canónico y prelude implícito del compilador, no posiciones accidentales ni el formato serializado del grafo.
Context v1/v2 limita profundidad, nodos y bytes; v2 añade recorrido direccional. El contexto por tarea y las proyecciones text, binary y model-text permiten intercambios enfocados con comprobación por replay. Menos bytes no implica menos tokens facturados ni mejores respuestas.
Inspeccionar contexto, derivar candidato, revisar impacto, reproducir comprobaciones y autorizar la aplicación explícitamente. Además de renombrar hay reemplazo limitado de expresiones, cambios estructurales y composición rebase/merge definida. Cada protocolo conserva sus límites de revisión, identidad y operación.
Las generaciones de workspace, evidencia de candidatos, almacén de revisiones y flujos MCP mantienen autoridad explícita de escritura y publicación. Validar varios archivos no actualiza atómicamente rutas arbitrarias, Git o editores. La API de integración Rust ofrece límites, cancelación y sesiones opacas, no acceso libre al host.
Los perfiles admiten records, variantes, clases, herencia, genéricos, Option/Result, mutación explícita, bucles, colecciones, iteradores, valores de función y closures limitados. Texto, bytes y biblioteca incluida permiten programas útiles. Capturas propietarias, restricciones genéricas generales y combinaciones arbitrarias siguen limitadas.
Se implementan valores propios y prestados, planes de limpieza, hechos de préstamos y composiciones seleccionadas de recursos/genéricos. v0.5.0 añade String propio como carga directa de variantes; las sustituciones genéricas String y records propios anidados siguen restringidos. No es un sistema general completo de lifetimes ni compatibilidad Rust.
Inicializar, observar, proponer, decodificar, autorizar, ejecutar y reducir. El reducer validado decide Continue, Complete, Suspend o Fail; se autoriza de nuevo en cada turno. Los esquemas Proposal compilados limitan streaming y decodificación antes de efectos. Las etapas Agent de código se ejecutan en el intérprete retenido, sin paridad nativa/Wasm.
Los adaptadores explícitos aportan credenciales, transporte y almacenamiento. Los límites cubren llamadas, tokens, bytes, plazos y costes cotizados. Los perfiles duraderos confirman intención antes de enviar y rechazan reenvíos inciertos. El host genérico admite retry/failover limitado; la ruta source-model ligada no reintenta ni cambia proveedor automáticamente. Uso observado no equivale a facturación garantizada.
HTTPS POST validado, autenticación/sesiones del host Rust y jobs con checkpoints son perfiles separados, no un framework web completo. Los agentes económicos exploran intenciones de pago, simulación, aprobación y conciliación con wallets y firma del host. Una propuesta no autoriza pagos ni garantiza liquidación exactamente una vez.
Project v8 transporta Bytes y formas concretas de Option/Result; v9 añade records propios planos, v10 UTF-8 propio y v11 records propios anidados. Consumidores native/Rust y npm/Wasm, transportes privados y metadatos genéricos tienen contratos separados. Publicar toolchain, paquetes y soporte público son decisiones distintas.
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 contra el commit fijado y el registro de v0.5.0. Las especificaciones versionadas delimitan admisión y autoridad; los encabezados antiguos de v0.4 en la matriz y el roadmap no identifican la última versión. Repositorio de GitHub.
Revisado contra el commit fijado y el registro de v0.5.0. Las especificaciones versionadas delimitan admisión y autoridad; los encabezados antiguos de v0.4 en la matriz y el roadmap no identifican la última versión.
No. Es una representación tipada derivada del compilador, no un índice documental ni una base de embeddings. Fuente canónica y prelude ligan revisiones; HIR validado aporta identidades y hechos semánticos.
No de forma arbitraria. v0.5.0 incluye familias delimitadas de reemplazo de expresiones, cambios estructurales y composición. Cada una valida revisión y admisión; evidencia e inspección de lectura no otorgan autoridad arbitraria sobre archivos, Git o publicación.