add rest of issues

nlnet-2024-12-324/progress.md

@@ -17,15 +17,15 @@ https://en.wikipedia.org/wiki/Transient_execution_CPU_vulnerability#Timeline
 This is for adding the code for translating Fayalite HDL to Rocq, as well as determining how exactly we'll describe HDL in Rocq. I expect the translation code to be of comparable size to the compiler portion of the simulator (the simulator is broken into three main parts, a compiler to an IR optimized for interpretation, the interpreter itself, and the code for reading/writing simulator I/O and handling time simulation), so somewhere around 5000 LoC.
 
 - € 2000 [Issue #2](https://git.libre-chip.org/libre-chip/grant-tracking/issues/2) Figure out how exactly we should represent HDL in Rocq, writing down a manually-translated version of common HDL components (e.g. how to translate a register, a memory, an add/sub/mul/div, etc.).
-- € 4000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Write the code to do the translation in Fayalite.
+- € 4000 [Issue #3](https://git.libre-chip.org/libre-chip/grant-tracking/issues/3) Write the code to do the translation in Fayalite.
 
 ## € 4000 Adding supporting code for generating FPGA bitstreams from Fayalite
 
 This is for adding the tooling to run all the right programs to generate FPGA bitstreams, as well as adding code to handle connecting I/O ports to the FPGA pins. I expect this to be on the order of 1000-2000 LoC for the FPGA pins code, as well as a few hundred for running all the right programs in sequence.
 
-- € 2000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Write support for board interface descriptions and the code for running the FPGA toolchain (similar to the existing code for running SymbiYosys -- the current formal verification toolchain).
-- € 1000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Add support for the Orange Crab since both Cesar and Jacob have one.
-- € 1000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Add support for the Arty A7 100T since that's what we're using for CI.
+- € 2000 [Issue #4](https://git.libre-chip.org/libre-chip/grant-tracking/issues/4) Write support for board interface descriptions and the code for running the FPGA toolchain (similar to the existing code for running SymbiYosys -- the current formal verification toolchain).
+- € 1000 [Issue #5](https://git.libre-chip.org/libre-chip/grant-tracking/issues/5) Add support for the Orange Crab since both Cesar and Jacob have one.
+- € 1000 [Issue #6](https://git.libre-chip.org/libre-chip/grant-tracking/issues/6) Add support for the Arty A7 100T since that's what we're using for CI.
 
 ## € 10000 Register Renaming, Execution, and Instruction Retire
 
@@ -33,9 +33,9 @@ This covers getting register renaming working, as well as scheduling, executing
 
 A lot of this is the work to come up with a detailed low-level plan for the CPU, so I don't have a good idea of how complex or not this is, though I expect it to be probably 40% of the CPU's complexity.
 
-- € 1500 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Add to the simulator in Fayalite the ability to transfer non-HDL data (e.g. HashMap) through the digital signalling mechanism, this allows using those data types when writing procedural models.
-- € 6000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Create a model of the whole rename/execute/retire control system, using procedural implementations of the most complex HDL modules where appropriate.
-- € 2500 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Translate the procedural model to use actual synthesizeable HDL. includes a proof of correctness of the out-of-order CPU in relation to a sequential CPU (probably most easily done by adding the proof to the retire stage).
+- € 1500 [Issue #7](https://git.libre-chip.org/libre-chip/grant-tracking/issues/7) Add to the simulator in Fayalite the ability to transfer non-HDL data (e.g. HashMap) through the digital signalling mechanism, this allows using those data types when writing procedural models.
+- € 6000 [Issue #8](https://git.libre-chip.org/libre-chip/grant-tracking/issues/8) Create a model of the whole rename/execute/retire control system, using procedural implementations of the most complex HDL modules where appropriate.
+- € 2500 [Issue #9](https://git.libre-chip.org/libre-chip/grant-tracking/issues/9) Translate the procedural model to use actual synthesizeable HDL. includes a proof of correctness of the out-of-order CPU in relation to a sequential CPU (probably most easily done by adding the proof to the retire stage).
 
 ## € 8000 Instruction Fetch/Decode
 
@@ -43,11 +43,11 @@ This covers instruction fetch, decoding, and caching. For the decoder, unless Op
 
 https://git.libre-chip.org/libre-chip/parse_powerisa_pdf
 
-- € 1000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Create the next-instruction logic -- includes some sort of branch prediction or branch target buffer so we can actually keep the rest of the CPU pipeline full. This should support fetching more than one instruction per clock.
-- € 1000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Create the fetch and i-cache logic.
-- € 2000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Create the PowerISA decoder -- it translates to the internal microcode. For now, only needs to support a reasonable subset of 64-bit LE integer instructions in problem mode (aka. user mode), FP and VMX/VSX can be disabled.
-- € 2000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Create a model of the instruction fetch/decode control system, using procedural implementations of the most complex HDL modules where appropriate.
-- € 2000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Translate the procedural model to use actual synthesizeable HDL.
+- € 1000 [Issue #10](https://git.libre-chip.org/libre-chip/grant-tracking/issues/10) Create the next-instruction logic -- includes some sort of branch prediction or branch target buffer so we can actually keep the rest of the CPU pipeline full. This should support fetching more than one instruction per clock.
+- € 1000 [Issue #11](https://git.libre-chip.org/libre-chip/grant-tracking/issues/11) Create the fetch and i-cache logic.
+- € 2000 [Issue #12](https://git.libre-chip.org/libre-chip/grant-tracking/issues/12) Create the PowerISA decoder -- it translates to the internal microcode. For now, only needs to support a reasonable subset of 64-bit LE integer instructions in problem mode (aka. user mode), FP and VMX/VSX can be disabled.
+- € 2000 [Issue #13](https://git.libre-chip.org/libre-chip/grant-tracking/issues/13) Create a model of the instruction fetch/decode control system, using procedural implementations of the most complex HDL modules where appropriate.
+- € 2000 [Issue #14](https://git.libre-chip.org/libre-chip/grant-tracking/issues/14) Translate the procedural model to use actual synthesizeable HDL.
 
 ## € 10000 Load/Store instructions
 
@@ -56,17 +56,16 @@ It should include d-cache, some kind of memory, and at least one IO device.
 
 It should include at least lr/sc, some atomic fetch-op, cached load/store, and IO load/store (IO needs to wait until non-speculative to start executing).
 
-- € 1000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) memory system: main memory and IO devices
-    I'm expecting just a big sram to be good enough for simulation of memory, on the fpga we could probably get away with a relatively small sram and put off a dram interface for later. for the IO device, I'm thinking we'd have a simple fixed-frequency uart.
-- € 1000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) d-cache
-- € 2500 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) memory load execution unit (we'll want to be able to do more than one load at once)
-- € 2500 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) memory store execution unit
-- € 2000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) adding atomics: lr/sc, atomic fetch-add (or other fetch-op)
-- € 1000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) adding order-violation detection logic, so we can make memory look like it has total-store-order (for x86), or even sequential consistency (meaning we can ignore all non-IO fences)
+- € 1000 [Issue #15](https://git.libre-chip.org/libre-chip/grant-tracking/issues/15) memory system: main memory and IO devices -- I'm expecting just a big sram to be good enough for simulation of memory, on the fpga we could probably get away with a relatively small sram and put off a dram interface for later. for the IO device, I'm thinking we'd have a simple fixed-frequency uart.
+- € 1000 [Issue #16](https://git.libre-chip.org/libre-chip/grant-tracking/issues/16) d-cache
+- € 2500 [Issue #17](https://git.libre-chip.org/libre-chip/grant-tracking/issues/17) memory load execution unit (we'll want to be able to do more than one load at once)
+- € 2500 [Issue #18](https://git.libre-chip.org/libre-chip/grant-tracking/issues/18) memory store execution unit
+- € 2000 [Issue #19](https://git.libre-chip.org/libre-chip/grant-tracking/issues/19) adding atomics: lr/sc, atomic fetch-add (or other fetch-op)
+- € 1000 [Issue #20](https://git.libre-chip.org/libre-chip/grant-tracking/issues/20) adding order-violation detection logic, so we can make memory look like it has total-store-order (for x86), or even sequential consistency (meaning we can ignore all non-IO fences)
 
 ## € 12000 Work towards the Formal Proof of No Spectre bugs
 
 This covers working on the Formal Proof of No Spectre bugs as well as improvements to other software/hardware needed for that. A major portion of this is to figure out what exact properties we need to formally prove for each part of the CPU, so we can put those parts together to make a working proof for the entire CPU. I'm hoping this will be enough work to get nearly all of the proof written out, even if there are some flaws we discover that we'll have to put off fixing for a later grant.
 
-- € 3000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Write Rocq and HDL logic for tracking which instructions will eventually be cancelled and which will eventually be retired.
-- € 9000 [Issue #N](https://git.libre-chip.org/libre-chip/grant-tracking/issues/) Attempt Proof that our CPU but with zeroed outputs for all eventually-cancelled instructions is equivalent to our real CPU design. This may need significant modifications to the CPU. This task may be too big and need further subdividing once we've made some progress on the proof so we know where to subdivide it.
+- € 3000 [Issue #21](https://git.libre-chip.org/libre-chip/grant-tracking/issues/21) Write Rocq and HDL logic for tracking which instructions will eventually be cancelled and which will eventually be retired.
+- € 9000 [Issue #22](https://git.libre-chip.org/libre-chip/grant-tracking/issues/22) Attempt Proof that our CPU but with zeroed outputs for all eventually-cancelled instructions is equivalent to our real CPU design. This may need significant modifications to the CPU. This task may be too big and need further subdividing once we've made some progress on the proof so we know where to subdivide it.

scripts/check-consistency.sh

@@ -52,7 +52,7 @@ function matches_split_prefix() {
     for split_token in "$@"; do
         text_prefix="$text"
         until [[ -z "$text_prefix" ]]; do
-            if [[ "$expected" = "$text_prefix" ]]; then
+            if [[ "$text_prefix" =~ ^"$expected"[[:blank:]]*$ ]]; then
                 return 0
             else
                 next_text_prefix="${text_prefix%"$split_token"*}"
@@ -86,51 +86,62 @@ function check_issue()
     nlnet_id="$2"
     subtask_title="$3"
     subtask_body="$4"
-    if [[ -z "$FORGEJO_TOKEN" ]]; then
-        return
-    fi
     example_title="NLnet $nlnet_id $subtask_title"
     body_prefix="Issue for tracking progress of a subtask of [NLnet grant $nlnet_id]($(grant_url "$nlnet_id")):
 $subtask_title
 $subtask_body
 "
     body_suffix="" # TODO
-    example_body_middle=$'\n<!-- add additional content here if you like -->\n'
+    body_middle_comment=$'<!-- add additional content here if you like -->'
+    example_body_middle=$'\n'"$body_middle_comment"$'\n'
     function error() {
-        # emit escape sequence for a hyperlink to the issue
         bar="---------------------------------------------------------------------------"
         body="$body_prefix"
         body_middle="${example_body_middle%$'\n'}"
         body+="${body_middle#$'\n'}"
         body+="$body_suffix"
-        printf '\e]8;;%s\e\\Issue #%s\e]8;;\e\\: error: %s\nExample Issue:\nTitle: %s\nDescription:\n%s\n%s\n%s\n' \
+        # emit escape sequence for a hyperlink to the issue
+        printf '\n\n\e]8;;%s\e\\Issue #%s\e]8;;\e\\: error: %s\nExample Issue:\nTitle: %s\nDescription:\n%s\n%s\n%s\n' \
             "$(issue_url "$issue_number")" "$issue_number" "$*" \
             "$example_title" "$bar" "$body" "$bar" >&2
         exit 1
     }
-    issue_json="$(curl -sS "https://git.libre-chip.org/api/v1/repos/libre-chip/grant-tracking/issues/$issue_number" \
-        -H "Accept: application/json" \
-        -H "Authorization: token $FORGEJO_TOKEN")" || error "can't retrieve issue"
-    issue_title="$(echo "$issue_json" | jq -r '.title')"
-    issue_body="$(echo "$issue_json" | jq -r '.body')"
+    if [[ "$issue_number" =~ ^'N'?$ ]]; then
+        error "issue number must be set"
+    fi
+    [[ "$issue_number" =~ ^[0-9]+$ ]] || error "invalid issue number"
+    if [[ "$FORGEJO_TOKEN" ]]; then
+        issue_json="$(curl -sS "https://git.libre-chip.org/api/v1/repos/libre-chip/grant-tracking/issues/$issue_number" \
+            -H "Accept: application/json" \
+            -H "Authorization: token $FORGEJO_TOKEN")" || error "can't retrieve issue"
+    else
+        # emit escape sequence for a hyperlink to the issue
+        printf '\n\n\e]8;;%s\e\\Issue #%s\e]8;;\e\\: warning: %s\n' \
+            "$(issue_url "$issue_number")" "$issue_number" \
+            "FORGEJO_TOKEN is not set, can't check issue (this is expected outside of CI)" >&2
+        return
+    fi
+    issue_title="$(echo "$issue_json" | jq -r '.title|gsub("\r\n"; "\n")')"
+    issue_body="$(echo "$issue_json" | jq -r '.body|gsub("\r\n"; "\n")')"
     [[ "$issue_title" =~ ^"NLnet $nlnet_id "(.*)$ ]] || error "title must start with \`NLnet $nlnet_id \`"
     issue_title_tail="${BASH_REMATCH[1]}"
-    split_punct=(',' '-' ';' ':')
+    split_punct=(',' '-' ';' ':' '. ')
     matches_split_prefix "$issue_title_tail" "$subtask_title" "${split_punct[@]}" || \
         error "issue title must be \`NLnet $nlnet_id \` followed by the subtask title, or a prefix of the subtask title that ends right before one of:$(printf ' `%s`' "${split_punct[@]}")"
     if [[ "$issue_body" =~ ^"$body_prefix".*"$body_suffix"$ ]]; then
         : # all good
-    elif [[ "$issue_body" =~ ^"$body_prefix"(.*)"$example_body_middle"(.*)$ || \
+    elif [[ "$issue_body" =~ ^"$body_prefix"(.*)"$body_middle_comment"(.*)$ || \
             "$issue_body" =~ ^"$body_prefix"(.*)()$ ]]; then
-        example_body_middle="${BASH_REMATCH[1]}$example_body_middle${BASH_REMATCH[2]}"
+        example_body_middle="${BASH_REMATCH[1]}$body_middle_comment${BASH_REMATCH[2]}"
         error "issue description is missing required suffix"
-    elif [[ "$issue_body" =~ ^(.*)"$example_body_middle"(.*)"$body_suffix"$ || \
+    elif [[ "$issue_body" =~ ^(.*)"$body_middle_comment"(.*)"$body_suffix"$ || \
             "$issue_body" =~ ^(.*)()"$body_suffix"$ ]]; then
-        example_body_middle="${BASH_REMATCH[1]}$example_body_middle${BASH_REMATCH[2]}"
+        printf '%q\n' "$body_prefix" "$issue_body"
+        example_body_middle="${BASH_REMATCH[1]}$body_middle_comment${BASH_REMATCH[2]}"
         error "issue description is missing required prefix"
-    elif [[ "$issue_body" =~ ^(.*)"$example_body_middle"(.*)$ || \
+    elif [[ "$issue_body" =~ ^(.*)"$body_middle_comment"(.*)$ || \
             "$issue_body" =~ ^(.*)()$ ]]; then
-        example_body_middle="${BASH_REMATCH[1]}$example_body_middle${BASH_REMATCH[2]}"
+        example_body_middle="${BASH_REMATCH[1]}$body_middle_comment${BASH_REMATCH[2]}"
         error "issue description is missing both the required prefix and suffix"
     fi
 )
@@ -231,7 +242,6 @@ function check_progress()
             issue_number="${BASH_REMATCH[2]}"
             issue_number2="${BASH_REMATCH[4]}"
             subtask_title="${BASH_REMATCH[5]}"
-            [[ "$issue_number" != "N" ]] || [[ "$nlnet_id" = "YYYY-MM-ID" ]] || nonfatal_error "issue number must be set"
             [[ ( "$issue_number" = "N" && -z "$issue_number2" ) || "$issue_number" = "$issue_number2" ]] || \
                 nonfatal_error "issue number in link name must match issue number in url"
             ((subtask_line_index = line_index))
@@ -252,7 +262,7 @@ function check_progress()
                     subtask_body_trailing_lines=""
                 fi
             done
-            if [[ "$issue_number2" =~ ^[0-9]+$ && "$nlnet_id" != "YYYY-MM-ID" && "$FORGEJO_TOKEN" ]]; then
+            if [[ "$nlnet_id" != "YYYY-MM-ID" ]]; then
                 check_issue "$issue_number2" "$nlnet_id" "$subtask_title" "$subtask_body" || diag "note:" -line_index="$subtask_line_index" "issue is linked from here"
             fi
         done