S565 · R1 güncelleme: aşamalı uygulama ve geri alma modeli

Doğrulanan kanıt

• S565, R1 telefon hedefinin A/B aşamalı güncelleme uygulama ve geri alma durum makinesini salt kaynak/host modeli olarak tanımlar; hiçbir SD kart, flash ortamı, panel, modem, board veya UART bu kapıda mevcut değildir ve journal/bariyer/güç kaybı yalnız bellekte modellenir.
• İki slot G8lS565SlotImage version, manifest hash, en fazla 8 entry kelimesi, boot_ok bayrağı ve S565_BOOT_TRIES_MAX=3 ile sınırlı tries_remaining taşır; slot tutarlılığı entry'lerin FNV-1a tarzı fold hash'inin manifest hash'e eşitliğiyle tanımlıdır ve baseline slot A version 1 / boot_ok=true, slot B boştur.
• Geçiş tablosu S565_TRANSITION_TABLE 11 açık satırdan oluşur: Idle→Staged (Stage), Staged→Verified (Verify), Staged/Verified→Idle (Abort), Verified→Committed (Apply, güç kaybında RolledBack), Committed/BootPending→BootPending (BootAttempt, sıfırda RolledBack), BootPending→Confirmed (ConfirmBoot), BootPending→RolledBack (Rollback) ve Confirmed/RolledBack→Idle (Finalize); tabloda olmayan her (durum, komut) çifti IllegalTransition'dır.
• Verify adımı manifest zinciri kararını chain_ok boolean'ı ve beklenen manifest hash olarak tüketir; S564 modülü import edilmez ve kapılar arası bağlaşım kurulmaz. chain_ok=false ManifestChainNotOk, hash uyumsuzluğu ExpectedManifestHashMismatch döner.
• Stage adımı 1..=8 entry, entry fold'una eşit manifest hash ve aktif slottan kesin yeni sürüm ister; bayat veya eşit sürüm VersionNotNewer ile reddedilir (anti-rollback).
• Apply, sıralı journal'ı kurar: hedef slota entry başına EntryWrite, FsyncBarrier, tek kayıtlık ManifestCommit (version, hash, entry sayısı, boot_ok=false, tries=3), FsyncBarrier, ActiveSwitch, FsyncBarrier; kapasite S565_JOURNAL_CAPACITY=16 ve en büyük kullanılan uzunluk 13'tür.
• Journal doğrulaması aktif slota yazan kaydı (JournalTargetsActiveSlot), 8 üstü entry indeks/sayısını, kapasite aşımını ve son entry yazısı ile manifest commit arasında veya commit ile switch arasında bariyeri eksik şekli (JournalBarrierMissing) uygulama başlamadan reddeder.
• Güç kaybı k indeksinde modellenir: k'den önceki son bariyere kadar olan kayıtlar dayanıklıdır, sonrası entry yazıları S565_TORN_WRITE_MASK ile yırtılır ve manifest/switch kayıtları düşer; focused test her k∈0..=journal_len için replay yapar ve switch dayanıklı değilken eski slotun bayt-özdeş tutarlı, dayanıklıyken yeni slotun yeni sürümle tam tutarlı olduğunu doğrular.
• Aynı süpürme service üzerinden tam olarak bir Committed (kayıpsız koşu) ve diğer her indekste PowerLossRecovered→RolledBack üretir; yırtık hedef slot kurtarmada geçersizlenir, eski slot dokunulmamış kalır ve Finalize ile Idle'a dönülür.
• Her BootAttempt tries_remaining'i azaltır (3→2→1→0); sıfırdaki deneme otomatik geri almadır: aktif işaretçi eski slota döner, reddedilen slotun boot_ok'u false kalır ve durum RolledBack olur. ConfirmBoot boot_ok=true ile Confirmed, Rollback manuel geri alma yoludur.
• Kabul edilen her komut sequence=565, predecessor=564, artan transition_sequence, komut id/kind, from/to durum, aktif/hedef slot, iki slot özeti, journal/dayanıklı/yırtık uzunlukları, hardware_present=false, physical_observations=0 ve runbook_executed=false alanlı bir G8lS565UpdateReceipt üretir.
• service_s565_model_staged_update sonraki anlık görüntüyü yerel kopyada hesaplar ve yalnız başarıda commit eder; komut id'leri bitişik olmak zorundadır, son kabul edilen komutun birebir tekrarı Retained ile aynı receipt'i döndürür ve aynı id altında farklı payload PublishedCommandDivergence'tır.
• On yedi hata kodu 1..=17 aralığında benzersiz ve sıfırdan farklıdır; aktif slot bozulması (inaktifken bozulup rollback hedefi olan slot dahil) ActiveSlotCorrupt ile fail-closed reddedilir ve her Err slotları, durumu, journal'ı ve sayaçları değiştirmeden bırakı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 journal, güç kaybı süpürmesi, otomatik geri alma, sıralama) içerir.
• Implementation 29548 B / 226862fbb3a85e5353f5a80e09f2f76e739ba5f75b945750a43cdcbaae297bd4; focused test 28573 B / 0ba7e32c573b14d2302576bcbd2f79bca4a90c45a8ef7291efbb0a472e77ab52 SHA-256'dır.
• Proof 7127 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.
• S565 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_S565=NO; supported-profile runtime observations=0, physical observations=0, hardware present=false, Boot-to-UI physically observed=false ve R1 acceptance=false'dur.
• S566 yalnız host üzerinde laboratuvar güncelleme gösterimi runbook sözleşmesini tanımlayacaktır; aygıt, SD, UART, güç veya fiziksel koşu yetkisi değildir.