This reverts commit 6d65ee90e8 and d269e429d0

@@ -1075,0 +1076,4 @@
+                                    (slice, false)
+                                }
+                                _ => {
+                                    eprintln!("attributes not annotated with `Kernel` or `KernelInvariants` at {}", &annotation.location);

@@ -1071,0 +1066,4 @@
+                                        ast::ExprKind::Subscript { value, .. }
+                                            if matches!(&value.node, ast::ExprKind::Name { id, .. } if id == &"list".into()) =>
+                                        {
+                                            return Err(format!("list is not allowed to be `Kernel` at {}", value.location))

@@ -1070,1 +1061,3 @@
-                                            None
+                            let (annotation, mutable) = match &annotation.node {
+                                ast::ExprKind::Subscript { value, slice, .. }
+                                    if matches!(&value.node, ast::ExprKind::Name { id, .. } if id == &"Kernel".into()) =>

@@ -93,0 +113,4 @@
+    if not isclass(cls):
+        raise ValueError("nac3 annotation decorator should only be applied to classes")
+    if not cls.__setattr__ in {base.__setattr__ for base in cls.__bases__}:
+        raise ValueError("custom __setattr__ is not supported in kernel classes")

@@ -9,6 +9,11 @@ use crate::{
 
 use super::*;
 
+pub enum CoreMode {

@@ -26,2 +31,4 @@
     // number of built-in function and classes in the definition list, later skip
     pub builtin_num: usize,
+    // indicate the mode that we are using the core
+    pub mode: CoreMode,

@@ -50,1 +47,3 @@
-    let (mut composer, builtins_def, builtins_ty) = TopLevelComposer::new(vec![]);
+    let (mut composer, builtins_def, builtins_ty) = TopLevelComposer::new(
+        vec![],
+        ComposerConfig { kernel_ann: None, kernel_invariant_ann: "Invariant" }

@@ -25,11 +30,16 @@ pub struct TopLevelComposer {
     pub method_class: HashMap<DefinitionId, DefinitionId>,
     // number of built-in function and classes in the definition list, later skip
     pub builtin_num: usize,
+    // indicate the mode that we are using the core

@@ -379,0 +381,4 @@
+        let (mut composer, _, _) = TopLevelComposer::new(self.builtins.clone(), ComposerConfig {
+            kernel_ann: Some("Kernel"),
+            kernel_invariant_ann: "KernelInvariant"
+        });

@@ -243,0 +242,4 @@
+        let (_, builtins_def, builtins_ty) = TopLevelComposer::new(builtins.clone(), ComposerConfig {
+            kernel_ann: Some("Kernel"),
+            kernel_invariant_ann: "KernelInvariant"
+        });