define TCS language and prove stage0 execution slice
This commit is contained in:
parent
8cfdba210f
commit
3959ae4270
31 changed files with 2449 additions and 5 deletions
102
language/compiler/TCS-COMPILER-STAGE1.tcs
Normal file
102
language/compiler/TCS-COMPILER-STAGE1.tcs
Normal file
|
|
@ -0,0 +1,102 @@
|
|||
TCS 0.1;
|
||||
|
||||
COMPILER TCS-COMPILER-STAGE1-0001 {
|
||||
header {
|
||||
schema = "tcs.compiler/v1";
|
||||
name_zh = "TCS 第一代自举编译器";
|
||||
version = "0.1.0";
|
||||
profile = "HLDP-NP/1";
|
||||
lifecycle = "SOURCE_DEFINED_NOT_YET_EXECUTABLE";
|
||||
bootstrap_seed = "TCS-STAGE0-IGNITION-0001";
|
||||
output = "GIR/1";
|
||||
}
|
||||
source_language {
|
||||
prologue = ["TCS", "VERSION", "SEMICOLON"];
|
||||
declaration_kinds = ["PROGRAM", "MODULE", "PROTOCOL", "COMPILER", "EVENT", "RECEIPT"];
|
||||
punctuation = ["LBRACE", "RBRACE", "LBRACKET", "RBRACKET", "LESS", "GREATER", "COLON", "EQUAL", "COMMA", "SEMICOLON", "DOT"];
|
||||
scalar_tokens = ["IDENTIFIER", "TEXT", "INT", "BOOL", "NULL"];
|
||||
comments = ["LINE_COMMENT", "BLOCK_COMMENT"];
|
||||
encoding = "UTF8_LF_NO_BOM";
|
||||
}
|
||||
lexer_rules {
|
||||
L001 { when = "BOM_AT_START"; emit_error = "TCS-E0001"; }
|
||||
L002 { when = "WHITESPACE_OR_COMMENT"; action = "SKIP_WITH_SOURCE_POSITION"; }
|
||||
L003 { when = "DOUBLE_QUOTE"; action = "READ_JSON_ESCAPED_TEXT"; on_unterminated = "TCS-E0002"; }
|
||||
L004 { when = "MINUS_OR_ASCII_DIGIT"; action = "READ_SIGNED_DECIMAL_INT"; on_overflow = "TCS-E2001"; }
|
||||
L005 { when = "UNICODE_LETTER_OR_UNDERSCORE"; action = "READ_IDENTIFIER_OR_KEYWORD"; }
|
||||
L006 { when = "REGISTERED_PUNCTUATION"; action = "EMIT_PUNCTUATION_TOKEN"; }
|
||||
L007 { when = "OTHER_CHARACTER"; emit_error = "TCS-E1001"; }
|
||||
}
|
||||
parser_rules {
|
||||
P001 { nonterminal = "document"; sequence = ["prologue", "declaration", "EOF"]; }
|
||||
P002 { nonterminal = "prologue"; sequence = ["TCS", "version", "SEMICOLON"]; }
|
||||
P003 { nonterminal = "declaration"; sequence = ["declaration_kind", "identifier", "block"]; }
|
||||
P004 { nonterminal = "block"; sequence = ["LBRACE", "member_zero_or_more", "RBRACE"]; }
|
||||
P005 { nonterminal = "member"; alternatives = ["identifier_assignment", "identifier_typed_assignment", "identifier_block"]; }
|
||||
P006 { nonterminal = "value"; alternatives = ["TEXT", "INT", "BOOL", "NULL", "IDENTIFIER", "array", "inline_object"]; }
|
||||
P007 { when = "DUPLICATE_MEMBER_IN_SAME_BLOCK"; emit_error = "TCS-E1002"; }
|
||||
P008 { when = "TOKEN_AFTER_TOP_LEVEL_DECLARATION"; emit_error = "TCS-E1001"; }
|
||||
}
|
||||
semantic_types {
|
||||
scalars = ["Text", "Bool", "Int", "UInt", "DecimalText", "Bytes", "DurationMs", "Timestamp", "Sha256", "NumberId", "Path", "Uri", "ErrorCode"];
|
||||
containers = ["List", "Set", "Map", "Option", "Ref", "Evidence", "Record"];
|
||||
domains = ["Subject", "ExactTarget", "AuthorityProof", "ActionGraph", "ReceiptPlan", "RelationEvent"];
|
||||
implicit_conversion = "FORBIDDEN";
|
||||
floating_point = "FORBIDDEN_V0_1";
|
||||
}
|
||||
program_validation {
|
||||
V001 { rule = "EXACT_REQUIRED_SECTIONS"; standard = "TCS-FIELD-STANDARD-0001"; error_missing = "TCS-E1004"; error_unknown = "TCS-E1003"; }
|
||||
V002 { rule = "CLOSED_FIELDS_PER_SECTION"; error = "TCS-E1003"; }
|
||||
V003 { rule = "ALL_INPUT_OUTPUT_AND_ACTION_REFS_RESOLVE"; error = "TCS-E2002"; }
|
||||
V004 { rule = "ALL_OPERATIONS_REGISTERED_AT_LOCKED_VERSION"; error = "TCS-E2101"; }
|
||||
V005 { rule = "SOURCE_ID_URI_HASH_AND_ROLE_RESOLVE"; errors = ["TCS-E3001", "TCS-E3002"]; }
|
||||
V006 { rule = "SUBJECT_TARGET_AND_AUTHORITY_EXACT"; errors = ["TCS-E4001", "TCS-E4002", "TCS-E4003"]; }
|
||||
V007 { rule = "ACTION_GRAPH_REACHABLE_AND_TERMINATING"; error = "TCS-E2001"; }
|
||||
V008 { rule = "FAILURE_STOP_CLEANUP_ROLLBACK_AND_RECEIPT_PRESENT"; error = "TCS-E1004"; }
|
||||
V009 { rule = "NO_FORBIDDEN_RUNTIME_PLACEHOLDER"; error = "TCS-E3002"; }
|
||||
V010 { rule = "RELATION_AND_EMOTION_DO_NOT_GRANT_AUTHORITY"; error = "TCS-E4001"; }
|
||||
}
|
||||
lowering_to_gir {
|
||||
G001 { from = "header"; to = "identity"; transform = "COPY_ID_VERSION_PROFILE_AND_LOCK_PROTOCOLS"; }
|
||||
G002 { from = "source"; to = "compiled_from"; transform = "VERIFY_AND_BIND_SOURCE_SHA256"; }
|
||||
G003 { from = "subject"; to = "subject"; transform = "RESOLVE_VERIFIED_SUBJECT"; }
|
||||
G004 { from = "target"; to = "exact_target"; transform = "RESOLVE_PATH_STATE_AND_FINGERPRINT"; }
|
||||
G005 { from = "actions"; to = "deterministic_action_graph"; transform = "SORT_ACTION_IDS_AND_RESOLVE_ALL_EDGES"; }
|
||||
G006 { from = "authority"; to = "authority_proof"; transform = "BIND_PROOF_WITHOUT_EXPANDING_SCOPE"; }
|
||||
G007 { from = "resources"; to = "resource_plan"; transform = "NORMALIZE_INTEGER_LIMITS"; }
|
||||
G008 { from = "stop"; to = "timeout_and_stop"; transform = "COPY_EXPLICIT_STOP_SEMANTICS"; }
|
||||
G009 { from = "cleanup"; to = "cleanup_plan"; transform = "COPY_EXACT_BOUNDARY"; }
|
||||
G010 { from = "rollback"; to = "rollback_plan"; transform = "COPY_ACTIONS_AND_VERIFICATION"; }
|
||||
G011 { from = "receipt"; to = "receipt_plan"; transform = "BIND_MACHINE_AND_HUMAN_OUTPUTS"; }
|
||||
G012 { from = "all"; to = "unresolved_natural_language"; transform = "MUST_BE_FALSE"; }
|
||||
}
|
||||
canonicalization {
|
||||
object_keys = "UTF8_BYTE_ORDER";
|
||||
list_order = "PRESERVE_SOURCE_SEMANTICS";
|
||||
integers = "MINIMAL_DECIMAL";
|
||||
strings = "JSON_ESCAPE_NO_OPTIONAL_ESCAPE";
|
||||
line_end = "LF";
|
||||
final_newline = true;
|
||||
semantic_digest = "SHA256";
|
||||
comments_in_semantic_digest = false;
|
||||
}
|
||||
output_contract {
|
||||
schema = "guanghu.gir/v1";
|
||||
unresolved_natural_language = false;
|
||||
unresolved_authority = false;
|
||||
drifting_dependency = false;
|
||||
target_must_be_exact = true;
|
||||
compiler_provenance_required = true;
|
||||
}
|
||||
self_host {
|
||||
stage0_compiles_stage1_to = "compiler-A.gir";
|
||||
compiler_A_compiles_stage1_to = "compiler-B.gir";
|
||||
fixed_point = "SEMANTIC_SHA256_A_EQUALS_B";
|
||||
stage0_disabled_test = "REQUIRED";
|
||||
standard_library_test = "REQUIRED";
|
||||
negative_corpus_test = "REQUIRED";
|
||||
minimum_runnable_module_test = "REQUIRED";
|
||||
current_state = "NOT_PROVEN";
|
||||
}
|
||||
}
|
||||
|
||||
Loading…
Reference in a new issue