Djinious
Logique de sécurité
Logique de vote 2oo3 et un déclenchement à verrouillage qui reste vrai une fois déclenché.
REQ-SF-001 · 002Neuf fonctions de sécurité, de l’exigence YAML au Rust embarqué certifié
Le projet de référence du voteur fait passer neuf fonctions de sécurité — vote, verrouillage, limitation de pente, surveillance de déclenchement, verrouillages de sécurité et une jauge de débit avec une frontière en virgule flottante — à travers les treize jalons, et rejoue chacune sur un Cortex-M4F émulé.
DjiniousSafe
- fonctions de sécurité
- 9fonctions de sécuritéREQ-SF-001 à REQ-SF-016
- jalons franchis
- 13jalons franchisBUILD ACCEPTÉ
- cas sur cible pour flow_gauge
- 406cas sur cible pour flow_gauge0 échec · 78 cas flottants
- différences entre deux builds
- 0différences entre deux buildsevidence.json, empreintes ELF incluses
Le projet
examples/voter est un projet djsafe complet : un fichier d’exigences, les spécifications Lean qu’il désigne, et une section cible nommant thumbv7em-none-eabihf sur la machine QEMU netduinoplus2. C’est le projet remis à un évaluateur externe accompagné d’un dossier de preuves unique.
Chaque exigence énonce, en texte clair, ce que la fonction doit faire — « La sortie du voteur doit être vraie si et seulement si au moins deux des trois canaux d’entrée sont vrais » — et son texte normalisé en espaces est fixé par empreinte dans les preuves, si bien qu’un changement de formulation est un changement que le build peut voir.
Ce que couvrent les neuf fonctions
Commande en virgule fixe
Un limiteur de pente borné à ±100 par pas dans [−1000, 1000], un moniteur de déclenchement à deux états avec hystérésis, et un bloc de gain Q4.
REQ-SF-010 · 011 · 012Division, racines et arithmétique large
Moyennes, ratios, racines carrées, normes de vecteurs et compteurs modulo, y compris l’arithmétique i64 large — certifiés sans panique (panic-free).
REQ-SF-013 · 014Entrées mixtes
Un verrouillage de pression qui se déclenche à l’activation à ≥ 3000 et s’efface à la réinitialisation en dessous de 2500, avec une pression pire cas verrouillée et une marge de sécurité.
REQ-SF-015Une frontière en virgule flottante
Une jauge de débit dont la valeur de capteur entre en f32 IEEE-754 par une conversion certifiée entiers uniquement vers Q4, et dont la marge ressort en f32 exactement convertie — le cœur en virgule fixe inchangé.
REQ-SF-016Un build, jalon par jalon
Exigences et preuves
Les exigences s’analysent avec des identifiants uniques ; le paquet Lean entier — spécifications, bibliothèque de sémantique, chaque théorème — s’élabore et se vérifie par le noyau.
Export frais
Chaque artefact dérivé de Lean est régénéré à partir des modules qui viennent d’être vérifiés, et une fonction mal formée est refusée à l’export.
Passages de relais fixés par empreinte
L’IR, les sources de spécification et la bibliothèque de sémantique sont hachés par Lean et par Rust, et les deux doivent concorder.
Traçabilité
Chaque exigence est satisfaite par une fonction, et chaque fonction ne cite que des exigences connues.
Deux générateurs, un seul programme
« 9 fonctions identiques en AST entre sgen-a et sgen-b », puis canoniques au bit près entre les deux.
Certificats
Par fonction, cinq théorèmes sur l’artefact tel que reparsé à partir des octets livrés, vérifiés par le noyau Lean.
Rejeu
Vecteurs de référence Lean face au code compilé sur l’hôte, puis par fonction sur la cible émulée, chaque ELF haché.
Preuves
Certificats, matrice de traçabilité, manifeste de comparaison dos à dos et transcription sur cible assemblés en un seul dossier.
Vérifié par quelqu’un d’autre que le pipeline
Le guide de preuves donne à un évaluateur cinq procédures qui ne dépendent pas du propre rapport du pipeline, chacune exécutée telle qu’écrite. Pour flow_gauge : un troisième SHA-256 de la source de spécification correspond aux deux empreintes enregistrées et à l’en-tête du certificat ; le certificat se réexécute à travers le noyau avec un code de sortie 0 et ne dépend que de propext et de Quot.sound ; et l’ELF rejoué à la main affiche « B2BT flow_gauge cases=406 failed=0 float_cases=78 » avec une empreinte égale à celle des preuves.
Le guide est tout aussi explicite sur les limites : la validité des exigences reste une revue humaine, aucune affirmation ne concerne le timing ou les bornes de pile, et QEMU n’est pas du silicium.
Continuer à explorer
Cas d’usage associés
Commande et apprentissage par renforcementCommande et RL du pendule inversé sur chariotLe benchmark canonique de la commande sous-actionnée, traité de bout en bout — dynamique non linéaire, un LQR qui stabilise le pendule inversé, une mise en mouvement par énergie, une politique d’apprentissage par renforcement sans modèle, et un jalon de robustesse par Monte-Carlo.
DjiniousLab
ÉlectromagnétismeÉlectromagnétisme (FDTD)Résoudre les équations de Maxwell sur une grille — les champs électrique et magnétique progressant en léapfrog dans l’espace et le temps. Un solveur FDTD autonome reproduit les phénomènes ondulatoires canoniques : rayonnement, réfraction, diffraction, diffusion et résonance de cavité. Le pendant en électromagnétisme du solveur de champ CFD.DjiniousLab
Apprentissage automatique scientifiqueML scientifique (UDE)Découvrir la physique manquante à partir des données avec les équations différentielles universelles (UDE) — conserver la physique connue, apprendre l’écart avec un réseau de neurones entraîné à travers le solveur d’EDO, puis relire le terme appris sous forme d’équation symbolique qui extrapole là où une boîte noire ne le peut pas.DjiniousLab