S553 · R1 ekran: kilit/durum/ayar ekranları system UI akış modeli

Doğrulanan kanıt

• S553, kernel/src/ui/scene.rs retained Scene/Layer soyutlamasının üzerine oturacak kontrollü system-UI akışını Lock, Home (durum), Settings ve App (placeholder) sahneleriyle salt kaynak/host modeli olarak tanımlar; hiçbir panel, dokunmatik denetleyici, framebuffer grant, modem, board veya UART bu kapıda mevcut değildir.
• Geçiş tablosu S553_TRANSITION_TABLE 11 açık satırdan oluşur: Lock→Home (gesture yalnız PIN_REQUIRED=0 iken, PinEntry sabit-zamanlı eşleşmede), Home→Settings/App push, Home Back→Lock, Settings ToggleSetting stay, Settings/App Back pop, Settings→App ve App→Settings push; tabloda olmayan her (sahne, olay) çifti InvalidTransition ile reddedilir.
• Lock sahnesinden OpenSettings açık bir guard satırıyla SettingsFromLockForbidden döner; Lock'tan OpenApp, Back ve ToggleSetting InvalidTransition'dır.
• PIN karşılaştırması s553_pin_matches_constant_time ile tüm 4 haneyi XOR-OR biriktirerek erken dönüşsüz yapılır; 9'dan büyük hane PinDigitOutOfRange ile reddedilir.
• S553_MAX_PIN_ATTEMPTS=5'tir; altıncı ardışık hatalı PIN LockedOut sonucu üretir, lockout_count checked u8 ile artar, deneme sayacı sıfırlanır ve lockout_release_tick=tick+3000 (30 s, 100 Hz) checked u64 ile hesaplanır; kilit süresince her unlock olayı Err(LockedOut) döner ve serbest bırakma tick'ine ulaşan Tick kilidi kaldırır.
• Sahne yığını S553_SCENE_STACK_MAX_DEPTH=4 ile sınırlıdır; dördüncü push kabul edilir, beşinci push SceneStackOverflow ile reddedilir ve yığın değişmez.
• Ayar deposu 8 slotluk u8 bayraktır (anahtar 0 = PIN_REQUIRED, varsayılan 1); ToggleSetting yalnız Settings sahnesinde, anahtar<8 ve değer<=1 iken kabul edilir, 8 ve 255 anahtarları SettingKeyOutOfRange döner.
• Durum çubuğu pil 0..=100, sinyal 0..=5 ve tick sayısından türetilen HH:MM saati (minute_of_day = tick/6000 % 1440) beş baytlık ASCII clock_text ile taşır; 101 pil, 6/255 sinyal ve tick gerilemesi fail-closed reddedilir; u64::MAX tick 00:18 olarak sarar.
• Her kabul edilen olay sequence=553, predecessor=552, artan transition_sequence, olay id/kind, from/to sahne, tam yığın, durum çubuğu, ayar anlık görüntüsü, deneme/lockout sayaçları, hardware_present=false, physical_observations=0 ve runbook_executed=false alanlı bir G8lS553SceneReceipt üretir.
• service_s553_model_scene_flow sonraki anlık görüntüyü yerel olarak hesaplar ve yalnız başarıda commit eder; olay id'leri bitişik olmak zorundadır (0, atlanmış, bayat ve u64::MAX id EventOrder), son kabul edilen olayın birebir tekrarı Retained ile aynı receipt'i döndürür, aynı id altında farklı payload PublishedEventDivergence'tır.
• On yedi hata kodu 1..=17 aralığında benzersiz ve sıfırdan farklıdır; TickOverflow (u64::MAX-1 tick'te altıncı hatalı PIN) ve LockoutCounterOverflow (255 lockout sonrası 256.) focused testte doğrulanmıştır.
• Focused target 1 grup / 24 passed / 0 failed / 0 ignored / 0 filtered verdi; 6 sözleşme testi ve 18 alan testi (mutlu yol, sınır değerleri, bozuk girdi, taşma, sıralama) içerir.
• Implementation 23913 B / cedaf20d38f88ff1914ff08e858b0240e57c279495ea0a9e86b40aef55cc1745; focused test 24302 B / 60edc05d1b322d449748d9761fd6a635e2edab6484672b8bbc5fe5b4f8f09f29 SHA-256'dır.
• Proof 6202 B'dır.
• Modül hiçbir boot, IRQ, scheduler veya sürücü yoluna bağlanmamıştır; unsafe, asm!, write_volatile, crate::uart, crate::arch, #[no_mangle] ve spin:: yüzeyi içermez.
• S540 immutable raw 20525 B ve S543 immutable raw 20509 B fiziksel RED kararlarıyla byte-exact korunur; automatic promotion=false ve rerun=false'dur.
• S553 sırasında candidate freeze, SD write/read-back/eject, UART open/capture, power transition, fiziksel koşu veya yeni immutable raw üretimi yapılmadı.
• RUNBOOK_EXECUTED_IN_S553=NO; supported-profile runtime observations=0, physical observations=0, hardware present=false, Boot-to-UI physically observed=false ve R1 acceptance=false'dur.
• S554 yalnız host üzerinde modem AT komut taşıma çerçeveleme modelini tanımlayacaktır; aygıt, modem veya fiziksel koşu yetkisi değildir.