ASELSANMicrokernel
S547 · AYRI İŞLEM VE TERMİNAL KANITI

S547 · R1 ekran: VideoCore mailbox framebuffer tahsis sözleşmesi

Bu statik detail route yalnız S547 kapısına aittir. Kaynak, focused test, regresyon, sınır ve yayın kanıtları komşu kapıların başarılarıyla birleştirilmez.

  1. PASSGLOBAL UMBRELLA PARTIAL · DAR PASS

    S547 · R1 ekran: VideoCore mailbox framebuffer tahsis sözleşmesi

    S547 kaynak/host model kapısı PASS'tir: Raspberry Pi 5 HDMI ilk-piksel yolunun VideoCore property-mailbox framebuffer tahsis işlemi, 36 word / 144 B / 16-byte katlı property buffer düzeni, yedi tag (0x00048003 fiziksel boyut, 0x00048004 sanal boyut, 0x00048005 derinlik 32, 0x00048006 piksel sırası BGR, 0x00040001 tahsis 4096 hizalı, 0x00040008 pitch, 0x00048009 sanal offset), 0x80000000/0x80000001 yanıt kodları, bus→ARM adres dönüşümü (& 0x3FFFFFFF) ve pitch >= width*4 / size >= pitch*height denetimleriyle fail-closed olarak modellendi. Varsayılan hedef 720x1280 portre Touch Display 2 profili, laboratuvar profili 1920x1080 HDMI'dır; her iki profil G8lS547FramebufferAllocationReceipt ve FramebufferCap tohum alanları (phys_addr, width, height, stride, Bgra8888) üretir. Focused 19/19 PASS'tir. S540 ve S543 fiziksel RED immutable kalır; physical observation=0, MMIO=0, donanım yoktur ve RUNBOOK_EXECUTED_IN_S547=NO'dur. S548 bu receipt'ten tohumlanan framebuffer capability'sine host-modelli test deseni bağlama kapısıdır.

    Doğrulanan kanıt

    • S547, S546'dan ayrı bir source/host model module, 19-test focused binary, proof, status manifest, Operations kaydı ve complete Code kartına sahiptir; hiçbir production callsite, boot/IRQ/scheduler/driver bağlantısı yoktur.
    • Dar S547 source-model status=PASS; R1 umbrella=PARTIAL ve S540/S543 physical gate status=RED olarak ayrı tutulur.
    • Property buffer düzeni exact 36 word / 144 B'dir ve driver::mailbox PropertyBuffer data: [u32; 36] adlandırmasını değiştirmeden yansıtır; kanal 8, word 0 boyut, word 1 istek kodu 0, word 34 end tag 0, word 35 padding 0'dır.
    • Tag tablosu exact word indeksleriyle sabittir: 0x00048003 @2, 0x00048004 @7, 0x00048005 @12 (32 bit), 0x00048006 @16 (BGR=0), 0x00040001 @20 (hizalama 4096), 0x00040008 @25, 0x00048009 @29 (offset 0,0).
    • Yanıt kodu yalnız 0x80000000 kabul edilir; 0x80000001 firmware parse hatası, diğer her değer geçersiz yanıt kodu olarak fail-closed döner.
    • Her tag çerçevesinde kimlik, değer boyutu, 0x80000000 yanıt biti ve exact yanıt uzunluğu doğrulanır; zincir word 34'te bitmezse veya padding sıfır değilse reddedilir.
    • Fiziksel boyut, sanal boyut, derinlik 32, piksel sırası BGR ve sanal offset (0,0) echo'ları exact olmalıdır; herhangi bir sapma ilgili drift hatasını üretir.
    • Bus adresi sıfır olamaz; ARM adresi bus & 0x3FFFFFFF ile türetilir, sıfır olamaz ve 4096 hizalı olmalıdır; buffer boyutu sıfır olamaz.
    • pitch >= width*4 (checked çarpma), pitch % 4 == 0, size >= pitch*height (checked çarpma) ve ARM adresi + size u32 taşması denetimleri uygulanır; taşma durumları ayrı diagnostic kodlarıyla reddedilir.
    • Portre profili 720x1280 için minimum pitch 2880 B ve minimum boyut 3686400 B; HDMI laboratuvar profili 1920x1080 için 7680 B ve 8294400 B'dir; firmware'in daha geniş pitch döndürmesi (örn. 3072 veya 8192) kabul edilir.
    • Receipt exact bir kez yayımlanır; aynı profil ve aynı yanıt kelimeleriyle replay Retained döner, farklı profil veya yanıt PublishedStateDrift ile fail-closed reddedilir.
    • Yirmi beş hata varyantının diagnostic kodları sıfırdan farklı ve benzersizdir.
    • Focused target 1 grup / 19 passed / 0 failed / 0 ignored / 0 filtered verdi.
    • Implementation 23979 B / ee0cba46519f790f84e18eac133e9bfd8a7b9dd4bf24fe2dc62f8e8f543c1b57; focused test 19792 B / 17bd3072b422e8096e88079a6a3c54ddd54ee9848294ae7d9331af1601e51ca6 SHA-256'dır.
    • Proof 4740 B'dir.
    • Kaynak unsafe, asm!, write_volatile, crate::uart, crate::arch, #[no_mangle] veya spin:: içermez; mailbox MMIO yapılmaz ve firmware yanıtı focused test tarafından host üzerinde sentezlenir.
    • S540 ve S543 immutable raw ve fiziksel RED kararları byte-exact korunur; automatic promotion=false'dur ve S546 kararı varsayılmaz.
    • RUNBOOK_EXECUTED_IN_S547=NO; supported-profile runtime observations=0, physical observations=0, SD/UART/power/new-raw=0/0/0/0, Boot-to-UI physically observed=false ve R1 acceptance=false'dur.
    • S548 yalnız host üzerinde S547 receipt'inden tohumlanan framebuffer capability'sine test deseni bağlayacaktır; aygıt veya fiziksel koşu yetkisi değildir.

    Sınır / bekleyen kanıt

    • S547 yalnız host üzerinde çalışan bir kaynak modelidir; hiçbir donanım/panel/modem/board gözlemi yoktur ve VideoCore firmware yanıtı sentezlenmiştir.
    • Mailbox MMIO, framebuffer belleğine yazma veya gerçek piksel çıkışı yapılmamıştır; BOOT_TO_UI_READY gerçek UART'ta görülmedi, Boot-to-UI ve R1 acceptance false kalır.
    • S540 ve S543 fiziksel RED immutable kalır; S546 üçüncü fiziksel koşunun kararı bu kapıda varsayılmaz veya yükseltilmez.
    • Modül hiçbir boot, IRQ, scheduler veya driver yoluna bağlı değildir; driver::mailbox değiştirilmemiştir.
    • S548 host-only test deseni ve capability bağlama kapısıdır; yeni SD/UART/power koşusu ayrı kapı, fresh target revalidation, açık operatör yetkisi ve yeni immutable raw ister.

    Terminal komutları ve gerçek yanıtlar

    S547 mailbox framebuffer allocation contract focused
    TAM ÇIKTIexit 0
    Komut
    $ CARGO_INCREMENTAL=0 cargo test -p aselsan_microkernel_simulation --test g8l_target_dispatch_scheduler_owner_scheduler_mutation_production_migration_lifecycle_s547_r1_display_mailbox_framebuffer_allocation_contract -- --test-threads=1
    Yanıt
    test result: ok. 19 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s
S547 focused=1 group / 19 passed / 0 failed
hardware=none physical=0 runbook=NO