Fix namespace declarations and add missing type annotations in Lean files

02_FORMAL/lean/RIINA.lean

@@ -1,9 +1,8 @@
 -- Domain files (bulk of theorems — compile independently)
 import RIINA.Domains.All
--- MobileOS, Industries, Compliance excluded: transpiler .mk constructor bug
--- import RIINA.Domains.MobileOS
--- import RIINA.Industries
--- import RIINA.Compliance
+import RIINA.Domains.MobileOS
+import RIINA.Industries
+import RIINA.Compliance
 -- Core files depend on Foundations.Syntax/Semantics which need hand-written Lean port.
 -- Excluded until transpiler generates valid Lean for core Coq definitions.
 -- import RIINA.Foundations.Syntax

02_FORMAL/lean/RIINA/Compliance/DO178CCompliance.lean

@@ -88,28 +88,33 @@ Generated by scripts/generate-multiprover.py
 | DAL_A_Full_Compliance | DAL_A_Full_Compliance | OK |
 -/
 
-namespace RIINA
+namespace RIINA.Compliance.DO178CCompliance
 
 /-- Coq compatibility shim: boolean negation -/
 @[inline] def negb (b : Bool) : Bool := !b
 /-- Coq compatibility shim: boolean conjunction -/
 @[inline] def andb (a b : Bool) : Bool := a && b
 /-- Coq compatibility shim: boolean disjunction -/
 @[inline] def orb (a b : Bool) : Bool := a || b
-/-- Coq compatibility shim: list universal predicate -/
+/-- Coq compatibility shim: List universal predicate -/
 @[inline] def forallb {α : Type} (f : α → Bool) (xs : List α) : Bool := xs.all f
-/-- Coq compatibility shim: list existential predicate -/
+/-- Coq compatibility shim: List existential predicate -/
 @[inline] def existsb {α : Type} (f : α → Bool) (xs : List α) : Bool := xs.any f
-/-- Coq compatibility shim: list length alias -/
+/-- Coq compatibility shim: List length alias -/
 @[inline] def length {α : Type} (xs : List α) : Nat := xs.length
-/-- Coq compatibility shim: list head option -/
+/-- Coq compatibility shim: List head option -/
 @[inline] def hd_error {α : Type} (xs : List α) : Option α := xs.head?
-/-- Coq compatibility shim: list find option -/
+/-- Coq compatibility shim: List find option -/
 @[inline] def find {α : Type} (p : α → Bool) (xs : List α) : Option α := xs.find? p
 /-- Coq compatibility shim: pair first projection -/
 @[inline] def fst {α β : Type} (p : α × β) : α := p.1
 /-- Coq compatibility shim: pair second projection -/
 @[inline] def snd {α β : Type} (p : α × β) : β := p.2
+/-- Coq compatibility shim: List membership -/
+@[inline] def In {α : Type} (x : α) (xs : List α) : Prop := x ∈ xs
+/-- Coq compatibility: check if pair is in list -/
+def pair_in_list {α : Type} [DecidableEq α] (p : α) (xs : List α) : Bool := xs.any (fun x => x == p)
+
 
 /-- Boolean conjunction iff (matches Coq: andb_true_iff) -/
 private theorem andb_true_iff (a b : Bool) :
@@ -118,6 +123,13 @@ private theorem andb_true_iff (a b : Bool) :
   · intro h; cases a <;> cases b <;> simp_all
   · intro ⟨ha, hb⟩; simp [ha, hb]
 
+/-- Coq compatibility: Nat equality test -/
+def Nat.eqb (a b : Nat) : Bool := a == b
+/-- Coq compatibility: Nat less-or-equal test -/
+def Nat.leb (a b : Nat) : Bool := decide (a ≤ b)
+/-- Coq compatibility: Nat less-than test -/
+def Nat.ltb (a b : Nat) : Bool := decide (a < b)
+
 /-- DAL (matches Coq: Inductive DAL) -/
 inductive DAL where
   | DAL_A : DAL
@@ -153,8 +165,8 @@ abbrev mkReq := Requirement.mk
 /-- TraceLink (matches Coq: Record TraceLink) -/
 structure TraceLink where
   trace_req : Requirement
-  trace_code : List
-  trace_tests : List
+  trace_code : List Nat
+  trace_tests : List Nat
   deriving DecidableEq, Repr
 /-- Coq constructor alias for TraceLink. -/
 abbrev mkTrace := TraceLink.mk
@@ -173,10 +185,10 @@ abbrev mkCov := CoverageData.mk
 
 /-- CodeAnalysis (matches Coq: Record CodeAnalysis) -/
 structure CodeAnalysis where
-  ca_all_code : List
-  ca_reachable_code : List
-  ca_deactivated_code : List
-  ca_deactivated_documented : List
+  ca_all_code : List Nat
+  ca_reachable_code : List Nat
+  ca_deactivated_code : List Nat
+  ca_deactivated_documented : List Nat
   deriving DecidableEq, Repr
 /-- Coq constructor alias for CodeAnalysis. -/
 abbrev mkCodeAnalysis := CodeAnalysis.mk
@@ -185,7 +197,7 @@ abbrev mkCodeAnalysis := CodeAnalysis.mk
 structure StackAnalysis where
   stack_allocated : Nat
   stack_max_usage : Nat
-  stack_per_function : List
+  stack_per_function : List (Nat × Nat)
   deriving DecidableEq, Repr
 /-- Coq constructor alias for StackAnalysis. -/
 abbrev mkStack := StackAnalysis.mk
@@ -222,24 +234,24 @@ abbrev mkInputVal := InputValidation.mk
 
 /-- ExceptionHandling (matches Coq: Record ExceptionHandling) -/
 structure ExceptionHandling where
-  eh_exception_types : List
-  eh_handled_types : List
+  eh_exception_types : List Nat
+  eh_handled_types : List Nat
   deriving DecidableEq, Repr
 /-- Coq constructor alias for ExceptionHandling. -/
 abbrev mkExcept := ExceptionHandling.mk
 
 /-- DataCoupling (matches Coq: Record DataCoupling) -/
 structure DataCoupling where
-  dc_data_dependencies : List
-  dc_documented_dependencies : List
+  dc_data_dependencies : List Nat
+  dc_documented_dependencies : List Nat
   deriving DecidableEq, Repr
 /-- Coq constructor alias for DataCoupling. -/
 abbrev mkDataCoupling := DataCoupling.mk
 
 /-- ControlCoupling (matches Coq: Record ControlCoupling) -/
 structure ControlCoupling where
-  cc_control_dependencies : List
-  cc_documented_dependencies : List
+  cc_control_dependencies : List Nat
+  cc_documented_dependencies : List Nat
   deriving DecidableEq, Repr
 /-- Coq constructor alias for ControlCoupling. -/
 abbrev mkControlCoupling := ControlCoupling.mk
@@ -255,16 +267,16 @@ abbrev mkSafety := SafetyProperty.mk
 
 /-- FunctionAnalysis (matches Coq: Record FunctionAnalysis) -/
 structure FunctionAnalysis where
-  fa_specified_functions : List
-  fa_implemented_functions : List
+  fa_specified_functions : List Nat
+  fa_implemented_functions : List Nat
   deriving DecidableEq, Repr
 /-- Coq constructor alias for FunctionAnalysis. -/
 abbrev mkFuncAnalysis := FunctionAnalysis.mk
 
 /-- RobustnessTest (matches Coq: Record RobustnessTest) -/
 structure RobustnessTest where
-  rt_invalid_input_types : List
-  rt_tested_invalid_inputs : List
+  rt_invalid_input_types : List Nat
+  rt_tested_invalid_inputs : List Nat
   rt_all_gracefully_handled : Bool
   deriving DecidableEq, Repr
 /-- Coq constructor alias for RobustnessTest. -/
@@ -314,21 +326,21 @@ abbrev mkConfig := ConfigurationManagement.mk
 /-- DO178CCompliance (matches Coq: Record DO178CCompliance) -/
 structure DO178CCompliance where
   comp_dal : DAL
-  comp_traces : List
+  comp_traces : List Nat
   comp_coverage : CoverageData
   comp_code_analysis : CodeAnalysis
   comp_stack : StackAnalysis
   comp_timing : TimingAnalysis
-  comp_partitions : List
-  comp_inputs : List
+  comp_partitions : List Nat
+  comp_inputs : List Nat
   comp_exceptions : ExceptionHandling
   comp_data_coupling : DataCoupling
   comp_control_coupling : ControlCoupling
-  comp_safety_props : List
+  comp_safety_props : List Nat
   comp_func_analysis : FunctionAnalysis
   comp_robustness : RobustnessTest
   comp_determinism : DeterminismAnalysis
-  comp_rt_tasks : List
+  comp_rt_tasks : List Nat
   comp_resources : ResourceUsage
   comp_config : ConfigurationManagement
   deriving DecidableEq, Repr
@@ -570,4 +582,4 @@ theorem COMPLY_003_20 : ∀ (c : DO178CCompliance), configuration_compliant (com
 theorem DAL_A_Full_Compliance : ∀ (c : DO178CCompliance), full_dal_a_compliance c = true → comp_dal c = DAL_A := by
   cases ‹_› <;> simp <;> omega
 
-end RIINA
+end RIINA.Compliance.DO178CCompliance

02_FORMAL/lean/RIINA/Compliance/HIPAACompliance.lean

@@ -61,28 +61,41 @@ Generated by scripts/generate-multiprover.py
 | COMPLY_001_15 | COMPLY_001_15 | OK |
 -/
 
-namespace RIINA
+namespace RIINA.Compliance.HIPAACompliance
 
 /-- Coq compatibility shim: boolean negation -/
 @[inline] def negb (b : Bool) : Bool := !b
 /-- Coq compatibility shim: boolean conjunction -/
 @[inline] def andb (a b : Bool) : Bool := a && b
 /-- Coq compatibility shim: boolean disjunction -/
 @[inline] def orb (a b : Bool) : Bool := a || b
-/-- Coq compatibility shim: list universal predicate -/
+/-- Coq compatibility shim: List universal predicate -/
 @[inline] def forallb {α : Type} (f : α → Bool) (xs : List α) : Bool := xs.all f
-/-- Coq compatibility shim: list existential predicate -/
+/-- Coq compatibility shim: List existential predicate -/
 @[inline] def existsb {α : Type} (f : α → Bool) (xs : List α) : Bool := xs.any f
-/-- Coq compatibility shim: list length alias -/
+/-- Coq compatibility shim: List length alias -/
 @[inline] def length {α : Type} (xs : List α) : Nat := xs.length
-/-- Coq compatibility shim: list head option -/
+/-- Coq compatibility shim: List head option -/
 @[inline] def hd_error {α : Type} (xs : List α) : Option α := xs.head?
-/-- Coq compatibility shim: list find option -/
+/-- Coq compatibility shim: List find option -/
 @[inline] def find {α : Type} (p : α → Bool) (xs : List α) : Option α := xs.find? p
 /-- Coq compatibility shim: pair first projection -/
 @[inline] def fst {α β : Type} (p : α × β) : α := p.1
 /-- Coq compatibility shim: pair second projection -/
 @[inline] def snd {α β : Type} (p : α × β) : β := p.2
+/-- Coq compatibility shim: list map -/
+@[inline] def map {α β : Type} (f : α → β) (xs : List α) : List β := xs.map f
+/-- Coq compatibility: Nat equality test -/
+def Nat.eqb (a b : Nat) : Bool := a == b
+/-- Coq compatibility: Nat less-or-equal test -/
+def Nat.leb (a b : Nat) : Bool := decide (a ≤ b)
+/-- Coq compatibility: Nat less-than test -/
+def Nat.ltb (a b : Nat) : Bool := decide (a < b)
+
+/-- Coq compatibility shim: List membership -/
+@[inline] def In {α : Type} (x : α) (xs : List α) : Prop := x ∈ xs
+/-- Coq compatibility shim: List filter -/
+@[inline] def filter {α : Type} (f : α → Bool) (xs : List α) : List α := xs.filter f
 
 /-- Role (matches Coq: Inductive Role) -/
 inductive Role where
@@ -127,7 +140,7 @@ inductive AuthFactor where
 
 /-- AuthState (matches Coq: Record AuthState) -/
 structure AuthState where
-  auth_factors : List
+  auth_factors : List Nat
   auth_user_id : Nat
   auth_timestamp : Nat
   deriving DecidableEq, Repr
@@ -171,7 +184,7 @@ structure BreachEvent where
   breach_detected_time : Nat
   breach_occurred_time : Nat
   breach_user_id : Nat
-  breach_phi_ids : List
+  breach_phi_ids : List Nat
   deriving DecidableEq, Repr
 /-- Coq constructor alias for BreachEvent. -/
 abbrev mkBreach := BreachEvent.mk
@@ -188,11 +201,11 @@ abbrev mkSession := Session.mk
 
 /-- SystemState (matches Coq: Record SystemState) -/
 structure SystemState where
-  state_phi_records : List
-  state_audit_log : List
-  state_active_sessions : List
-  state_user_roles : List
-  state_disposals : List
+  state_phi_records : List Nat
+  state_audit_log : List Nat
+  state_active_sessions : List Nat
+  state_user_roles : List Nat
+  state_disposals : List Nat
   state_current_time : Nat
   deriving DecidableEq, Repr
 /-- Coq constructor alias for SystemState. -/
@@ -210,7 +223,7 @@ abbrev mkTransmission := Transmission.mk
 
 /-- BREACH_DETECTION_LIMIT_S (matches Coq: Definition BREACH_DETECTION_LIMIT_S) -/
 def BREACH_DETECTION_LIMIT_S : Nat :=
-  Z.to_nat 86400%Z
+  86400
 
 /-- can_access (matches Coq: Definition can_access) -/
 def can_access (role : Role) (cat : PHICategory) : Bool :=
@@ -317,15 +330,15 @@ theorem COMPLY_001_02 : ∀ (ts : TransportSecurity), is_hipaa_transport ts = tr
   rfl
 
 /-- COMPLY_001_03 (matches Coq) -/
-theorem COMPLY_001_03 : ∀ (role : Role) (cat : PHICategory), can_access role cat = false → ~ (can_access role cat = true) := by
+theorem COMPLY_001_03 : ∀ (role : Role) (cat : PHICategory), can_access role cat = false → ¬(can_access role cat = true) := by
   simp_all [Bool.and_eq_true]
 
 /-- COMPLY_001_04 (matches Coq) -/
-theorem COMPLY_001_04 : ∀ (log : list AuditEntry) (user_id phi_id timestamp action : nat) (success : bool), let new_log := access_with_audit log user_id phi_id timestamp action success in audit_∃_for new_log user_id phi_id = true := by
+theorem COMPLY_001_04 : ∀ (log : List AuditEntry) (user_id phi_id timestamp action : Nat) (success : Bool), let new_log := access_with_audit log user_id phi_id timestamp action success in audit_exists_for new_log user_id phi_id = true := by
   simp
 
 /-- COMPLY_001_05 (matches Coq) -/
-theorem COMPLY_001_05 : ∀ (role : Role) (requested : list PHICategory) (cat : PHICategory), In cat (minimum_necessary_access role requested) → can_access role cat = true := by
+theorem COMPLY_001_05 : ∀ (role : Role) (requested : List PHICategory) (cat : PHICategory), In cat (minimum_necessary_access role requested) → can_access role cat = true := by
   simp_all [Bool.and_eq_true]
 
 /-- COMPLY_001_06 (matches Coq) -/
@@ -349,23 +362,29 @@ theorem COMPLY_001_10 : ∀ (auth : AuthState), is_mfa auth = true → length (a
   simp_all [Bool.and_eq_true]
 
 /-- COMPLY_001_11 (matches Coq) -/
-theorem COMPLY_001_11 : ∀ (current_time last_activity : nat), current_time - last_activity > session_timeout → session_expired current_time last_activity = true := by
+theorem COMPLY_001_11 : ∀ (current_time last_activity : Nat), current_time - last_activity > session_timeout → session_expired current_time last_activity = true := by
   simp_all [Bool.and_eq_true]
 
 /-- COMPLY_001_12 (matches Coq) -/
-theorem COMPLY_001_12 : ∀ (s : Session) (current_time : nat), session_is_active s = true → current_time - session_last_activity s > session_timeout → session_is_active (check_and_terminate current_time s) = false := by
+theorem COMPLY_001_12 : ∀ (s : Session) (current_time : Nat), session_is_active s = true → current_time - session_last_activity s > session_timeout → session_is_active (check_and_terminate current_time s) = false := by
   simp_all [Bool.and_eq_true]
 
+
+/-- Check if all user IDs in the list are unique -/
+def all_unique_ids (users : List (Nat × Role)) : Bool :=
+  let ids := users.map (fun p => p.1)
+  ids.length = ids.eraseDups.length
+
 /-- COMPLY_001_13 (matches Coq) -/
-theorem COMPLY_001_13 : ∀ (users : list (nat * Role)) (uid : nat) (r1 r2 : Role), all_unique_ids users = true → In (uid, r1) users → In (uid, r2) users → r1 = r2 := by
+theorem COMPLY_001_13 : ∀ (users : List (Nat * Role)) (uid : Nat) (r1 r2 : Role), all_unique_ids users = true → In (uid, r1) users → In (uid, r2) users → r1 = r2 := by
   cases ‹_› <;> simp
 
 /-- COMPLY_001_14 (matches Coq) -/
-theorem COMPLY_001_14 : ∀ (log : list AuditEntry) (user_id phi_id timestamp : nat) (cat : PHICategory), let new_log := emergency_access log user_id phi_id timestamp in audit_∃_for new_log user_id phi_id = true ∧ can_access Emergency cat = true := by
+theorem COMPLY_001_14 : ∀ (log : List AuditEntry) (user_id phi_id timestamp : Nat) (cat : PHICategory), let new_log := emergency_access log user_id phi_id timestamp in audit_exists_for new_log user_id phi_id = true ∧ can_access Emergency cat = true := by
   cases ‹_› <;> simp
 
 /-- COMPLY_001_15 (matches Coq) -/
 theorem COMPLY_001_15 : ∀ (t : Transmission), transmission_secure t = true → trans_security t = TLS13 ∧ phi_encryption (trans_phi t) = EncryptedAES256 ∧ trans_verified t = true := by
   simp_all [Bool.and_eq_true]
 
-end RIINA
+end RIINA.Compliance.HIPAACompliance