-
Notifications
You must be signed in to change notification settings - Fork 0
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
[G0-06] Mechanize K0 metatheory and lock the proof TCB
area:formal-methodsMechanized metatheory and proof checkingMechanized metatheory and proof checkingg0-blockerBlocks the G0 formal implementation gateBlocks the G0 formal implementation gatestatus:no-goDurable implementation work is not authorizedDurable implementation work is not authorizedStatus: Open.[G0-04] Cover every K0 and memory Rule ID
area:conformanceRule coverage and conformance evidenceRule coverage and conformance evidenceg0-blockerBlocks the G0 formal implementation gateBlocks the G0 formal implementation gatestatus:no-goDurable implementation work is not authorizedDurable implementation work is not authorizedStatus: Open.[G0-03] Complete K0 object and resource state machines
area:memoryObject, ownership, borrow, and allocation modelObject, ownership, borrow, and allocation modelg0-blockerBlocks the G0 formal implementation gateBlocks the G0 formal implementation gatestatus:no-goDurable implementation work is not authorizedDurable implementation work is not authorizedStatus: Open.[G0-02] Complete K0 Core grammar and operational semantics
area:semanticsCore static or dynamic semanticsCore static or dynamic semanticsg0-blockerBlocks the G0 formal implementation gateBlocks the G0 formal implementation gatestatus:no-goDurable implementation work is not authorizedDurable implementation work is not authorizedStatus: Open.[G0-08] Prove K1 and K2 are unreachable from K0 inputs
area:layeringK0/K1/K2 isolation and feature reachabilityK0/K1/K2 isolation and feature reachabilityg0-blockerBlocks the G0 formal implementation gateBlocks the G0 formal implementation gatestatus:no-goDurable implementation work is not authorizedDurable implementation work is not authorizedStatus: Open.