hvm-weakpoints.md

Based on my analysis of the HVM3 codebase you provided, here are the potential weak points and bugs that could cause issues:

1. Memory Management Issues

The code extensively uses unsafeInterleaveIO in functions like collapseDupsAtLazy and extractCoreAtLazy. This creates thunks with non-deterministic evaluation order, which can lead to:

Memory leaks if thunks retain large data structures
Unpredictable resource usage patterns
Potential race conditions in parallel contexts

2. Collapse Implementation Weaknesses

In HVML.Collapse:

bind :: Collapse a -> (a -> Collapse b) -> Collapse b
bind k f = fork k IM.empty where
  fork CEra         paths = CEra
  fork (CVal v)     paths = pass (f v) (IM.map (\x -> x E) paths)
  fork (CSup k x y) paths =
    let lft = fork x $ IM.alter (\x -> Just (maybe (putO id) putO x)) (fromIntegral k) paths in
    let rgt = fork y $ IM.alter (\x -> Just (maybe (putI id) putI x)) (fromIntegral k) paths in
    CSup k lft rgt

This implementation has a potential bug in how it tracks paths through superpositions. The paths mapping could overflow or behave unexpectedly with deeply nested superpositions, especially if labels are reused.

3. Integer Overflow Risk

HVM3 uses Word64 for labels and addresses, but doesn't always check bounds:

genFreshLabel :: ParserM Word64
genFreshLabel = do
  st <- getState
  let lbl = freshLabel st
  putState st { freshLabel = lbl + 1 }
  when (lbl > 0x7FFF) $ do
    error "Label overflow: generated label would be too large"
  return $ lbl + 0x8000

This checks for overflow, but similar checks are missing in other parts of the code.

4. Inefficient Flattening

The current flattening implementation can be inefficient for deeply nested structures:

flatten :: Collapse a -> [a]
flatten = flattenBFS  -- Could use other strategies

The breadth-first search approach can consume excessive memory for complex superpositions, as it needs to store the entire frontier.

5. Handling of DUP Nodes

In collapseDupsAt, the handling of duplicate nodes might be buggy:

DP0 -> do
  let loc = termLoc term
  let lab = termLab term
  dups <- readIORef dupsRef
  if IS.member (fromIntegral loc) dups
  then do
    name <- return $ "$" ++ show (loc + 0) ++ "_0"
    return $ Var name
  else do
    ...

This logic relies on the dupsRef IntSet to track duplicate nodes, but if the memory layout changes, the same location might be reused for different nodes, leading to incorrect sharing.

6. Parser Error Recovery

The parser has limited error recovery capabilities:

handleParseError :: String -> String -> ParseError -> ParserM a
handleParseError path contents err = do
  liftIO $ showParseError path contents err
  fail $ "Error importing file " ++ show path ++ ": parse failed"

When a parsing error occurs, the entire compilation fails rather than attempting to recover.

7. Potential Race Condition in Reduction

The reduceAt function may have race conditions in parallel contexts:

reduceAt debug book host gc = do 
  term <- got host
  let tag = termTag term
  let lab = termLab term
  let loc = termLoc term
  
  -- Reading and then modifying without proper synchronization

There's no explicit synchronization between reading a term and modifying it, which could cause issues in parallel reductions.

8. Inefficient Pattern Matching

The pattern matching implementation generates suboptimal code for complex patterns:

compileFastBody book fid term@(Mat val mov css) ctx stop@False itr reuse = do
  -- Complex nested conditionals and switches

This could lead to performance bottlenecks for programs with many pattern matches.

9. Limited Error Reporting

The error reporting is often minimal and not user-friendly:

checkRefAri :: Book -> Core -> Compile ()
checkRefAri book core = do
  case core of
    Ref nam fid arg -> when ((funArity book fid) /= fromIntegral (length arg)) $ do
      error $ "Arity mismatch on term: " ++ showCore core ++ ". Expected " ++ show (funArity book fid) ++ ", got " ++ show (length arg) ++ "."
    _ -> return ()

More comprehensive error messages with source locations would be beneficial.

10. The Superposition Handling Bug (Your Issue)

As you discovered, there's a potential bug in how superpositions are handled and collapsed:

flattenBFS term = go term (SQ [] [] :: SQ (Collapse a)) where
  go (CSup k a b) sq = go CEra (sqPut b $ sqPut a $ sq)
  go (CVal x)     sq = x : go CEra sq
  go CEra         sq = case sqPop sq of
    Just (v,sq) -> go v sq
    Nothing     -> []

This approach generates all combinations of choices rather than preserving the hierarchical structure of superpositions, leading to the 4 universes issue you observed.

These issues point to areas where HVM3 could be improved for better performance, reliability, and usability.

meghuizen/hvm-weakpoints.md