Static analysis of explicit purity constraints in Go: Design and verification of mikoto

Overview

I created mikoto (source), a tool that checks the length of Go functions and the purity constraints explicitly specified for functions. By annotating a function declaration with //mikoto:pure, it inspects inputs and outputs that use only value types, access to package variables, modifications of referenced objects, pointer indirection, call targets, and so on. The implementation uses Go’s AST and type information, limiting the scope of inspection to function declarations within the same package.

The motivation stems from the difficulty of repeatedly having humans re‑examine design intent as codebases grow. Even if a function is intended to “simply compute a result from its inputs,” adding later references to the current time or updates to shared state changes that premise. Therefore, we explicitly encode the desired constraints in the source code and have the tool diagnose any implementation that violates those constraints.

When we examined the initial implementation, we discovered that it missed map traversals through type parameters and implicit indirections of array pointers, while also incorrectly rejecting legitimate generic calls and parenthesized expressions. PR #6 (PR #6) addressed these issues as well as the line‑count calculation problem. In this article we present the inspection model, the implementation, examples of fixes, and verification results, and we consider what can be concluded—and what cannot—when no diagnostics are reported.

The following serves as a development record that separates problem definition from evaluation, akin to an academic paper, but it is not a report that proves referential transparency for arbitrary Go programs. The target is main as of September 30 2026, and commit 2235f226aa (source). We distinguish between the proposed usage and the behavior that can be verified by the implementation.

1. Background and Problem Definition

1.1 Implementation Growth and Verification Effort Do Not Increase at the Same Rate

In the article “AI Coding and Code Review” (source), we argued that we should not rely on humans to read every line of code at the same density, but instead strengthen specifications, tests, static analysis, and observability. Mikoto is an attempt to mechanically verify design constraints, starting with a small scope.

In code reviews, we check not only the correctness of each individual expression but also whether a function’s role has remained unchanged. For example, does a function that calculates fees also update the database? Does a function that classifies input directly read the current time? Has a function that performs a small calculation been extended with notifications, log output, or updates to a shared cache? None of these concerns are addressed by compiler type checking alone; they are design‑level issues.

Such changes are not necessarily bugs. Reading the current time or updating state may be required by the broader system. However, if you have separated the part that computes results from inputs and the part that reads from or writes to the outside world, then any decision to cross that boundary must be deliberate. We want to verify separately that the code works and that it stays within the intended responsibilities.

Thus, before asking an LLM each time whether a piece of code might have side effects, we consider using an analysis tool to flag explicitly prohibited syntax or dependencies. If the diagnostics correspond to operations in the source code, the developer who made the change can decide whether to move that operation out of the computational part or to alter the function’s responsibilities. This separates the task of detecting problems from the task of deciding how to handle them.

1.2 Handling Two Constraints with a Single Tool

Mikoto provides two kinds of checks: one on function length and another on the purity constraints explicitly specified for functions. The former applies to every target function, while the latter applies only to functions marked with the annotation. The default maximum length is 80 lines, and specifying -max-lines=0 disables the line‑count check.

The two aspects are related but not identical. A short function can still modify external state in complex ways, and a long function can perform only value transformations. Simply splitting a function into smaller pieces does not necessarily make its dependencies clearer. We treat line count as a metric for reconsidering the scope of reading, and purity constraints as a rule that limits relationships with external state, handling them independently.

The acceptable length for a single function varies by project policy. The default of 80 lines does not represent a universal quality boundary. Likewise, the goal is not to make every function pure. Functions that open files, send HTTP requests, or start transactions inherently have responsibilities that involve interacting with the outside world.

The question addressed in this article is narrower than “whether any Go function can be definitively classified as pure.” When we explicitly mark a function whose role should be limited to computing from its inputs, we ask how tightly and with how clear a rule we can inspect for operations that breach that boundary. Moreover, when we implement that rule using Go’s syntax and type system, we ask where the simple decision process inevitably breaks down.

2. How Purity Is Treated as a Property

2.1 Modifications to External State and Dependence on External State

When describing pure functions, the phrase “no side effects” alone is ambiguous. Even if a function does not write to external state, reading that state and using it to affect the result means the output is not determined solely by its inputs. A function that returns the current time can produce a different value for the same arguments, even though it does not itself alter the clock.

For example, the following two cases present different issues.

var rate = 2

func Multiply(n int) int {
    return n * rate
}

func Count(n int) int {
    rate++
    return n * 2
}

Multiply depends on the current value of a package variable. Count yields the same result for the same inputs when looking only at its return value, but calling it modifies external state. The determinism of the return value and the non‑modification of external state must be considered separately. Mikoto diagnoses both reads and writes to package variables from the annotated functions.

Conceptually, we can denote the arguments of x, the external state before the call as s, the return value as y, and the external state after the call as s', and express the function’s execution as follows.

execute(f, x, s) = (y, s')

Do not alter external state: s' = s
Result does not depend on external state: y = g(x)

This is a explanatory model; mikoto does not actually enumerate state spaces to verify it. Moreover, the meaning of the property changes depending on what is considered external state and what is observed. If we required that nothing about the machine’s state—including memory allocation or the garbage collector—change at all, virtually no ordinary computation would satisfy that condition. What we are concerned with here is the relationship between the computation’s result and the dependencies or modifications observable by the caller or the outside world.

2.2 Distance from Referential Transparency

Referential transparency can be described as the property that an expression can be replaced by its value without changing observable behavior. If a computation can be performed once and its result reused, or executed anew wherever needed, the location and frequency of that computation become easier to reason about.

However, in a program the return value is not the only thing that can be observed. Panics, infinite loops, resource consumption, floating‑point behavior, and differences in execution environments also matter. Moreover, it is not always sufficient to compare the return value using Go’s ==. There are values, such as NaN, that are not equal to themselves. We do not want to conflate semantically identical results with the outcome of a particular comparison operation.

The mikoto README (source code) also does not treat the checks as a formal proof of referential transparency. The absence of diagnostics simply means that no operations violating the current rules were detected. It does not generate a certificate that justifies memoization or changes in execution order.

Nevertheless, reducing the number of paths that read from or modify external state is worthwhile. When the cause is tied to the inputs, it becomes easier to construct test conditions and to organize the information needed for reproducibility when a failure occurs. Before achieving universal guarantees, this helps narrow the scope of investigation.

2.3 Allowing Modifications of Local Variables

Not modifying external state is not the same as never performing any assignments inside a function. For example, when summing integers, updating a local variable to accumulate the result does not change the caller’s state as long as that variable is not shared with the surrounding code.

//mikoto:pure
func Sum(n int) int {
    total := 0
    for i := range n {
        total += i
    }
    return total
}

The current mikoto accepts this function. It does not reject it simply because there are assignments to total and i. In ordinary assignments, the left‑hand side’s parentheses are stripped, and if the LHS is an identifier the assignment is allowed. If that identifier refers to a package variable, a separate check for references to package variables will diagnose it.

Conversely, assignments to array elements or struct fields are rejected even when the target is a local value. This asymmetry stems from implementation constraints rather than from the definition of purity itself. Because we do not include analysis that tracks whether a local array is shared with the surrounding code, we broadly restrict any operation whose left‑hand side is not a simple identifier. This point will be addressed both in the evaluation and in the discussion of limitations later.

3. Inspection Model and Scope of Application

3.1 Adopting Explicit Markers

The target of inspection is specified by the //mikoto:pure comment attached to a function declaration. It is not an approach that automatically extracts pure functions from all functions. The marker expresses the design intent of “apply this constraint to the function.”

//mikoto:pure
func Double(n int) int {
    return n * 2
}

The marker does not give the Go compiler any new meaning. In a normal compilation it remains just a comment. Only when mikoto is run is the function actually inspected. Therefore, adding markers and incorporating the inspection into the development process must be considered together.

In the current implementation, the tool examines a function’s doc comment, strips the line‑comment prefix and any surrounding whitespace, and checks whether the result matches mikoto:pure. Rather than inferring the inspected target from naming conventions or directory names, the marker is placed explicitly next to the declaration. Anyone reading the code can also see that the function is subject to a constraint.

Of course, if the marker is removed, the function will no longer be subject to purity checks. Mikoto does not implement a change‑approval rule to prevent this. Whether a change is deliberately altering a function’s responsibility or merely evading the check must be judged based on the context of the modification. Tool diagnostics alone cannot reveal the underlying design decisions.

3.2 Requiring Only Value‑Type Inputs and Outputs

For the arguments, return values, and method receivers of the specified functions, the current implementation requires types that the tool recognizes as value types. Basic types are allowed except for unsafe.Pointer, and arrays and structs are examined recursively for their elements or fields. Pointers, slices, maps, channels, interfaces, function types, and similar constructs do not satisfy this signature constraint.

Here, “value type” is a term used to explain mikoto’s rules; it does not introduce a new classification into Go’s type system. In Go, slices and maps are also values that can be assigned to variables. However, because copying such values can still share the underlying data, mikoto excludes them in order to keep the boundary between inputs and outputs as narrow as possible.

Types with predefined names are also examined by recursively descending to their underlying type via Underlying(). For example, type Amount int64 is treated as a basic type, while type Result struct {...}, which contains only value‑type fields, is recognized as a struct. This is not a method that simply checks whether the name string appears in an allow list.

On the other hand, the implementation does not restrict all local variables inside a function body to value types. Code that creates a slice from a local array, reads its elements, and returns an integer is accepted as an allowed example even in regression tests. The constraints on the function signature and the constraints on individual operations within the body are separate checks.

3.3 Restricting Call Targets

Calls from a specified function are limited to functions and methods marked with the marker in the same package, type conversions, and a set of permitted built‑in functions. The allowed built‑in functions are len, cap, complex, real, imag, min, and max.

This does not involve analyzing and inferring whether every possible call target is semantically pure. Functions that are not explicitly listed cannot be called, even if they perform only simple calculations. Numeric functions from the standard library are also generally disallowed under the current rules, because they are not among the designated functions of the same package.

Narrowing the constraints inevitably introduces practical inconvenience. However, when an external function is permitted, the scope of what that function may call and which states it may depend on also expands. The current mikoto chooses to keep that scope small. Sharing purity information with external packages or analyzing calls through function aliases are not features included in the existing implementation.

4. Implementation: Combining AST and Type Information

4.1 Foundations of Analysis

The CLI is launched via singlechecker.Main(checker.Analyzer). The analyzer is built on the framework of golang.org/x/tools/go/analysis and receives the target syntax tree together with type information. It is not an implementation that merely scans the source strings for * or go.

The AST represents how the source code is syntactically structured. Type information indicates which declaration an identifier refers to, whether an expression denotes a value or a type, whether a selector involves an implicit indirection, and so on. Mikoto uses these two pieces of information separately. Some checks can be performed based on syntax alone, while others require examining the types.

For example, an AST node labeled p[0] does not reveal whether p is an array, a slice, or a pointer to an array. The syntax represented by Double[int]() also includes nodes that look like simple array index accesses. Even when the name is identical—rate—the meaning to be inspected differs between a local variable and a package‑level variable.

flowchart TD
    S["Go source code"] --> A["AST and type information"]
    A --> M["Collect the specified functions"]
    M --> L["Check the physical line count of each function"]
    L --> P{"Whether a pure annotation is present"}
    P -->|Yes| V["Signature value‑type constraints"]
    V --> B["Body operations, name, and call targets"]
    B --> D["Diagnose violation locations"]
    P -->|No| E["Not subject to purity checking"]

In practice, finding a single diagnostic does not cause the tool to abort all checks immediately. Even for functions whose signatures do not meet the required conditions, the tool proceeds to inspect the function body and can emit multiple diagnostics. Conversely, when the analysis encounters a prohibited construct such as a closure, it may stop traversing its interior. The number of diagnostics should not be taken as a direct count of independent bugs.

4.2 Why Collect Markers First

run first scans the target file’s function declarations, storing the types.Object of each function that carries a marker in a set. It then revisits the function declarations to examine the line numbers and the function bodies.

By performing this in two stages, a function declared later in the source code can still be called from functions declared earlier. This avoids situations where the same‑package calls are allowed or disallowed depending on the order of files or the order of declarations. Because it relies on Go’s resolved declaration identity, it is easier to handle receiver types and name hiding than simply storing function names in a string set.

However, this set is not a collection of “functions that have been proven pure by the inspection,” but rather a collection of “functions that have been explicitly designated.” If a designated function violates the rules internally, a diagnostic is issued for that function itself. The caller is allowed to invoke it based on the marker. This is not a mechanism that propagates purity results throughout the entire call graph and computes a fixed point.

Therefore, it is important to verify collectively that no diagnostics are reported for the set of designated functions. One cannot assume that because no warning appears on a single line of the caller, the downstream code has also been verified. This distinction is essential for accurately describing the implementation in detail.

5. Function Length: What to Count

5.1 The Metric of Physical Line Count

The line‑count check measures the difference between the physical line numbers of a function’s start and end, then adds one. It counts every line occupied by the declaration, including blank lines and comments within the body. It does not count the number of statements, branches, or tokens. Argument declarations that span multiple lines are also included in the range.

function_lines = physical_end_line - physical_start_line + 1

Choosing physical line count means that even semantically identical code can yield different values depending on formatting. A long expression can be squeezed onto a single line to appear shorter, while adding explanatory comments can make it longer. Therefore, this is not a mathematical measure of complexity. It serves as a coarse indicator of how much reading effort a function written in typical style will require.

The implementation’s counting, which is done per function‑declaration node in the AST, also has its limits. It applies to FuncDecl that have a concrete function body, and it does not treat function literals—such as anonymous functions—as separate entities subject to the same line‑count check. Lines belonging to a function literal that is nested inside an outer function are counted as part of the outer function’s range, but the same constraints are not automatically applied to function literals used in package‑variable initializers or similar contexts.

5.2 //line Changed the Metric

In the initial implementation, line numbers were obtained from Fset.Position. In Go, //line can adjust the logical source position, so using this method can sometimes produce a discrepancy that differs from the actual number of lines in the file. Issue #5 shows an example of a function that physically has 12 lines but is not detected even when the limit is set to 8 lines.

func long() int {
    n := 0
    n++
    n++
    n++
    n++
    n++
    n++
    n++
//line imaginary.go:1
    return n
}

In this example, the displayed line numbers wrap around partway through the function. If the corrected numbers are used for both the start and the end, the function’s length can be calculated as zero lines. Conversely, advancing to a much larger line number can make a short function appear extremely long. This isn’t a bug that changes the meaning of the source code, but the line‑count metric was being dragged along by metadata intended for a different purpose.

The fix, introduced in PositionFor(pos, false), was to take the position without applying any correction. When compared with the documentation for FileSet.PositionFor (source), it becomes clear that the physical position is what’s needed for line‑count calculations. The position used for diagnostic display and the position used for metric calculation are not necessarily intended for the same purpose.

The regression tests include a case where line numbers are reduced to hide a function’s length and a case where they are increased to make a short function appear long. Fixing only the missed detections can leave false positives in the opposite direction. We defined the measurement criteria and verified, in both directions, that the result does not depend on whether corrections are applied.

6. Inspecting External State via Names and Assignments

6.1 Local Variables with the Same Name as Package Variables

When detecting access to package variables, the name alone is insufficient. For example, even if there is a package variable named state, a parameter or local variable with the same name inside a function may refer to a different value.

var state = 10

//mikoto:pure
func Local(state int) int {
    state++
    return state
}

The argument state is not a package variable. The current implementation retrieves the object referenced by the identifier in TypesInfo.Uses, then checks in types.Var whether that object’s scope is the package scope. The determination is based on the resolved binding rather than on name matching.

Package constants are not variables, so they are not subject to this rule’s diagnostics. Constants used for calculations are not treated the same as package variables that could be modified at runtime. Conversely, even for package variables that are intended to remain unchanged after initialization, mikoto diagnoses them without inferring that intention. If necessary, consider converting them to constants or passing the required values as arguments.

“The fact that the code does not actually change now” is different from “being able to infer from the type and declaration that it cannot change.” The current rule leans toward the latter. However, it does not perform a full‑program analysis to infer immutability. It treats any variable as evidence of external‑state access and uniformly restricts such accesses.

6.2 Restricting to Assignments to Identifiers

For ordinary assignments, the left‑hand side is normalized using ast.Unparen, and assignments that match Ident are permitted. All other cases are diagnosed as assignments through a reference. Increment/decrement operations are handled similarly: after removing any surrounding parentheses, we verify that the target is an identifier.

Consequently, n = 4, n++, (n) = 4, and (n)++ are treated the same when the target is a local integer. Parentheses change the shape of the syntax tree, but they do not alter the meaning of the assignment target we wish to inspect. In Issue #4 (issue #4), the initial implementation examined ParenExpr directly and consequently rejected even ordinary assignments.

On the other hand, the following code is still rejected today.

//mikoto:pure
func SetLocal(n int) [1]int {
    a := [1]int{}
    a[0] = n
    return a
}

Both the input and output are value types, and a is also a local array. This example does not contain any operation that modifies the caller’s array. However, because the left‑hand side is IndexExpr, it is diagnosed as pure function cannot assign through a reference. I confirmed this behavior with the current CLI while writing the article.

Interpreting this diagnostic as “Go arrays are always external references” is incorrect. The implementation adopts a simple rule that rejects any assignment target that matches this pattern, and the same restriction applies to assignments to local fields of a struct. To permit assignments that do not affect external state with precision, a separate analysis would be required.

For example, instead of setting each field individually and then returning the struct, you could construct a struct literal and return it; this approach does not violate the restriction. However, it is not always desirable to introduce many unnatural coding patterns merely to satisfy the tool. Whether the diagnostics clearly delineate design boundaries or simply make coding overly restrictive should be evaluated by looking at the set of functions to which they apply.

7. Nondeterministic Traversal and Generic Type Sets

7.1 Even Local Maps Can Depend on Order

Even if access to external state is prohibited, there remain execution paths that can produce different results from the same input. A clear example is iterating over a local map. Even without sharing the map externally, returning the first element encountered makes the traversal order affect the result.

//mikoto:pure
func First() int {
    m := map[int]int{1: 1, 2: 2}
    for k := range m {
        return k
    }
    return 0
}

The Go specification for range (source) does not guarantee any particular iteration order for maps. Even for the same map, code whose result depends on the order of iteration cannot expect deterministic behavior. Whether the map resides outside the function is a separate issue.

mikoto diagnoses range for maps, channels, and function types used as iterators. Traversals of arrays, slices, or integers are not rejected solely on that basis. Of course, if obtaining the iterable or the loop body contains other prohibited operations, those checks will apply.

Code that sums all elements of a map can sometimes produce a result that is independent of order. However, the implementation does not attempt to prove—and therefore permit—such cases by demonstrating that the operation’s nature or order does not affect the outcome. The current rule uniformly rejects any range over a map. When summing floating‑point numbers, the order of addition can affect rounding results, making it difficult to generalize that “summing everything is safe.”

A range over a channel involves communication, and a range over an iterator involves the behavior of the called function. These are not impure for the same reason. Although the diagnostic groups them together, the underlying reasons for imposing the restriction differ: order, communication, and the code being executed. Even if an iterator is actually pure, there is no mechanism to infer that and grant an exception.

7.2 Overlooking Type Parameters

In Issue #1 (issue #1), the diagnostic missed cases where a map’s type appears through a type parameter.

//mikoto:pure
func Nondeterministic[T ~map[int]int]() int {
    m := T{1: 1, 2: 2}
    for k := range m {
        return k
    }
    return 0
}

The initial implementation examined the type of the iterable in Underlying(), checking whether it was Map, Chan, or Signature. However, the type of m is TypeParam, whose underlying base type is an interface that expresses a constraint. Although the constraint explicitly permits maps, the check only looked at the immediate type classification, so the prohibited case was not detected.

In this example, the function has no parameters or return values involving type parameters. Consequently, the value‑type constraints in the signature alone cannot stop it. Even if the signature is narrowed, that does not eliminate paths within the function body that use type parameters. When combining multiple checks, it is better not to assume merely because one check exists that the other’s gaps become irrelevant.

In reproducing the issue, repeatedly invoking the same function produced both outcomes 1 and 2. However, there is no need to make the regression test depend on how often each outcome occurs. Rather than demanding that the map’s iteration order differ each time, it is sufficient to verify that the rule prohibiting map traversal also applies to this syntax. The lack of a guarantee in the specification and the observation of variability in a particular run are distinct matters.

7.3 Computing Intersections as Well as Unions

The fix added typeTerms (source code), which expands the type terms that appear in a type‑parameter’s constraints. It strips away type aliases, and when a type parameter is encountered, it proceeds to its constraints. Unions are formed by combining the terms, while embedded interfaces are treated as intersections of the constraints.

The crucial point here is that the rule does not simply reject any constraint that contains the word “map” even once. When multiple constraints are satisfied simultaneously, a map may be excluded from the final type set. The regression tests contain examples such as the following.

type First interface {
    ~[]int | ~map[int]int
}

type Second interface {
    ~[]int | ~map[string]int
}

type SliceIntersection interface {
    First
    Second
}

In First, either a map with integer keys or an integer slice is allowed; in Second, either a map with string keys or an integer slice is permitted. When considering a type that satisfies both constraints, the common element is the integer slice. If we simply collect the map cases, we end up issuing diagnostics for constraints that originally disallow maps.

First = slice or map[int]int
Second = slice or map[string]int

First ∩ Second = slice

In the current implementation, the set of terms for nil is treated as having no structural restrictions—an empty set—and an empty set that is not nil is handled as an empty intersection. When intersecting a term that includes ~ with a term of the exact type, we also verify whether their base types match. If we collapse this distinction into a single “term could not be obtained” message, we conflate a situation with no restrictions with one where no type can satisfy the constraints.

However, it is not appropriate to present this helper function as a complete prover for all Go type sets. The implementation expands the structural constraints needed for range and array‑pointer checks, but it does not fully resolve the additional narrowing imposed by method requirements. Here, too, we distinguish the processing of auxiliary type information from the semantics of type sets in general.

8. Indirect references can occur even without an explicit *p

8.1 Indexing an array pointer

The initial pointer‑checking implementation mainly focused on StarExpr. However, in Go, access through a pointer is not always expressed as *p. In Issue #2, an example showed that an index operation on an array pointer could read external mutable memory. (issue #2)

//mikoto:pure
func Read(addr uintptr) int {
    p := (*[1]int)(unsafe.Pointer(addr))
    return p[0]
}

This example requires an import of unsafe and is not the kind of code we would recommend for ordinary applications. It is used here to illustrate a gap in the checks. addr satisfies the signature condition as an integer, and type conversions are allowed during call inspection. In the final p[0], reading through an array pointer is presented syntactically as an index expression.

Even if the address supplied is the same integer, the result can change if the memory it points to changes. The fact that a signature involves only value types does not prove that the function body cannot reach external memory. This example shows that, beyond checking each rule individually, one must also consider how type conversions and implicit operations are linked.

After the fix, we verify whether the target type of an index expression is an array pointer, and issue a diagnostic if it is being accessed as a value. The same check is applied to p[:], which converts an array pointer to a slice. Determining whether a type is an array pointer uses the type‑term expansion described earlier, so named pointer types and those accessed through type parameters are also covered.

8.2 Field and method selection

Fields of a struct pointer can be read as p.N even without an explicit (*p).N. When invoking a method with a value receiver through a pointer, an indirect reference may be involved to obtain the value. A strategy that only looks for StarExpr will miss such operations.

The current check extracts the type‑information selection for SelectorExpr and issues a diagnostic if Indirect() is true. It examines not only the name of the method or the comment attached to the function, but also whether the call involves extracting a value through a pointer.

The regression tests include a case where a struct pointer is converted from uintptr to read a field, as well as a case where a pre‑specified value‑receiver method is called on that pointer. Even if the method itself carries a marker, it does not permit operations that obtain the receiver from external memory. The permission for the callee and the retrieval of the value passed to the call are separate checks.

This is also important when considering the granularity of static analysis. Just because a permitted function is being called does not guarantee that the entire call expression is safe. If prohibited operations occur while constructing arguments or receivers, they must be detected separately. A design that scans the whole AST of the program’s body also has the role of checking such surrounding expressions.

8.3 Range over array pointers requires case distinction

When iterating over an array pointer, the operation differs between obtaining the element’s value and merely obtaining its index. In the regression tests, a range that receives elements is diagnosed, whereas a range that uses only the indices of a fixed‑size array is accepted.

//mikoto:pure
func RangeIndices() int {
    var p *[2]int
    n := 0
    for i, _ := range p {
        n += i
    }
    return n
}

In this case, what is needed is the length of the array type as a constant, not the reading of each element. The implementation diagnoses an array‑pointer indirect reference when the value side of a range contains a variable that is not a blank identifier. It does not reject a type simply because a pointer appears in it; it also distinguishes what the operation is retrieving.

Conversely, with for _, v := range p, the referenced location is read in order to obtain the element’s value. This distinction cannot be captured by merely detecting the word “pointer.” One must gradually verify the meaning of operations through the types involved.

8.4 Inspecting the destination of a range

A range can not only declare new variables but also update existing destinations. When written as for p[0] = range n, the range writes to the referenced location as it progresses. This does not appear as a normal AssignStmt.

In the initial implementation, only the target of range was inspected, and its assignment destination was ignored. After the fix, when the token is ASSIGN, the same checks applied to ordinary assignments are performed on both the Key and the Value. The pointeraccess regression test (source code) includes cases where both assignment destinations are array elements.

The same semantic operation—modifying external state—is expressed by multiple language constructs. Having inspected assignment statements does not mean we have inspected all assignments. This bug demonstrated that the classification of AST nodes does not correspond one‑to‑one with the classification of operations we wish to forbid by design.

9. Identity of callees and syntactic normalization

9.1 Calls with type arguments

Issue #3 described a problem where a generic function that had been explicitly specified was rejected as an unspecified function when called with explicit type arguments. This occurred because the initial callee resolution handled only Ident and SelectorExpr. (issue #3)

//mikoto:pure
func Constant[T any]() int {
    return 1
}

//mikoto:pure
func Read() int {
    return Constant[int]()
}

Constant[int] is a syntax that includes type arguments, so it does not appear as a plain identifier. When there are multiple type arguments, it becomes a different node. Even if Go can resolve the callee, the parser may not process the entire syntax, preventing the result from being extracted.

In the fix, we use typeutil.Callee to obtain the callee object from the type information. Rather than manually stripping syntax step by step, we delegate more of this to Go’s analysis helper APIs. This also applies to generic functions and methods, aligning them with their original declarations.

9.2 Instantiated methods

For methods of generic types, the instantiated method obtained by supplying type arguments and the method registered with a marker at declaration (types.Func) must be treated as the same entity. Simple object comparison alone broke this correspondence.

The current implementation, when the callee is types.Func, normalizes it to the original function using Origin() and then matches it against the set of collected markers. This process organizes the relationship between type‑argument instantiation and the original declaration rather than inferring that a different function might be called at runtime.

However, the claim that generic functions are supported should not be taken to mean that signatures using arbitrary type parameters are also permitted. For example, func Double[T ~int](n T) T triggers a diagnostic on the signature because the current value‑type check does not allow TypeParam. This was verified in the auxiliary example for this article.

The regression tests for generic methods use examples where the type has type parameters but its actual field is int. The presence of type parameters in a type name is not the same as having type parameters remain after recursively examining the signature’s types. Summarizing this as “generic support” in a single phrase obscures the scope of its applicability.

9.3 Distinguishing parentheses from indexing

Calls with parentheses were also important for resolving the call target. We do not want Double(n) and (Double)(n), nor len("abc") and (len)("abc"), to produce different results in this check. Currently we resolve call targets based on type information, and we use ast.Unparen for assignments and increments/decrements.

On the other hand, it is not always safe to strip away every index expression. Constant[int]()’s [int] is a type argument, whereas f[0](2)’s [0] retrieves an element from an array that holds function values. If we carelessly strip the latter and allow functions stored in an array, the tool might mistakenly treat the call target as already resolved, even for dynamically determined calls.

The regression tests also include cases that reject examples where a designated function is placed in an array and the array element is called. We have also confirmed that undesignated functions with parentheses and prohibited built‑ins are not permitted after normalization. When making changes to reduce false positives, we must also verify that they do not increase missed detections.

10. Verification Methods and Observations

10.1 Testing the Diagnosis Itself

Mikoto’s tests use analysistest. In the Go source files used for testing, we place want comments to specify where each diagnostic should appear. This is not merely a test to confirm that the analysis does not crash.

In addition to providing source that should trigger diagnostics, we also place source that should be accepted in the same test fixture. Even if the tool can detect incorrect code, it would be impractical as a real‑world checker if it rejects all legitimate code. The setup is designed to verify both missed detections and false positives.

For example, the generic‑range fixture includes, besides rejection cases for maps, channels, and iterators, an acceptance case where only slices remain after intersecting arrays, integers, and constraints. The pointer fixture also contains a rejection case for implicit reads and an acceptance case for indexing that uses a constant length. Including legitimate syntax that is close to the prohibited constructs makes it easier to verify the decision boundaries.

10.2 Comparing Before and After Fixes

In the verification record of PR #6 (PR #6), we confirmed that the added regression tests failed before the fix and passed after it. We also analyzed the reproducible code for each issue with the CLI, confirming that diagnostics are emitted for map traversals and external‑memory accesses, while no diagnostics appear for legitimate generic calls or parenthesized operations.

The purpose of this comparison is to verify that the newly added tests actually exercise the bug that was fixed this time. Seeing tests pass only after the fix does not tell us whether they also passed before the fix. In particular, when fixing missed detections, it is easy to assume we were checking the positions where a diagnostic was required.

In preparing this article, we fetched the publicly available current revision into a temporary directory and performed the following verification using Go 1.25.0 on macOS ARM64. The tests recorded in the PR for the pre‑ and post‑fix stages, and the tests we ran locally on the current version, were not mixed together as a single experiment.

The acceptance example also includes func Divide(n int) int { return 10 / n }, which could potentially cause division by zero. This function passes without any diagnostic. This is less a success case demonstrating the tool’s effectiveness and more an example that actually confirms a property the analysis does not handle. Because it passes the purity rules, we must not infer that it will terminate normally for all possible inputs.

10.3 How to Evaluate This Fix

When we organize the five issues that were closed this time by the nature of the problem, they fall into the following categories.

What this shows is that we have revised the initial decision logic for specific combinations of syntax and types, and confirmed those boundaries with regression tests. We have not measured the tool’s coverage, detection rate, analysis time, or the reduction in developer review time for large Go codebases. The number of issues cannot be taken as a direct measure of the tool’s overall accuracy.

11. Application Example: Externalizing I/O While Keeping the Computation

11.1 Encapsulating Price Calculation in a Value

As a concrete usage, consider a function that computes an amount from a unit price and a quantity. If the function also fetches the unit price from a network or stores the result, verification would require an external environment. By contrast, if the function is split into a part that takes values as input and returns values as output, only that portion needs to be examined.

type Order struct {
    UnitPrice int64
    Quantity  int64
}

type Result struct {
    Amount int64
    Valid  bool
}

//mikoto:pure
func Quote(order Order) Result {
    if order.UnitPrice < 0 || order.UnitPrice > 1_000_000_000 {
        return Result{}
    }
    if order.Quantity < 0 || order.Quantity > 1_000_000 {
        return Result{}
    }
    return Result{
        Amount: order.UnitPrice * order.Quantity,
        Valid:  true,
    }
}

We have confirmed that this example is accepted by the current CLI. The imposed upper bound is merely to clarify the input domain for the example, ensuring that the product stays within the int64 range. Mikoto does not judge the practical reasonableness of the unit price and quantity, the tax or rounding rules, or the meaning of a zero amount.

The return value is not error because, under the current signature constraints, an interface‑type error is not allowed. This does not mean that the usual Go idiom of returning an error is bad. As a small example that conforms to mikoto’s current rules, we are using a result that can be expressed solely with values. Whether this constraint is appropriate for actual API design must be judged together with the requirements of the users.

11.2 Passing External Information as Arguments

If a computation depends on the current time, instead of reading the timer inside the function, you can pass the required time as a value argument. If it depends on configuration, rather than reading package‑level variables directly, you can bundle the necessary settings into a value and pass them. This does not eliminate external dependencies, but the information that influences the result becomes explicit in the function’s inputs.

For example, if the only data needed for a deadline check is an integer timestamp, the caller can obtain the current time and pass that value to the checking function. When using the full date‑time type directly, you must separately verify that its internal representation and method calls satisfy the current rules. We are not claiming that “passing a time as an argument makes everything work.”

flowchart LR
    I["Retrieve from clock, settings, or database"] --> V["Convert required information into values"]
    V --> C["Specified calculation function"]
    C --> R["Return the result as a value"]
    R --> O["Save, notify, respond"]

This structure is not generated automatically by mikoto. Humans split the responsibilities and attach markers to the computational part. The tool then diagnoses, within the scope of the implemented rules, any later introduction of references to or updates of external state.

The surrounding code still handles concerns such as timeouts, retries, transactions, and duplicate executions. Even if the computational portion meets its constraints, the correctness of the entire system cannot be determined solely by that. However, when you can inspect the acquisition of inputs, the computation, and the propagation of results separately, it becomes easier to pinpoint which assumptions to doubt when a failure occurs.

11.3 The Cost of Adding More Boundaries

Introducing such separation also incurs costs. More types are needed to collect values, conversion steps become necessary, and the call hierarchy deepens. Enforcing this pattern on every function would force even operations whose primary responsibility is handling external state to take unnecessary detours.

The most natural candidates for this approach are calculations such as fees or scores, classification of conditions, conversion of protocol values, and small state‑transition decisions—any part where inputs and outputs can be expressed as values. However, even string processing that relies on standard‑library calls is restricted by the current rules, and handling reference‑type data structures in state transitions may violate the signature constraints.

Therefore, instead of lumping everything together as “usable in this domain,” it’s better to examine each concrete function to see what arguments it takes, what it returns, and what it calls. Starting with small targets and evaluating the required constraints separately from operations that are rejected merely for implementation reasons is the practical approach.

12. Limitations: What the Lack of Diagnosis Does Not Guarantee

12.1 Termination and Exceptions

The earlier example of division by zero shows that when the argument is zero, the function does not return a valid value. Recursive functions and infinite loops are also not analyzed for termination by the current mikoto. Calling a pre‑specified function recursively may be permitted solely based on the marker of the callee.

In other words, even if you get closer to the purpose of computing a result from the input, the fact that the computation will inevitably finish is a separate issue. A function’s contract also concerns which inputs are considered valid, which failures are allowed, and how much time and resource usage is permitted. These cannot all be compressed into a single short marker such as pure.

Even if built‑in functions that panic are prohibited, runtime failures in arithmetic operations or index accesses are not eliminated entirely. Even when only operations permitted by the tool are used, the assumptions about the inputs still need to be verified through tests or other checks.

12.2 Floating‑Point and the Environment

Floating‑point numbers are allowed as a primitive type, but the precision and stability of numerical computations are not examined. Whether NaNs, infinities, rounding errors, or loss of significance are acceptable in a given context depends on the requirements of the calculation. Even for the same expression, unless we define what counts as an equivalent result, the very assessment of determinism becomes ambiguous.

Moreover, there are conditions that depend on the execution environment, such as the widths of int and uintptr. Even for functions that compute solely from their inputs, mikoto does not guarantee that the same numeric results will be produced across different environments. The relevant Go language specifications, types, and runtime conditions must be aligned separately.

As noted in the earlier article on FP6 and quantization, we treated finite numeric representations and the properties we wish to preserve as separate concerns. Here as well, not referring to external state and ensuring that the computation’s result meets the required precision are distinct properties. Tests that address numerical errors cannot be replaced by purity diagnostics. (source)

12.3 Verification Across Package Boundaries

The set of designated functions is built from the declarations of the same package that the analysis receives. We have not implemented a mechanism that incorporates analysis results showing that functions from other packages carry the same marker, nor one that permits such calls.

go/analysis provides a way to propagate analysis information across packages, but the existence of such a feature in the framework is distinct from mikoto actually using it. The current Analyzer does not define purity facts. While it could be listed as a future candidate, it is not included in the present guarantees.

If external functions are permitted, you must decide how to maintain the guarantees when library versions change, on what basis to trust code that is outside the analysis scope, and how to handle dynamically resolved call targets. Simply expanding the convenient allowlist can obscure the rationale behind those decisions.

12.4 Inspecting Unreachable Code as Well

The current core analysis merely traverses the AST and does not rigorously prove that execution reaches each branch. Even if a prohibited call appears in an unreachable branch, the diagnostic can flag it once the syntax is detected. The absence of side effects at runtime is not the same as satisfying the syntactic rules in the source code.

This assessment depends on the intended purpose of the constraints. If you want to ensure that no external operations are introduced even when conditions change in the future, it is worthwhile to diagnose even unreachable locations. Conversely, if you aim to make a precise judgment only about runtime behavior, doing so can become inconvenient due to false positives. Mikoto’s current design does not strive for full inference of the latter case.

13. Considerations: Conservative Rules and Analysis Precision

13.1 A Wide Rejection Scope Is Not the Same as Soundness

In static analysis, both rejecting code that is semantically safe and overlooking truly dangerous code are problems. Mikoto also has broad constraints—such as disallowing assignments to local arrays—while its initial implementation missed implicit indirections.

Simply labeling a rule as “conservative” does not eliminate all missed detections. To claim soundness, you must define the target language and observation model, and demonstrate that each permitted operation—and any combination of them—preserves the desired properties. Having many prohibited items alone does not constitute such a proof.

What this PR demonstrates is that we fixed specific missed detections and tested that similar legitimate cases are not erroneously rejected. We have not formally proven soundness for every possible syntax. The fact that the implementation is small enough to be fully understood is distinct from it being able to handle every possible execution path in the language.

13.2 What Is Required to Introduce More Precise Analysis

To allow modifications to local arrays, you would need to track that the array is not shared with external code and that no references to it escape. To permit calls to function values, you would need to determine which functions those values might refer to. If different assignments occur in different branches, you also need mechanisms to merge that information.

As you relax these constraints, the scope of analysis expands from simple AST shape checks to data‑flow, aliasing, reachability, and call‑graph analyses. While alternative representations such as SSA could be used, the current mikoto does not implement such analyses. Maintaining simple rules in a compact form versus accepting more legitimate code involves both implementation and explanatory costs.

When analysis becomes more precise, users may gain greater freedom in how they write code. However, this also increases the prerequisites for understanding why a diagnostic was issued—or not issued. We need to consider how far it is worthwhile to introduce complexity as a tool that can be applied explicitly to small functions.

13.3 Normalizing Syntax and Verifying Semantics

The current changes involved several distinct issues: normalizing parentheses, handling identity of generic declarations, unions and intersections of constraints, and implicit indirection. Each requires different kinds of information, and they cannot all be solved merely by “examining the AST more closely.”

Parentheses can be removed without altering the meaning of the operations inspected. Calls with type arguments resolve the original function using type information. The prohibition of map accesses proceeds as far as the constraints on the type parameters. Accesses through pointers rely on type and selection information rather than merely the presence or absence of *.

The implementation guideline derived from this is to first define the semantics you wish to prohibit, then map those semantics to the corresponding syntax and type information. If any mapping is missing, a detection will be missed. Conversely, if you overly merge syntactically similar constructs, you will generate false positives. By encoding these mappings as part of regression tests, you can verify them each time the code changes.

14. Deployment and Future Evaluation

14.1 Introducing It Starting with Small Targets

The current usage is as follows. The required Go version is 1.24 or later, and the CLI accepts a Go package specification.

go install github.com/ieee0824/mikoto/cmd/mikoto@latest
mikoto -max-lines=80 ./...

If you do not check the length of functions and only inspect functions that have the marker, use the following specification.

mikoto -max-lines=0 ./...

When using it in CI, it is easier to track changes in diagnostics if you fix which revision of the analyzer you employ. Updating the analyzer can cause previously missed code to be flagged, as in this release, or code that was erroneously rejected to pass. The example deployment using latest and the operational practice of repeatedly checking the same conditions serve different purposes.

Initially, attach markers to small computational functions and verify whether the diagnostics clarify the boundaries of their intended role. Specifying markers for a large number of functions at once and mechanically rewriting any syntax that fails defeats the purpose, because it becomes unclear what the checks are meant to protect. The limit on line count should also be used as a cue to reassess how responsibilities are partitioned overall.

14.2 Division of Labor with Testing

Mikoto performs static checks on the constraints of the specified syntax, types, and dependencies. Whether the computed result matches the expected value is verified through unit tests. If there are relationships that must hold over a broad set of inputs, property‑based testing can be employed. Results that involve external fetching or storage are confirmed via integration tests or end‑to‑end tests.

For example, in a price‑calculation scenario, even if mikoto confirms that the code does not touch external state, the amount will still be wrong if the multiplication of unit price and quantity is performed incorrectly. Whether to reject invalid inputs, where to perform rounding, and which point in time the tax rate should represent must be defined by the specification and tested. Static boundary checks and verification of the desired behavior complement each other.

The same applies when AI generates code. By using markers and the analyzer, you can explicitly convey part of the conditions that must be upheld, and mechanically detect when the generated code deviates from those conditions. However, deciding whether to remove a marker, relax a condition, or even retain the feature itself still requires design judgment.

14.3 What to Measure

Going forward, when evaluating the tool’s usefulness, we should record not only the number of diagnostics but also what changes each diagnostic induces. Potential metrics include the number of external‑state dependencies discovered, the number of violations of intended responsibilities that were corrected, the number of safe local operations that were erroneously rejected, and the functions for which enforcement was dropped along with the reasons.

We also need to measure analysis time separately. The fact that the current test succeeded does not constitute a performance evaluation showing that the system is sufficiently fast even on a large codebase. It is easier to make a judgment by separating package loading and type checking from Mikoto’s own scanning, and measuring under consistent conditions regarding code size, Go version, and caching.

However, these evaluations and improvements have not yet been implemented as concrete results at this time. Cross‑package information sharing, precise permission control for local changes, and dynamic tracking of call targets will also become candidates for consideration once their necessity is confirmed. Rather than expanding the list of features, we first want to verify which design problems the current rules can address.

15. Conclusion

In Mikoto, we impose explicit constraints on Go functions and statically inspect each function’s physical line count as well as the boundaries, operations, and dependencies of the value types specified for those functions. Rather than automatically discovering pure functions, we specify the parts we want to treat as pure computations and diagnose implementations that deviate from that intent.

Through revising the initial implementation, we found that classifying syntax alone is insufficient to distinguish prohibited operations from permitted ones. Maps over type parameters, index references to array pointers, and the targets of a range assignment can be missed if one only follows the surface syntax. Conversely, parentheses and type arguments can alter the syntax tree or declaration correspondence even when their meaning does not change. It was necessary to combine type information with normalization and test the boundaries on both sides.

What we confirmed this time are the specific fixes and the results of the regression tests. We have not collectively proven referential transparency, termination, or the correctness of numerical computations. Still, it is valuable that the boundaries we must enforce are not left merely as comments but can be repeatedly verified through implemented rules.

What humans must decide is which functions should have those boundaries applied, how to handle changes that trigger diagnostics, and whether the computed results are truly needed. Mikoto is being built as a tool that lets us check, in the same form even as code grows, the conditions used for those judgments.