Skip to content

Commit 3163e14

Browse files
hyperpolymathClaude
hyperpolymath
and
Claude
authored
Resurrect the framework Idris2 core: compile all 13 modules (Framework + Filesystem + A2ML) (#16)
* fix(framework): compile Framework core + Filesystem subsystem Make the Framework core and Filesystem modules type-check (8/13 of the package; the A2ML chain is a separate WIP sketch): - Progressive: define rank/atLeast, add Eq, complete the Ord instance (was '-- ... [Remaining cases]'). - Proof: fix //! and // comments; define HashValue (+ DecEq) and the FullyAttested witness + fullyAttest smart constructor. - Error: define showPriority/showQuery/showZone and the hashError smart constructor. - Interface: define the Snapshot type; implement the verifyOrRepair pipeline (was a stub referencing an undefined 'proof'); bind {sub}. - Filesystem.Merkle: rename the 'proof' parameter (now a reserved word in Idris2 0.8) and import Data.Nat for div on Nat. - Filesystem.Verify: replace the placeholder 'MkHashesMatch _ cv cv Refl' with a genuine decEq-derived equality proof over HashValue. * feat(a2ml): implement the A2ML lexer/parser/validator/serializer Replace the A2ML design sketch (undefined core types, stubbed bodies) with a complete, total, working implementation of its section-based design: - Types: define SourceLoc, Token (+ Eq TokenKind), the punctuation/number/bool token kinds, and the four section types (ManifestSection, RefsSection with Ref, AttestationSection, PolicySection with PolicyMode). - Lexer: a total, fuel-bounded scanner with structural collectors; handles @Keywords, strings, numbers, booleans, punctuation, and algo:digest hashes. - Parser: a total recursive-descent parser (fuel-bounded section dispatch, structural @refs loop) producing a Manifest. - Validator: per-section semantic checks (hash length/format, required fields). - Serializer: renders a Manifest back to canonical surface syntax. Verified with Idris2 0.8.0: package builds 13/13; lex/parse/serialize/validate are total; a sample manifest parses, validates, and round-trips (parse (lex (serialize m)) preserves the manifest). * fix(ci): point CodeQL at 'actions', not absent javascript-typescript The repo has zero JS/TS sources, so CodeQL's javascript-typescript extractor failed with a configuration error ('no code found') on every run. Analyse the GitHub Actions workflows instead (build-mode none), matching the ochrance repo's working CodeQL config. SPDX header, permissions, and SHA-pins are unchanged, so the workflow-security-linter gate stays green. --------- Co-authored-by: Claude <paraordinate@yahoo.co.uk>
1 parent 8970a45 commit 3163e14

12 files changed

Lines changed: 651 additions & 133 deletions

File tree

‎.github/workflows/codeql.yml‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,10 @@ jobs:
3030
fail-fast: false
3131
matrix:
3232
include:
33-
- language: javascript-typescript
33+
# This repo is Idris2/Rust/C with no JS/TS sources, so CodeQL's
34+
# javascript-typescript extractor errored ("no code found"). Analyse
35+
# the GitHub Actions workflows instead (matches the ochrance repo).
36+
- language: actions
3437
build-mode: none
3538

3639
steps:

‎ochrance-core/Ochrance/A2ML/Lexer.idr‎

Lines changed: 100 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@
33

44
||| Ochrance.A2ML.Lexer — High-Assurance Tokenization.
55
|||
6-
||| This module transforms raw A2ML source text into a stream of semantic
6+
||| This module transforms raw A2ML source text into a stream of semantic
77
||| tokens. It is the first stage of the manifest parsing pipeline.
88
|||
9-
||| TOTALITY GUARANTEE: The lexer uses structural recursion on the input
10-
||| character list. Since every recursive call consumes at least one
11-
||| character (or terminates), the process is guaranteed to halt.
9+
||| TOTALITY GUARANTEE: the scanner is fuel-bounded (fuel initialised to the
10+
||| input length); every iteration either consumes input and decrements fuel,
11+
||| or terminates. The character collectors recurse structurally on the input.
1212

1313
module Ochrance.A2ML.Lexer
1414

@@ -19,48 +19,122 @@ import Data.List
1919
%default total
2020

2121
--------------------------------------------------------------------------------
22-
-- Lexer State
22+
-- Errors and State
2323
--------------------------------------------------------------------------------
2424

25-
||| STATE: Tracks the remaining characters and the current source position.
25+
||| LEX ERROR: a character that cannot begin any token, or an unterminated string.
26+
public export
27+
data LexError : Type where
28+
UnexpectedChar : (char : Char) -> (loc : SourceLoc) -> LexError
29+
UnterminatedString : (loc : SourceLoc) -> LexError
30+
31+
||| STATE: the remaining characters and the current source position.
2632
record LexState where
2733
constructor MkLexState
2834
input : List Char
2935
line : Nat
3036
column : Nat
3137

38+
currentLoc : LexState -> SourceLoc
39+
currentLoc st = MkSourceLoc st.line st.column
40+
41+
initState : String -> LexState
42+
initState s = MkLexState (unpack s) 1 1
43+
3244
--------------------------------------------------------------------------------
33-
-- Tokenization Logic
45+
-- Character classes and collectors
3446
--------------------------------------------------------------------------------
3547

36-
||| KEYWORD RECOGNITION: Maps identifiers starting with '@' to their
37-
||| corresponding A2ML section headers.
48+
isIdentStartChar : Char -> Bool
49+
isIdentStartChar c = isAlpha c || c == '_'
50+
51+
isIdentChar : Char -> Bool
52+
isIdentChar c = isAlphaNum c || c == '_' || c == '-' || c == '.'
53+
54+
||| Collect the longest prefix satisfying `p` (structural recursion).
55+
collectWhile : (Char -> Bool) -> List Char -> (List Char, List Char)
56+
collectWhile p [] = ([], [])
57+
collectWhile p (c :: cs) =
58+
if p c then let (a, b) = collectWhile p cs in (c :: a, b)
59+
else ([], c :: cs)
60+
61+
||| Collect a string body up to (and consuming) the closing quote.
62+
collectString : List Char -> Maybe (List Char, List Char)
63+
collectString [] = Nothing
64+
collectString ('"' :: cs) = Just ([], cs)
65+
collectString (c :: cs) = map (\(a, b) => (c :: a, b)) (collectString cs)
66+
67+
||| KEYWORD RECOGNITION: maps an `@`-prefixed word to its section header token.
3868
recogniseKeyword : String -> Maybe TokenKind
3969
recogniseKeyword "manifest" = Just TK_MANIFEST
4070
recogniseKeyword "refs" = Just TK_REFS
4171
recogniseKeyword "attestation" = Just TK_ATTESTATION
4272
recogniseKeyword "policy" = Just TK_POLICY
4373
recogniseKeyword _ = Nothing
4474

45-
||| SCANNER LOOP: Dispatches based on the first character of the remaining input.
46-
|||
47-
||| PATTERNS:
48-
||| - `@` -> Section Header.
49-
||| - `"` -> String Literal.
50-
||| - `#` -> Hash Literal (Hex).
51-
||| - `{`, `}`, `:`, `=` -> Punctuation.
75+
||| Bare words `true`/`false` lex as booleans; anything else is an identifier.
76+
identOrBool : String -> TokenKind
77+
identOrBool "true" = TK_BOOL True
78+
identOrBool "false" = TK_BOOL False
79+
identOrBool s = TK_IDENT s
80+
81+
digitsToNat : List Char -> Nat
82+
digitsToNat ds = integerToNat (cast (pack ds))
83+
84+
--------------------------------------------------------------------------------
85+
-- Scanner
86+
--------------------------------------------------------------------------------
87+
88+
||| SCANNER LOOP: dispatches on the first character of the remaining input.
5289
lexLoop : (fuel : Nat) -> LexState -> List Token -> Either LexError (List Token)
5390
lexLoop Z st acc = Right (reverse (MkToken TK_EOF (currentLoc st) :: acc))
5491
lexLoop (S k) st acc =
55-
let st' = skipWhitespace k st in
56-
case st'.input of
57-
[] => Right (reverse (MkToken TK_EOF (currentLoc st') :: acc))
58-
('@' :: _) =>
59-
-- 1. EXTRACT keyword.
60-
-- 2. RECOGNIZE and PUSH token.
61-
lexLoop k st2 (MkToken tk (currentLoc st') :: acc)
62-
-- ... [Other pattern match branches]
63-
_ => Left (UnexpectedChar '?' (currentLoc st'))
92+
case st.input of
93+
[] => Right (reverse (MkToken TK_EOF (currentLoc st) :: acc))
94+
(c :: cs) =>
95+
let loc = currentLoc st in
96+
if c == '\n'
97+
then lexLoop k (MkLexState cs (S st.line) 1) acc
98+
else if c == ' ' || c == '\t' || c == '\r'
99+
then lexLoop k (MkLexState cs st.line (S st.column)) acc
100+
else if c == '{'
101+
then lexLoop k (MkLexState cs st.line (S st.column)) (MkToken TK_LBRACE loc :: acc)
102+
else if c == '}'
103+
then lexLoop k (MkLexState cs st.line (S st.column)) (MkToken TK_RBRACE loc :: acc)
104+
else if c == ':'
105+
then lexLoop k (MkLexState cs st.line (S st.column)) (MkToken TK_COLON loc :: acc)
106+
else if c == '='
107+
then lexLoop k (MkLexState cs st.line (S st.column)) (MkToken TK_EQUALS loc :: acc)
108+
else if c == '"'
109+
then case collectString cs of
110+
Nothing => Left (UnterminatedString loc)
111+
Just (strChars, rest) =>
112+
let col' = st.column + length strChars + 2 in
113+
lexLoop k (MkLexState rest st.line col') (MkToken (TK_STRING (pack strChars)) loc :: acc)
114+
else if c == '@'
115+
then let (word, rest) = collectWhile isIdentChar cs in
116+
case recogniseKeyword (pack word) of
117+
Just tk => lexLoop k (MkLexState rest st.line (st.column + 1 + length word)) (MkToken tk loc :: acc)
118+
Nothing => Left (UnexpectedChar '@' loc)
119+
else if isDigit c
120+
then let (digits, rest) = collectWhile isDigit (c :: cs) in
121+
lexLoop k (MkLexState rest st.line (st.column + length digits))
122+
(MkToken (TK_NUMBER (digitsToNat digits)) loc :: acc)
123+
else if isIdentStartChar c
124+
then let (word, rest) = collectWhile isIdentChar (c :: cs)
125+
wordStr = pack word
126+
in case rest of
127+
(':' :: afterColon) =>
128+
let (hashChars, rest') = collectWhile isHexDigit afterColon in
129+
if length hashChars > 0
130+
then let raw = wordStr ++ ":" ++ pack hashChars
131+
col' = st.column + length word + 1 + length hashChars
132+
in lexLoop k (MkLexState rest' st.line col') (MkToken (TK_HASH raw) loc :: acc)
133+
else lexLoop k (MkLexState rest st.line (st.column + length word))
134+
(MkToken (identOrBool wordStr) loc :: acc)
135+
_ => lexLoop k (MkLexState rest st.line (st.column + length word))
136+
(MkToken (identOrBool wordStr) loc :: acc)
137+
else Left (UnexpectedChar c loc)
64138

65139
--------------------------------------------------------------------------------
66140
-- Public API
@@ -69,7 +143,4 @@ lexLoop (S k) st acc =
69143
||| ENTRY POINT: Ingests an A2ML string and returns a list of tokens.
70144
public export
71145
lex : String -> Either LexError (List Token)
72-
lex input =
73-
let fuel = length input + 1
74-
st = initState input
75-
in lexLoop fuel st []
146+
lex input = lexLoop (length (unpack input) + 1) (initState input) []

0 commit comments

Comments
 (0)